# Lambda encoding

## 組合子 combinator
- 恆等 `I x = x`
- lambda：`I = \ x . x`
- SKI：`I = S K K`
- Haskell：`id`
- 常數 `K x y = x`
- lambda：`K = \ x y . x`
- Haskell：`const`, `pure` for Applicative `(r →)`
- 融合 `(S f g) x = (f x) (g x)`
- lambda：`S = \ x y z . x z (y z)`
- Haskell：`(<*>)` for Applicative `(r →)`
- [Why is the `S` combinator an S?](https://blog.plover.com/math/combinator-s.html)
- 合成 `(B f g) x = f (g x)`
- lambda：`B = \ x y z . x (y z)`
- SKI：`B = S (K S) K`
- Haskell：`(.)`、`fmap` for Functor `(r →)`
- 交換 `(C f) x y = f y x`
- lambda：`C = \ x y z . x z y`
- SKI：`C = S (S (K K) S) (K K)`
- Haskell：`flip`
- 複製 `(W f) x = f x x`
- lambda：`W = \ x y . x y y`
- SKI：`W = S S (K I)`
- Haskell：`join` for Monad `(r →)`
- `(P f g) x y = f (g x) (g y)`
- lambda：`P = \ x y z w . x (y z) (y w)`
- SKI：`P = ?`
- 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

#### biFold

biFold = \ f g e s .
  s (\ x b k h p . p (b (\ _ . G x) (F x) (K I))
                     (h x (b (K e) # K))
    (\ k h p . k _)
    (K e) # K

上面的 `#` 可以是任何東西，但若要型態正確的話可改成 `\ _ _ . e`。這能夠實現類似以下的功能：

biFold :: (a -> a -> b -> b) -> (a -> b) -> b -> [a] -> b
biFold f g e []       = e
biFold f g e [x]      = g x
biFold f g e (x:y:xs) = f x y (biFold f g e xs)