Lambda encoding

組合子 combinator

• I = \ x . x
  • 恆等函式：I x = x
  • I = S K K
  • Haskell：id
• K = \ x y . x
  • 常數函式：K x = \ _ . x
  • Haskell：const, pure for Applicative (r →)
• S = \ x y z . x z (y z)
  • 融合（fusion）：(S f g) x = (f x) (g x)
  • Haskell：(<*>) for Applicative (r →)
  • Why is the S combinator an S?
• B = \ x y z . x (y z)
  • 合成：(B f g) x = f (g x)
  • Haskell：(.)、fmap for Functor (r →)
• C = \ x y z . x z y
  • 交換：(C f) x y = f y x
  • Haskell：flip
• W = \ x y . x y y
  • 複製：(W f) x = f x x
  • Haskell：join for Monad (r →)
• P = \ x y z w . x (y z) (y w)
  • (P f g) x y = f (g x) (g y)
  • Haskell：on

不動點（fixed-point）組合子

如果想定義下面的遞迴函式 f（注意到下面的定義裡 f 指涉到了自己）：

f x | terminate x = baseCase x
    | otherwise   = recurStep f x

我們可以定義函式 F：

F f x | terminate x = baseCase x
      | otherwise   = recurStep f x

然後用不動點組合子 fix 實現遞迴：

(fix F) x = F (fix F) x
  = baseCase x           -- if terminate x
  = recurStep (fix F) x  -- otherwise

• 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))
  • Turing fixed-point combinator [Alan Turing]
  • Θv = (\ x y . y (\v. x x y v)) (\ x y . y (\v. x x y v))

上面的 Z 跟 Θv 是 Y 跟 Θ 在及早求值語言裡的版本，就不會無止境：

(fix F) x → F (fix F) x → F (F (fix F)) x → ...

編碼

編碼大致上分為 Church 編碼與 Scott 編碼兩大類，對於非遞迴定義的型態來說這兩類編碼除了參數順序以外都相同。

Scott 編碼

假設型態 T 定義如下

data T = C1 X11 X12 … X1m1
       | C2 X21 X22 … X2m2
       …
       | Cn Xn1 Xn2 … Xnmn

（或用 GADT 語法定義）

{-# LANGUAGE GADTSyntax #-}
data T where
  C1 :: X11 -> X12 -> … -> X1m1 -> T
  C2 :: X21 -> X22 -> … -> X2m2 -> T
  …
  Cn :: Xn1 -> Xn2 -> … -> Xnmn -> T

建構子 Cj 編碼成

Cj = \ x1 x2 … xmj . \ c1 c2 … cn . cj x1 x2 … xmj

那麼它的資料本身就能反映模式匹配：

(Cj x1 x2 … xmj) f1 f2 … fn
  = fj x1 x2 … xmj

Church 編碼

與 Scott 編碼不同的是，Church 編碼會自動將應用上的值進一步應用於嵌入建構式的值中。

粗略地說，建構子 Cj 可能會編碼成

Cj = \ x1 x2 … xmj . \ c1 c2 … cn .
  cj (x1 c1 c2 … cn) (x2 c1 c2 … cn) … (xmj c1 c2 … cn)

布林：Bool = True | False

直接 if cond then else = cond then else

True  = \ t f . t
False = \ t f . f

if = I = \ p x y . p x y

not = \ p . p False True
and = \ p q . p q False
or  = \ p q . p True q

自然數

Church 編碼

Zero =       \ f x . x
Succ = \ n . \ f x . f (n f x)

Succⁿ Zero = \ f x . fⁿ x
nest = \ n f x . n f x

add = \ m n . \ f x . m f (n f x)
mul = \ m n . \ f . m (n f)
pow = \ m n . n m
pred = \ n . \ f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)

一元 Scott 編碼：Nat = Zero | Succ Nat

Zero =       \ z s . z
Succ = \ n . \ z s . s n

二元 Scott 編碼：Nat = Ed | B0 Nat | B1 Nat

Ed =       \ e o i . e
B0 = \ n . \ e o i . o n
B1 = \ n . \ e o i . i n

0 = Ed
1 = B1 Ed
2 = B0 (B1 Ed)
3 = B1 (B1 Ed)
4 = B0 (B0 (B1 Ed))

is-zero = \ n . n True (\ _ . False) (\ _ . False)

double = \ n . n 0 (\ _ . B0 n) (\ _ . B0 n)
succ = \ n . n 1 B1 (\ m . B0 (succ m))
pred = \ n . n 0 (\ m . B1 (pred m)) double

nest = \ f x . \ n . n x (nest f² x) (nest f² (f x))
  where f² = \ y . f (f y)

如果我們讓 B0 Ed = Ed，那麼就要改成下面的樣子

is-zero = \ n . n True is-zero (\ m . False)
double = B0

序對

Pair = \ x y . \ f . f x y

fst = \ p . p (\ x y . x)
snd = \ p . p (\ x y . y)
uncurry = \ f p . p f

列表

單序對編碼：(x, xs)

Nil  = False =  \ f . I
Cons = Pair
     = \ x xs . \ f . f x xs

isNil = \ s . s (\ x xs d . False) True
head = fst
tail = snd
list = \ n f s . s (\ x xs d . f x xs) n

機制很酷：

list n g Nil
  = (\ f . I) (\ x xs d . g x xs) n
  = I n
  = n

list n g (Cons y ys)
  = (\ f . f y ys) (\ x xs d . g x xs) n
  = (\ d . g y ys) n
  = g y ys

雙序對編碼：(isNil, (x, xs))

Nil  =          Pair True  True
Cons = \ x xs . Pair False (Pair x xs)

isNil = fst
head = \ s . fst (snd s)
tail = \ s . snd (snd s)
list = \ n f s . fst s n (snd s f)

Scott 編碼：List a = Nil | Cons a (List a)

Nil  =          \ n c . n
Cons = \ x xs . \ n c . c x xs

isNil = \ s . s True (\ x xs . False)
head = \ s . s K   (\ x xs . x)
tail = \ s . s Nil (\ x xs . xs)
list = \ n f s . s n f

foldl = \ f e s . s e (\ x xs . foldl f (f e x) xs)
foldr = \ f e s . s e (\ x xs . f x (foldr f e xs))
map = \ f s . s Nil (\ x xs . Cons (f x) (map f xs))
    = \ f . foldr (\ x ys . Cons (f x) ys) Nil

Church 編碼：右 fold 編碼

列表代表 foldr

Nil  =          \ f e . e
Cons = \ x xs . \ f e . f x (xs f e)

isNil = \ s . s (\ x ys . False) True
head = \ s . s (\ x ys . x) K
tail = \ s . snd (s (\ x p . p (\ xs _ . Pair (Cons x xs) xs)) (Pair Nil Nil))

foldr = \ f e s . s f e
map = \ g s . \ f . s (\ x . f (g x))
    = B (C B) (C B)

上面用到了 map-foldr fusion：

(map g xs) f e
  = foldr f e (map g xs)
  = foldr (B f g) e xs
  = xs (B f g) e

左 fold 編碼

列表代表 foldl

Nil  =          \ f e . e
Cons = \ x xs . \ f e . xs f (f e x) 

isNil = ?
head = ?
tail = ?

foldl = \ f e s . s f e
map = ?