Правила переписывания на Haskell и состав функций - PullRequest
9 голосов
/ 13 февраля 2012

Почему 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

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

Ответы [ 2 ]

13 голосов
/ 13 февраля 2012

Правило не срабатывает во многих случаях, потому что очень простая функция 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 в первую фазу упрощения, оно будет заменено своим телом в том же цикле, что и встроенные ($) и (.), поэтому в следующей итерации упрощатель не больше не вижу * 1017, он видит только 2*(2*x), что не соответствует правилу.

3 голосов
/ 13 февраля 2012

Я бы подумал, что это будет работать по умолчанию, но вы можете добавить еще два правила перезаписи, чтобы сделать ./$ сокращенным до 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]
...