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

Question

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

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

Answer 1

правило не срабатывает во многих случаях, потому что очень простая функция 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), что не соответствует правилу.

Answer 2

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

{-# 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 

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

mapf x = map f $ map f $ [x] 
mapf' x = map (f.f) $ [x] 
mapf'' x = map (\x -> f (f x)) $ [x]