I = \ x . x
I x = x
I = S K K
id
K = \ x y . x
K x = \ _ . x
const
, pure
for Applicative (r →)
S = \ x y z . x z (y z)
(S f g) x = (f x) (g x)
(<*>)
for Applicative (r →)
S
combinator an S?B = \ x y z . x (y z)
(B f g) x = f (g x)
(.)
、fmap
for Functor (r →)
C = \ x y z . x z y
(C f) x y = f y x
flip
W = \ x y . x y y
(W f) x = f x x
join
for Monad (r →)
P = \ x y z w . x (y z) (y w)
(P f g) x y = f (g x) (g y)
on
如果想定義下面的遞迴函式 f
(注意到下面的定義裡 f
指涉到了自己):
我們可以定義函式 F
:
然後用不動點組合子 fix
實現遞迴:
Y = \ f . (\ x . f (x x)) (\ x . f (x x))
X = \ f . (\ x . x x) (\ x . f (x x))
Z = \ f . (\ x . f (\ v . x x v)) (\ x . f (\ v . x x v))
Y' = (\ x y . x y x) (\ y x . y (x y x))
Θ = (\ x y . y (x x y)) (\ x y . y (x x y))
Θv = (\ x y . y (\v. x x y v)) (\ x y . y (\v. x x y v))
上面的 Z
跟 Θv
是 Y
跟 Θ
在及早求值語言裡的版本,就不會無止境:
編碼大致上分為 Church 編碼與 Scott 編碼兩大類,對於非遞迴定義的型態來說這兩類編碼除了參數順序以外都相同。
假設型態 T
定義如下
(或用 GADT 語法定義)
建構子 Cj
編碼成
那麼它的資料本身就能反映模式匹配:
與 Scott 編碼不同的是,Church 編碼會自動將應用上的值進一步應用於嵌入建構式的值中。
粗略地說,建構子 Cj
可能會編碼成
Bool = True | False
直接 if cond then else = cond then else
Nat = Zero | Succ Nat
Nat = Ed | B0 Nat | B1 Nat
如果我們讓 B0 Ed = Ed
,那麼就要改成下面的樣子
(x, xs)
機制很酷:
(isNil, (x, xs))
List a = Nil | Cons a (List a)
列表代表 foldr
上面用到了 map
-foldr
fusion:
列表代表 foldl