Spec-Zone.ru › Haskell 9

6.19.1. Правила переписывания

{-# RULES "⟨name⟩" forall ⟨binder⟩ ... . ⟨expr⟩ = ⟨expr⟩ ... #-}
Где:

верхнего уровня

Определяет правило переписывания, используемое для оптимизации исходной программы.

Программист может указать правила переписывания как часть исходной программы (в директиве). Вот пример:

{-# RULES
      "map/map"    forall f g xs.  map f (map g xs) = map (f . g) xs
  #-}

Используйте флаг отладки -ddump-simpl-stats, чтобы увидеть, какие правила сработали. Если вам нужна более подробная информация, то -ddump-rule-firings покажет каждое отдельное срабатывание правила, а -ddump-rule-rewrites также покажет, как код выглядит до и после переписывания.

-fenable-rewrite-rules

Разрешает компилятору применять правила переписывания к исходной программе.

6.19.1.1. Синтаксис

С точки зрения синтаксиса:

  • В директиве RULES может быть ноль или более правил, разделенных точкой с запятой (которая может быть сгенерирована правилом форматирования).
  • Правило форматирования применяется в директиве. В настоящее время новый уровень отступа не устанавливается, поэтому если вы поместите несколько правил в одну директиву RULES и хотите использовать форматирование для их разделения, вам необходимо выровнять начало по той же колонке, что и окружающие определения.

    {-# RULES
          "map/map"    forall f g xs.  map f (map g xs) = map (f . g) xs
          "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
      #-}
    

    Кроме того, закрывающая #-} должна начинаться в колонке правее открывающей {-#.

  • Каждое правило имеет имя, заключённое в двойные кавычки. Само имя не имеет никакого значения. Оно используется только при сообщении о том, сколько раз правило сработало.
  • Правило может необязательно иметь номер управления фазами (см. Управление фазами), сразу после имени правила. Таким образом:

    {-# RULES
          "map/map" [2]  forall f g xs. map f (map g xs) = map (f . g) xs
      #-}
    

    [2] означает, что правило активно в 2-й и последующих фазах. Обратный вариант [~2] также принимается, что означает, что правило активно до, но не включая, 2-ю фазу.

    Правила поддерживают специальную запись управления фазами [~], что означает, что правило никогда не активно. Эта функция поддерживает плагины (см. Плагины компилятора), позволяя определять RULE, который никогда не запускается GHC, но при этом парсится, проверяется на типы и т. д., чтобы он был доступен плагину.

  • Каждая (терм)переменная, упомянутая в правиле, должна быть либо в области видимости (например, map), либо связана с forall (например, f, g, xs). Переменные, связанные с forall, называются переменными шаблона. Они разделяются пробелами, так же как и в типе forall.
  • У переменной шаблона может быть необязательная подпись типа. Если тип переменной шаблона полиморфный, у него обязательно должна быть подпись типа. Например, вот правило foldr/build:

    "fold/build"  forall k z (g::forall b. (a->b->b) -> b -> b) .
                  foldr k z (build g) = g k z
    

    Так как g имеет полиморфный тип, у него должна быть подпись типа.

  • Если включена опция ExplicitForAll, переменные типа/вида также могут быть явно связаны. Например:

    {-# RULES "id" forall a. forall (x :: a). id @a x = x #-}
    

    Когда присутствует явная переменная типа/вида на уровне типа, каждая переменная типа/вида, упомянутая в нём, должна теперь также быть либо в области видимости, либо связана с forall. В частности, в отличие от некоторых других мест в Haskell, это означает, что свободные переменные вида не будут неявно связаны. Например:

    "this_is_bad" forall (c :: k). forall (x :: Proxy c) ...
    "this_is_ok"  forall k (c :: k). forall (x :: Proxy c) ...
    

    Когда нужны связанные переменные типа/вида, оба forall должны всегда включаться, хотя если переменные шаблона не нужны, второй можно оставить пустым. Например:

    {-# RULES "map/id" forall a. forall. map (id @a) = id @[a] #-}
    
  • Левая часть правила должна состоять из переменной верхнего уровня, применённой к произвольным выражениям. Например, это не правильно:

    "wrong1"   forall e1 e2.  case True of { True -> e1; False -> e2 } = e1
    "wrong2"   forall f.      f True = True
    "wrong3"   forall x.      Just x = Nothing
    

    В "wrong1" левая часть не является применением; в "wrong2" левая часть содержит переменную шаблона в голове. В "wrong3" левая часть состоит из конструктора, а не переменной, применённого к аргументу.

  • Правило не обязательно должно быть в том же модуле, что и (любая из) переменных, которые оно упоминает, хотя, конечно, они должны быть в области видимости.
  • Все правила неявным образом экспортируются из модуля и поэтому действуют в любом модуле, который импортирует модуль, определивший правило, непосредственно или косвенно. (То есть, если A импортирует B, который импортирует C, правила C действуют при компиляции A.) Ситуация очень похожа на ту, что, например, для объявлений переменных.
  • Внутри директивы RULES «forall» обрабатывается как ключевое слово, независимо от других настроек флагов. Кроме того, внутри директивы RULES, расширение языка ScopedTypeVariables автоматически включено; см. Лексически связанные переменные типа.
  • Как и другие директивы, директивы RULES всегда проверяются на ошибки области видимости и проверяются на типы. Проверка типов означает, что левая и правая части правила проверяются на типы и должны иметь один и тот же тип. Однако правила активируются только в том случае, если включён флаг -fenable-rewrite-rules (см. Семантика).

6.19.1.2. Семантика

С точки зрения семантики:

  • Правила активируются (то есть используются во время оптимизации) флагом -fenable-rewrite-rules. Этот флаг подразумевается флагом -O, и может быть отключён (как обычно) флагом -fno-enable-rewrite-rules. (Примечание: включение -fenable-rewrite-rules без -O может не дать ожидаемого результата, так как без -O GHC игнорирует всю информацию об оптимизации в файлах интерфейса; см. -fignore-interface-pragmas). Обратите внимание, что -fenable-rewrite-rules является флагом оптимизации и не оказывает никакого влияния на синтаксический анализ или типизацию.
  • Правила рассматриваются как правила переписывания слева направо. Когда GHC находит выражение, являющееся подстановкой левой части правила, он заменяет выражение правой частью (с соответствующей подстановкой). Под «подстановкой» подразумевается, что левую часть можно сделать равной выражению, выполнив подстановку для переменных шаблона.
  • GHC не пытается проверить, что левая и правая части правила имеют одинаковый смысл. Это, вообще говоря, неразрешимо, и невыполнимо в большинстве интересных случаев. Ответственность целиком и полностью лежит на программисте!
  • GHC не пытается убедиться, что правила являются конfluent или завершаемыми. Например:

    "loop"        forall x y.  f x y = f y x
    

    Это правило заставит компилятор попасть в бесконечный цикл.

  • Если несколько правил соответствуют вызову, GHC выберет одно произвольно для применения.
  • GHC в настоящее время использует очень простой, синтаксический алгоритм сопоставления для сопоставления левой части правила с выражением. Он ищет подстановку, которая делает левую часть и выражение синтаксически равными с учётом альфа-преобразования. Шаблон (правило), но не выражение, расширяется эта-преобразованием, если необходимо. (Расширение эта-преобразованием выражения может привести к ошибкам ленивости.) Но не бета-преобразование (это называется сопоставлением высокого порядка).

    Сопоставление выполняется на промежуточном языке GHC, который включает абстракции типов и приложения. Таким образом, правило соответствует только в том случае, если типы тоже совпадают. См. Специализация ниже.

  • GHC продолжает попытки применения правил по мере оптимизации программы. Например, рассмотрим:

    let s = map f
        t = map g
    in
    s (t xs)
    

    Выражение s (t xs) не соответствует правилу "map/map", но GHC подставит значения для s и t, что даст выражение, которое соответствует. Если s или t использовалось (а) более одного раза и (б) было большим или редексом, то оно не было бы заменено, и правило не сработало бы.

  • GHC никогда не будет сопоставлять переменную forall в шаблоне с выражением, содержащим локально связанные переменные. Например, разрешается написать правило, содержащее выражение case:

    {-# RULES
      "test/case-tup" forall (x :: (Int, Int)) (y :: Int) (z :: Int).
        test (case x of (l, r) -> y) z = case x of (l, r) -> test y z
      #-}
    

    Но правило не будет соответствовать, когда y содержит либо l, либо r, поскольку они связаны локально. Таким образом, следующее применение не вызовет правило:

    prog :: (Int, Int) -> (Int, Int)
    prog x = test (case x of (p, q) -> p) 0
    

    потому что y должно соответствовать p (которое связано локально), но оно сработает для:

    prog :: (Int, Int) -> (Int, Int)
    prog x = test (case x of (p, q) -> 0) 0
    

    потому что y может соответствовать 0.

  • GHC реализует сопоставление высокого порядка, как описано в предложении GHC #555. Когда переменная шаблона применяется к различным локально связанным переменным, она образует то, что мы называем шаблоном высокого порядка. При сопоставлении шаблоны высокого порядка обрабатываются как переменные шаблонов, но им разрешается соответствовать выражениям, содержащим локально связанные переменные, которые являются частью шаблонов высокого порядка.

    Например, это позволяет исправить нерабочее правило из примера предыдущего пункта:

    {-# RULES
      "test/case-tup" forall (x :: (Int, Int)) (f :: Int -> Int -> Int) (z :: Int).
        test (case x of (l, r) -> f l r) z = case x of (m, n) -> test (f m n) z
      #-}
    

    Это изменённое правило срабатывает для:

    prog :: (Int, Int) -> (Int, Int)
    prog x = test (case x of (p, q) -> p) 0
    

    При сопоставлении высокого порядка f p q соответствует p, назначив f = \p q -> p. Полученный код после переписывания:

    prog x = case x of (m, n) -> test ((\p q -> p) m n) 0
    
  • Правило, содержащее обобщающий связующий элемент с полиморфным типом, вероятно, не сработает. Например:

    {-# RULES forall (x :: forall a. Num a => a -> a).  f x = blah #-}
    

    Здесь x имеет полиморфный тип. Это относится к обобщающему связующему элементу с ограничением класса типов, например:

    {-# RULES forall @m (x :: KnownNat m => Proxy m).  g x = blah #-}
    

    См. #21093 для обсуждения.

6.19.1.3. Как правила взаимодействуют с директивами INLINE/NOINLINE

Обычная вставка происходит одновременно с переписыванием правил, что может привести к неожиданным результатам. Рассмотрим этот (искусственный) пример

f x = x
g y = f y
h z = g True

{-# RULES "f" f True = False #-}

Поскольку правая часть f небольшая, она вставляется в g, что даёт

g y = y

Теперь g вставляется в h, но RULE f не имеет возможности сработать. Если бы GHC сначала вставил g в h, то было бы больше шансов, что RULES f сработало бы.

Для получения предсказуемого поведения необходимо использовать директиву NOINLINE или директиву INLINE[⟨phase⟩] для f, чтобы убедиться, что она не вставляется до тех пор, пока её RULES не будет иметь возможности сработать. Флаг предупреждений -Winline-rule-shadowing (см. Предупреждения и проверка корректности) предупреждает об этой ситуации.

6.19.1.4. Как правила взаимодействуют с директивами CONLIKE

GHC очень осторожен в отношении дублирования работы. Например, рассмотрим

f k z xs = let xs = build g
           in ...(foldr k z xs)...sum xs...
{-# RULES "foldr/build" forall k z g. foldr k z (build g) = g k z #-}

Поскольку xs используется дважды, GHC не запускает правило foldr/build. Это правильно, так как вычисление xs может потребовать значительных затрат, которые будут дублироваться при запуске правила.

Иногда, однако, этот подход чересчур осторожен, и мы хотим, чтобы правило сработало, даже если это приведёт к дублированию redex. GHC не может определить, когда это хороший подход, поэтому мы предоставляем директиву CONLIKE для её объявления, например:

{-# INLINE CONLIKE [1] f #-}
f x = blah

CONLIKE – это модификатор для директив INLINE или NOINLINE. Он указывает, что применение f к одному аргументу (в общем случае, к числу аргументов слева от знака =) должно считаться достаточно дешёвым, чтобы его можно было дублировать, если такое дублирование позволит сработать правилу. (Название «CONLIKE» сокращение от «constructor-like», так как у конструкторов, безусловно, есть такое свойство). Директива CONLIKE – это модификатор для INLINE/NOINLINE, так как она действительно имеет смысл только в том случае, если вам известно, что f соответствует левой части правила, если вы уверены, что f не будет вставлен до того, как правило получит возможность сработать.

6.19.1.5. Как правила взаимодействуют с методами класса

Нежелательно давать RULE для метода класса:

class C a where
  op :: a -> a -> a

instance C Bool where
  op x y = ...rhs for op at Bool...

{-# RULES "f" op True y = False #-}

В этом примере, op – это не обычная функция верхнего уровня; это метод класса. GHC быстро переписывает любые вхождения op-используемое-с-типом-Bool в специализированную функцию, скажем, opBool, где

opBool :: Bool -> Bool -> Bool
opBool x y = ..rhs for op at Bool...

Таким образом, RULE никогда не имеет возможности сработать по тем же причинам, что и в Как правила взаимодействуют с директивами INLINE/NOINLINE.

Решение заключается в определении функции, специфичной для экземпляра, с директивой для предотвращения преждевременной вставки и предоставлением RULE для неё:

instance C Bool where
  op = opBool

opBool :: Bool -> Bool -> Bool
{-# NOINLINE [1] opBool #-}
opBool x y = ..rhs for op at Bool...

{-# RULES "f" opBool True y = False #-}

Если вы хотите правило, которое действительно относится к перегруженному методу класса, единственный способ – сделать это так:

class C a where
  op_c :: a -> a -> a

op :: C a => a -> a -> a
{-# NOINLINE [1] op #-}
op = op_c

{-# RULES "reassociate" op (op x y) z = op x (op y z) #-}

Теперь вставка op откладывается до тех пор, пока правило не получит возможность сработать. Недостаток состоит в том, что объявления экземпляров должны определить op_c, но все другие использования должны происходить через op.

6.19.1.6. Слияние списков

Механизм правил используется для реализации слияния (сжатия) общих функций над списками. Если «хороший потребитель» потребляет промежуточный список, созданный «хорошим производителем», промежуточный список должен быть полностью удалён.

Хорошими производителями являются:

  • Списки-генераторы
  • Перечисления Int, Integer и Char (например, ['a'..'z']).
  • Явные списки (например, [True, False])
  • Конструктор cons (например 3:4:[])
  • ++
  • map
  • take, filter
  • iterate, repeat
  • zip, zipWith

Хорошими потребителями являются:

  • Списки-генераторы
  • array (по второму аргументу)
  • ++ (по первому аргументу)
  • foldr
  • map
  • take, filter
  • concat
  • unzip, unzip2, unzip3, unzip4
  • zip, zipWith (но только по одному аргументу; если оба являются хорошими производителями, zip сольётся только с одним)
  • partition
  • head
  • and, or, any, all
  • sequence_
  • msum

Например, следующее не должно генерировать промежуточных списков:

array (1,10) [(i,i*i) | i <- map (+ 1) [0..9]]

Этот список можно легко расширить; если вы часто используете функции Prelude, которых нет в списке, сообщите нам об этом.

Если вы хотите написать собственных хороших потребителей или производителей, обратитесь к определениям функций Prelude выше, чтобы узнать, как это сделать.

6.19.1.7. Специализация

Правила переписывания могут использоваться для достижения того же эффекта, что и функция, присутствующая в более ранних версиях GHC. Например, предположим, что:

genericLookup :: Ord a => Table a b   -> a   -> b
intLookup     ::          Table Int b -> Int -> b

где intLookup — реализация genericLookup, которая работает очень быстро для ключей типа Int. Возможно, вы захотите сказать GHC использовать intLookup вместо genericLookup всякий раз, когда последний вызывается с типом Table Int b -> Int -> b. Раньше было возможно написать прагму SPECIALIZE с правой частью:

{-# SPECIALIZE genericLookup :: Table Int b -> Int -> b = intLookup #-}

Эта функция больше не поддерживается в GHC, но правила переписывания позволяют сделать то же самое:

{-# RULES "genericLookup/Int" genericLookup = intLookup #-}

Это немного необычное правило инструктирует GHC заменить genericLookup на intLookup при совпадении типов. Более того, это правило не обязательно должно находиться в том же файле, что и genericLookup, в отличие от прагм SPECIALIZE, которые в настоящее время это делают (так что они имеют доступное для специализации исходное определение).

Вы несёте ответственность за то, чтобы intLookup действительно вела себя как специализированная версия genericLookup!!!

Пример, в котором использование RULES для специализации даст значительный выигрыш:

toDouble :: Real a => a -> Double
toDouble = fromRational . toRational

{-# RULES "toDouble/Int" toDouble = i2d #-}
i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly

Функция i2d практически является одной машинной инструкцией; по сравнению, стандартное преобразование через промежуточную Rational-оказалось крайне затратным.

6.19.1.8. Управление процессами в правилах переписывания

  • Используйте -ddump-rules, чтобы увидеть правила, определённые в этом модуле. Это включает правила, сгенерированные этапом специализации, но исключает правила, импортированные из других модулей.
  • Используйте -ddump-simpl-stats, чтобы увидеть, какие правила применяются. Если вы добавите -dppr-debug, вы получите более подробный список.
  • Используйте -ddump-rule-firings или -ddump-rule-rewrites, чтобы подробно увидеть, какие правила применяются. Если вы добавите -dppr-debug, вы получите ещё более подробный список.
  • Определение (скажем) build в GHC/Base.hs выглядит следующим образом:

    build   :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
    {-# INLINE build #-}
    build g = g (:) []
    

    Обратите внимание на INLINE! Это предотвращает встраивание (:) при компиляции PrelBase, так что импортирующий модуль «увидит» (:) и сможет сопоставить его с левой частью правила. INLINE предотвращает любое встраивание в правой части INLINE. Мне жаль за тонкость этого.

  • В libraries/base/GHC/Base.hs посмотрите на правила для map, чтобы узнать, как писать правила, которые будут выполнять слияние и тем не менее дадут эффективную программу, даже если слияние не произойдёт. Больше правил в GHC/List.hs.

© 2002–2007 The University Court of the University of Glasgow. All rights reserved.
Licensed under the Glasgow Haskell Compiler License.
https://downloads.haskell.org/~ghc/9.12.1/docs/users_guide/exts/rewrite_rules.html

Spec-Zone.ru

Настройки Оффлайн Что нового Помощь О нас
Spec-Zone .ru
спецификации, руководства, описания, API