前面给了一个Product的等价表示，还有一种是Sum的。
同样的先给出两种表示。
data S a b = L a | R b
等价的表示：
newtype S‘ a b = S‘ { unS‘ :: forall r. (a -> r) -> (b -> r) -> r }
这里对于S’,forall r限制了可能的值。由于r不可知，所有只能是下面的两种形式：
sl = \f g -> f x sr = \f g -> g y
可以证明:
sl id g‘ == id x == x
sr f‘ id == id y == y
这里g’和f’未知，但是我们可以用不定点来替代。
g‘ = \_ -> fix id
f’ = \_ ->fix id
所以递归的表示为：
sl = \f g -> f (sl id (\_ -> fix id))
sr = \f g -> g (sr (\_ ->fix id) id)
剩下的给出一一映射关系：
toS‘ :: S a b -> S‘ a b toS‘ (L a) = S‘ (\f g -> f a) toS‘ (R b) = S‘ (\f g -> g b)
反方向比较麻烦一点，我们需要判断是S‘两种形式的哪一种。
我们给出一个helper函数toTrue和toFalse，用它们来test我们的S‘表示，由此来判断是哪种。
toTrue :: a -> Bool toTrue _ = True toFalse :: a -> Bool toFalse _ = False
fromS‘ :: S‘ a b -> S a b fromS‘ (S‘ s) = case (s toTrue toTrue) == (s toFalse toTrue) of True -> R (s (\_ ->fix srf) id) False -> L (s id (\_ ->fix slf))
好了，剩下的不证明了。 ：）
有了RankNTypes,代数数据结构不是必须的。(结论太早？没有考虑递归的代数数据结构：）)
后面会谈谈free monad的非代数数据结构表示，因为Free monad可以看成是很多层的数据包装，所以等价的函数表示会跟高效。
原文：http://www.cnblogs.com/ski-comb/p/4361401.html