Правила перезаписи Haskell и композиция функций

Почему Haskell требует нескольких правил перезаписи в зависимости от метода композиции функции и ее длины? Есть ли способ избежать этого?

Например, учитывая следующий код...

{-# RULES
"f/f" forall a. f ( f a ) = 4*a
  #-}
f a = 2 * a

это работает для

test1 = f ( f 1 )

однако нам нужно добавить правило для

test2 = f . f $ 1

а также

test3 = f $ f 1

оставив нам следующие правила

{-# RULES
"f/f1" forall a. f ( f a ) = 4 * a
"f/f2" forall a. f . f $ a  = 4 * a
"f/f3" forall a. f $ f $ a  = 4 * a
   #-}

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

test4 = f . f . f $ 1
test5 = f $ f $ f $ 1
test6 = f $ 1

Почему это? Должен ли я писать правила перезаписи для каждой возможной реализации?


function-composition rules haskell ghc
person Toymakerii    schedule 12.02.2012    source источник
comment
На самом деле я не знаю, но я предполагаю, что это потому, что правила перезаписи не применяются к импортированным вами функциям. А $ и . — это просто импортированные функции из Prelude.   -  person Tikhon Jelvis    schedule 13.02.2012

Ответы (2)


arrow_upward
13
arrow_downward

Во многих случаях правило не срабатывает, потому что очень простая функция f встраивается до того, как правило срабатывает. Если вы задержите встраивание,

{-# INLINE [1] f #-}

правило

{-# RULES "f/f" forall a. f (f a) = 4*a #-}

должен срабатывать во всех этих случаях (здесь работал с 7.2.2 и 7.4.1).

Причина в том, что сопоставитель правил не слишком проработан, он сопоставляет только выражения, имеющие синтаксическую форму правила (не совсем так, тело правила тоже подвергается некоторой нормализации). Выражения f $ f 3 или f . f $ 4 не соответствуют синтаксической форме правила. Чтобы правило совпало, должна произойти некоторая перезапись, ($) и (.) должны быть встроены до того, как правило будет соответствовать выражению. Но если вы не предотвратите встраивание f на первой фазе упрощения, оно будет заменено своим телом в том же прогоне, что и ($) и (.), поэтому на следующей итерации упроститель больше не увидит f, он видит только 2*(2*x), что не соответствует правилу.

person Daniel Fischer    schedule 13.02.2012

arrow_upward
3
arrow_downward

Я бы подумал, что это будет работать по умолчанию, но вы можете добавить еще два правила перезаписи, чтобы уменьшить ./$ до lambdas/application, чтобы это всегда совпадало:

{-# RULES
"f/f" forall a. f ( f a ) = 4*a

"app" forall f x. f $ x = f x
"comp" forall f g. f . g = (\x -> f (g x))
  #-}

f a = 3 * a -- make this 3*a so can see the difference

Тест:

main = do
    print (f . f $ 1)
    print (f (f 1))
    print (f $ f 1)
    print (f $ f $ 1)
    print (f $ f $ f $ f $ 1)
    print (f . f . f . f $ 1)
    print (f $ f $ f $ 1)
    print (f . f . f $ 1)
    print (f $ 1)

Выход:

4
4
4
4
16
16
12
12
3

Это также будет работать в некоторых (но не во всех) более неясных случаях из-за других правил перезаписи. Например, все это будет работать:

mapf x = map f $ map f $ [x]
mapf' x = map (f.f) $ [x]
mapf'' x = map (\x -> f (f x)) $ [x]
person porges    schedule 12.02.2012