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

6.19.1.1. Синтаксис

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

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

• Правило расстановки отступов применяется в pragma. В настоящее время новый уровень отступа не задаётся, поэтому, если вы помещаете несколько правил в одну pragma 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 на уровне типов, каждая упомянутая переменная типа или вида также должна либо находиться в области видимости, либо быть связана с помощью 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" левая часть (LHS) не является применением; в "wrong2" переменная шаблона находится в голове LHS. В "wrong3" LHS состоит из конструктора, а не переменной, применённого к аргументу.

• Правило не обязано находиться в том же модуле, что и упомянутые в нём переменные (или хотя бы одна из них), однако, разумеется, они должны находиться в области видимости.
• Все правила неявно экспортируются из модуля и поэтому действуют во всех модулях, импортирующих модуль, в котором правило было определено, напрямую или косвенно. (То есть, если A импортирует B, который импортирует C, правила C действуют при компиляции A.) Ситуация очень похожа на ситуацию с объявлениями экземпляров.
• Внутри RULES «forall» считается ключевым словом независимо от любых других настроек флагов. Кроме того, внутри RULES автоматически включается языковое расширение ScopedTypeVariables; см. Переменные типов с лексической областью видимости.
• Как и другие pragmas, pragmas RULES всегда проверяются на ошибки области видимости и проходят проверку типов. Проверка типов означает, что LHS и RHS правила проверяются на соответствие типам и должны иметь одинаковый тип. Однако правила активируются только при включённом флаге -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 находит выражение, являющееся экземпляром LHS правила при некоторой подстановке, он заменяет это выражение на RHS с соответствующей подстановкой. Под «экземпляром при подстановке» подразумевается, что LHS можно сделать равным выражению, подставив значения вместо переменных шаблона.
• GHC совершенно не пытается проверять, имеют ли LHS и RHS правила одинаковый смысл. В общем случае это неразрешимо, а в большинстве интересных случаев — практически невыполнимо. Ответственность целиком лежит на программисте!

• GHC не пытается гарантировать, что правила конфлюэнтны или завершаются. Например:

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

  Это правило приведёт к бесконечному циклу компилятора.

• Если вызову соответствуют несколько правил, GHC произвольно выбирает одно из них для применения.

• В настоящее время GHC использует очень простой синтаксический алгоритм сопоставления LHS правила с выражением. Он ищет подстановку, при которой LHS и выражение синтаксически совпадают с точностью до альфа-переименования. При необходимости шаблон (правило), но не выражение, раскрывается по eta. (Раскрытие выражения по eta может привести к ошибкам ленивых вычислений.) Бета-преобразование не выполняется (оно называется сопоставлением высшего порядка).

  Сопоставление выполняется на промежуточном языке 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
  

• Правило со связанным forall переменной полиморфного типа, скорее всего, не сработает. Например:

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

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

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

  Обсуждение см. в #21093.

6.19.1.3. Взаимодействие правил с pragmas 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 была бы выше.

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

6.19.1.4. Взаимодействие правил с pragmas 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 может потребовать много работы, которая продублировалась бы при срабатывании правила.

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

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

CONLIKE — это модификатор pragma INLINE или NOINLINE. Он указывает, что применение f к одному аргументу (в общем случае — к числу аргументов слева от знака =) следует считать достаточно дешёвым для дублирования, если это дублирование позволит сработать правилу. Название «CONLIKE» — сокращение от «похожий на конструктор», поскольку конструкторы, безусловно, обладают таким свойством. Pragma CONLIKE является модификатором INLINE/NOINLINE, поскольку сопоставлять f в LHS правила имеет смысл, только если вы уверены, что 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 не получает возможности сработать по той же причине, что и в случае, описанном в разделе Взаимодействие правил с pragmas INLINE/NOINLINE.

Решение — самостоятельно определить функцию для конкретного экземпляра, запретить её преждевременное встраивание с помощью pragma и задать для неё 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 #-}

Если нужно RULE, которое действительно применяется к перегруженному методу класса, это можно сделать только следующим образом:

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. Слияние списков

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

К хорошим производителям относятся:

• Генераторы списков
• Диапазоны 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. Раньше можно было написать pragma SPECIALIZE с правой частью:

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

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

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

Это правило, выглядящее несколько необычно, указывает GHC заменять genericLookup на intLookup при совпадении типов. Более того, это правило не обязано находиться в том же файле, что и genericLookup, в отличие от pragmas 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, чтобы импортирующий модуль «видел» (:) и мог сопоставить его с LHS правила. INLINE предотвращает любое встраивание в RHS конструкции INLINE. Жаль, что здесь всё так деликатно.

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