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)
  • 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ΘvYΘ 在及早求值語言裡的版本,就不會無止境:

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

編碼

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

Scott 編碼

假設型態 T 定義如下

data T = C1 X11 X12X1m1
       | C2 X21 X22X2m2| Cn Xn1 Xn2Xnmn

(或用 GADT 語法定義)

{-# LANGUAGE GADTSyntax #-}
data T where
  C1 :: X11 -> X12 ->-> X1m1 -> T
  C2 :: X21 -> X22 ->-> X2m2 -> TCn :: 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 = ?