Применение Theorems for free

[deniok]

Выложу-ка я мой ответ kurilka про применение Theorems for free как пост, а то в докладе на SPbHUG я это как-то не успел рассказать.




build/fold и map/map rules используются для оптимизаций в Rewrite rules в GHC.

Есть ещё destroy/unfoldr rule для

destroy :: forall a.forall c.(forall b. (b -> Maybe (a,b)) -> b -> c) -> [a] -> c
unfoldr :: forall a.forall b.(b -> Maybe (a,b)) -> b -> [a]

для того же самого, что build/fold.

И ещё Concatenates Vanish Rule, позволяющее элиминировать конкатенации списков:

Для любой

g :: forall b.b -> (A -> b -> b) -> (b -> b -> b) -> b

выполняется теорема

g [] (:) (++) = vanish g

где

vanish :: forall a. (forall b.b -> (a -> b -> b)
                              -> (b -> b -> b)) -> [a]
vanish g = g id (\x h ys -> x:(h ys)) (.) []

Но этого в GHC не используют, хотя программист при желании может сам задать соответствующие правила.

Фишка в применении Free Theorems в том, что функции должны быть под них заточены. Библиотечные реализации многих функций из Prelude написаны так, чтобы быть хорошими консьюмерами и продюсерами для List Fusion.