Как использовать фазовый контроль встраивания в haskell?
Документация говорит,
Иногда вы хотите точно контролировать, когда в конвейере GHC включена прагма INLINE.
Зачем мне это хотеть? (За исключением случаев, когда я также использую прагму "ПРАВИЛА", в этом случае я могу отложить встраивание функции для того, чтобы разрешить запуск связанных правил.) Какие типы функций лучше встроить только на определенной стадии упрощения процесса?
2 ответа
Вы, по сути, ответили на свой вопрос, как говорили другие. Но я думаю, что вам может понадобиться более урезанный и конкретный пример использования фазового контроля в сочетании с RULES/INLINE это выгодно.* Вы не видите их за пределами сильно оптимизированных библиотек, которые часто бывают сложными, поэтому здорово видеть меньшие случаи.
Вот пример, который я недавно реализовал, используя схемы рекурсии. Мы проиллюстрируем это, используя концепцию катаморфизма. Вам не нужно знать, что это такое, просто они характеризуют операторы свертывания. (Действительно, не зацикливайтесь здесь на абстрактных понятиях. Это просто самый простой пример, который у меня есть, где вы можете неплохо ускориться.)
Краткое введение в катаморфизм
Мы начнем с Muтип фиксированной точки и определение Algebra который является просто причудливым синонимом функции, которая "деконструирует" значение f a вернуть a,
newtype Mu f = Mu { muF :: f (Mu f) }
type Algebra f a = f a -> a
Теперь мы можем определить два оператора, ffold а также fbuild, которые являются весьма универсальными версиями традиционных foldr а также build операторы для списков:
ffold :: Functor f => Algebra f a -> Mu f -> a
ffold h = go h
where go g = g . fmap (go g) . muF
{-# INLINE ffold #-}
fbuild :: Functor f => (forall b. Algebra f b -> b) -> Mu f
fbuild g = g Mu
{-# INLINE fbuild #-}
Грубо говоря, ffold разрушает структуру, определяемую Algebra f a и дает a, fbuild вместо этого создает структуру, определяемую его Algebra f a и дает Mu значение. Тот Mu значение соответствует любому рекурсивному типу данных, о котором вы говорите. Как обычный foldr а также build: мы деконструируем список, используя его минусы, и мы также строим список, используя его минусы. Идея в том, что мы только что обобщили эти классические операторы, чтобы они могли работать с любым рекурсивным типом данных (например, списками или деревьями!)
Наконец, есть закон, который сопровождает этих двух операторов, который будет направлять нашу общую RULE:
forall f g. ffold f (build g) = g f
Это правило по существу обобщает оптимизацию обезлесения / слияния - удаление промежуточной структуры. (Я полагаю, что доказательство правильности указанного закона оставлено читателю в качестве упражнения. Должно быть довольно легко с помощью эквалайзера).
Теперь мы можем использовать эти два комбинатора, наряду с Mu, для представления рекурсивных типов данных, таких как список. И мы можем написать операции над этим списком.
data ListF a f = Nil | Cons a f
deriving (Eq, Show, Functor)
type List a = Mu (ListF a)
instance Eq a => Eq (List a) where
(Mu f) == (Mu g) = f == g
lengthL :: List a -> Int
lengthL = ffold g
where g Nil = 0
g (Cons _ f) = 1 + f
{-# INLINE lengthL #-}
И мы можем определить map функция также:
mapL :: (a -> b) -> List a -> List b
mapL f = ffold g
where g Nil = Mu Nil
g (Cons a x) = Mu (Cons (f a) x)
{-# INLINE mapL #-}
Встраивание FTW
Теперь у нас есть средство написания терминов над этими рекурсивными типами, которые мы определили. Тем не менее, если бы мы написать такой термин, как
lengthL . mapL (+1) $ xs
Тогда, если мы расширим определения, мы по существу получим композицию из двух ffold операторы:
ffold g1 . ffold g2 $ ...
А это значит, что мы фактически разрушаем структуру, затем восстанавливаем ее и разрушаем снова. Это действительно расточительно. Также мы можем переопределить mapL с точки зрения fbuildтак что, будем надеяться, он сливается с другими функциями.
Ну, у нас уже есть закон, так что RULE в порядке. Давайте кодифицировать это:
{-# RULES
-- Builder rule for catamorphisms
"ffold/fbuild" forall f (g :: forall b. Algebra f b -> b).
ffold f (fbuild g) = g f
-}
Далее мы переопределим mapL с точки зрения fbuild для целей слияния:
mapL2 :: (a -> b) -> List a -> List b
mapL2 f xs = fbuild (\h -> ffold (h . g) xs)
where g Nil = Nil
g (Cons a x) = Cons (f a) x
{-# INLINE mapL2 #-}
Ааааа а мы закончили, верно? Неправильно!
Фазы для удовольствия и прибыли
Проблема в том, что когда происходит встраивание, нет никаких ограничений, что полностью испортит это. Рассмотрим случай, который мы ранее хотели оптимизировать:
lengthL . mapL2 (+1) $ xs
Мы хотели бы, чтобы определения lengthL а также mapL2 быть встроенным, чтобы ffold/fbuild Правило может стрелять послесловиями по всему телу. Итак, мы хотим перейти к:
ffold f1 . fbuild g1 ...
через встраивание, и после этого перейдите к:
g1 f1
через наш RULE,
Ну, это не гарантировано. По существу, на одном этапе упрощения GHC может не только включать определения lengthL а также mapL, но он также может включать определения ffold а также fbuild на их сайтах использования. Это означает, что ПРАВИЛО никогда не получит шанс запустить, так как фаза "сожрала" все соответствующие идентификаторы и впутала их в ничто.
Наблюдение состоит в том, что мы хотели бы включить ffold а также fbuild как можно позже. Таким образом, мы постараемся раскрыть как можно больше возможностей для применения нашего ПРАВИЛА. И если этого не произойдет, то тело будет встроено, и GHC все равно даст все возможное. Но, в конечном счете, мы хотим, чтобы он был встроен поздно; RULE сэкономит нам больше эффективности, чем любая умная оптимизация компилятора.
Так что исправление здесь заключается в том, чтобы аннотировать ffold а также fbuild и укажите, что они должны стрелять только на этапе 1:
ffold g = ...
{-# INLINE[1] ffold #-}
fbuild g = ...
{-# INLINE[1] fbuild #-}
Сейчас, mapL и друзья будут вставлены очень рано, но они придут очень поздно. GHC начинается с некоторого номера фазы N, а номера фаз уменьшаются до нуля. Фаза 1 является последней фазой. Также было бы возможно встроить fbuild/ffold раньше, чем Фаза 1, но это, по сути, означает, что вам нужно начать увеличивать количество фаз, чтобы восполнить это, или начать следить за тем, чтобы ПРАВИЛО всегда срабатывало на некоторых более ранних стадиях.
Заключение
Вы можете найти все это и многое другое в моей сути **, со всеми упомянутыми определениями и примерами здесь. Это также идет с критерием критерия нашего примера: с нашими фазовыми аннотациями GHC может сократить время выполнения lengthL . mapL2 пополам по сравнению с lengthL . mapL1, когда RULE пожары.
Если вы хотите увидеть это сами, вы можете скомпилировать код с -ddump-simpl-statsи увидеть, что ffold/fbuild правило срабатывает во время компиляции конвейера.
Наконец, большинство таких же принципов применимы к библиотекам, таким как vector или bytestring. Хитрость в том, что у вас может быть несколько уровней встраивания здесь и намного больше правил. Это связано с тем, что такие методы, как слияние потоков и массивов, имеют тенденцию эффективно объединять циклы и повторно использовать массивы - в отличие от этого, где мы просто делаем классическую вырубку лесов, удаляя промежуточную структуру данных. В зависимости от традиционного "шаблона" сгенерированного кода (скажем, из-за векторизованного, параллельного понимания списков) может стоить того, чтобы чередовать или, в частности, выполнять фазовую оптимизацию таким образом, чтобы очевидные недостатки были устранены ранее. Или оптимизировать для случаев, когда RULE в сочетании с INLINE даст больше RULEs (отсюда ступенчатые фазы, которые вы видите иногда - это в основном чередует фазу встраивания.) По этим причинам вы также можете контролировать фазы, в которых RULE пожары.
Так что пока RULEЭтапы могут сэкономить нам много времени выполнения, они могут занять много времени, чтобы получить права тоже. Вот почему вы часто видите их только в самых "высокопроизводительных", сильно оптимизированных библиотеках.
Заметки
* Ваш первоначальный вопрос был "какие функции выигрывают от контроля фазы", что для меня звучит как вопрос "какие функции выигрывают от постоянного устранения подвыражений". Я не уверен, как точно ответить на это, если это вообще возможно! Это больше относится к области компиляции, чем к любому теоретическому результату о том, как ведут себя функции или программы - даже с математическими законами, не все "оптимизации" дают ожидаемые результаты. В результате, ответ на самом деле таков: "Вы, вероятно, будете знать, когда будете писать и оценивать его".
** Вы можете спокойно игнорировать много других вещей в файле; В основном это была игровая площадка, но вам тоже может быть интересно. Там есть и другие примеры, такие как натуральные и бинарные деревья - вы можете попробовать использовать различные другие возможности слияния, используя их.
Во-первых, я должен отметить, что поведение GHC по умолчанию разработано так, чтобы быть в большинстве случаев оптимальным. Если у вас нет проблем, вы, вероятно, лучше всего позволите очень умным людям, которые каждый день думают о Haskell, быть в основном правы (PS Я не из тех людей), но вы спросили...
Насколько я понимаю, есть две причины использования этого.
Заставьте программу сходиться в лучшую форму быстрее:
Haskell будет пытаться каждый проход правил несколько раз, пока то, что выходит на другом конце, строго лучше, чем то, с чего он начинал. Он всегда будет сходиться, но ничто не говорит о том, что он сделает это до тепловой смерти вселенной. В общем случае для этого требуется не более руки, полной пасов, но есть некоторые угловые случаи, которые можно сделать патологически плохими. Это позволит вам вручную обойти эти крайние случаи, если они возникнут.
Избегайте сближения с локальным минимумом
Есть несколько случаев, когда применение правила
Aпредотвратит применение лучшего правилаB, Тогда важно, чтобыBприйти раньшеA, Правила оптимизации по умолчанию хорошо разработаны, чтобы избежать этой проблемы, но, как говорится в документации, они также очень консервативны. По мере добавления новых правил вы неизбежно начнете нарушать другие возможные оптимизации. Затем вам нужно будет найти место в цепочке правил, где это не произойдет. Насколько мне известно, единственный способ узнать это методом проб и ошибок.