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.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2007-11-18 11:18 am (UTC)Есть ещё destroy/unfoldr rule для
для того же самого, что build/fold.
И ещё Concatenates Vanish Rule, позволяющее элиминировать конкатенации списков:
Для любой
выполняется теорема
где
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.