lambda演算與數據類型
在大多數編程語言裡面，數據類型和函數都是不同的，但它們又有種種關聯。我們可以說函數是一種數據類型，換句話說就是first class function。通過pattern match我們可以拿到ADT（代數數據類型）的各個constructor的argument。再用Idris舉個例子：
data Maybe : (a : Type) -> Type where Nothing : Maybe a Just : (x : a) -> Maybe a
我們定義了2個函數：Nothing和Just，這兩個function都用於構造數據類型Maybe，所以他們的返回值的類型是Maybe，我們把這兩個函數稱之為constructor。
前置知識
- 對函數式編程及相關編程語言的了解
- 對Lambda演算的基本知識
- ADT（代數數據類型）的基本知識
數據類型與函數
在lambda calculus中，一切都是函數。我們通過：variable、abstraction、application來組成lambda的term。一般通過對lambda term應用normal order reduction來對lambda term進行求值。
既然函數可以是一種數據類型，數據類型可不可以用函數來表示呢？當然可以。例如在lambda演算中通常表示自然數的方式，或者說church number則是：
zero := λf.λx.x;succ := λn.λf.λx.f (n f x);
如果不熟悉church encoding的自然數可以在維基百科中了解：
https://en.wikipedia.org/wiki/Lambda_calculus我們有多種方式將數據類型encode到lambda calculus中，如church number：
0 := λf.λx.x;1 := λf.λx.f x;2 := λf.λx.f (f x);
則是通過將參數f遞歸的應用在x上來encode自然數的。
而peano number，或者也可以說是scott encoding的自然數：
zero := λz.λs.z;succ := λn.λz.λs.s n;0 := λz.λs.z;1 := λz.λs.s (λz.λs.z);2 := λz.λs.s (λz.λs.s (λz.λs.z));
則是將數據類型的constructor定義出來，並encode每個constructor的pattern match函數。
數據類型的表示
我們可以通過將數據類型相關的一種operator進行encode，來將數據類型表示到lambda calculus中。例如上文自然數的例子，Church encoding是將」遞歸的把函數f應用n次到x上(f^n)「這種operator進行encode。Scott encoding則是將pattern match這種operator進行encoding。
一個operator就是一個函數，在Church encoding的自然數中，遞歸的把函數f應用n次到x上的function是trivial的，而pattern match則不是：
funcPow := λf.λx.λn.n f x;matchNat := λz.λs.λn.n (λm.m (λu.λg.g (λf.λx.x)) (λg.λu.λh.h (λf.λx.f (g f x)))) (λx.λu.x) z s;
而用Scott encoding的peano number中，pattern match是trivial的，而funcPow則不是：
funcPow := λf.λx.λn.n x ((λg.(λy.g (y y)) (λy.g (y y))) (λg.λh.f (h x g)));matchNat := λz.λs.λn.n z s;
不單單是自然數，其他數據類型也可以用類似的方法進行encode。例如對於List，我們可以將其按fold right進行encode，或者按pattern match進行encode等。
Scott encoding
在上文中多次提到了scott encoding、pattern match這兩個名詞。具體來說，對於ADT（也就是有多個constructor，每個constructor有任意argument，或者說product的sum）來說，可能最簡單、最直觀的encode數據類型的方法就是將pattern match進行encode了，scott encoding就是指的這種encode數據類型的方法。
具體對於有n個constructor的ADT，對於第x個constructor，有m個argument，用如下方法進行encode：
CtorX := λA_1 A_2 ... A_m.λC_1 C_2 ... C_n.C_x A_1 A_2 ... A_m;
這樣就可以對直觀的對不同的case進行pattern match了。
Encoding of list
上文中提到過對list進行encode的2種方法，關於其他的encode方法，可以參考維基百科：
https://en.wikipedia.org/wiki/Church_encoding#List_encodings
這裡我們使用Scott encoding來encode list，定義list(pattern match)、nil(constructor)、cons(constructor)、length、null、append、foldr、foldl函數：
list := λn.λc.λl.l n c;nil := λn.λc.n;cons := λh.λt.λn.λc.c h t;length := λl.l zero (λh.λt.succ (length t));null := λl.l true (λh.λt.false);append := λl.λm.l m (λh.λt.cons h (append t m));foldr := λf.λx.λl.l x (λh.λt.f h (foldr f x t));foldl := λf.λx.λl.l x (λh.λt.foldl f (f x h) t);
每個函數的定義都比較直觀，就不詳細描述了。對於引用了其他函數的情況可以直接代換，也可以將其當作free variable，並使用abstraction將其捕獲，通過application傳入其定義，例如對於null：
null := (λtrue.λfalse.λl.l true (λh.λt.false)) (λt.λf.t) (λt.λf.f);
需要注意的是length、append、foldr、foldl都在定義中引用了自身，也就是使用了遞歸。對於這種情況，需要使用不動點運算元：
fix := λf.(λx.f (x x)) (λx.f (x x));
將其轉化為：
length := fix (λlength.λl.l zero (λh.λt.succ (length t)));append := fix (λappend.λl.λm.l m (λh.λt.cons h (append t m)));foldr := fix (λfoldr.λf.λx.λl.l x (λh.λt.f h (foldr f x t)));foldl := fix (λfoldl.λf.λx.λl.l x (λh.λt.foldl f (f x h) t));
總結
本文介紹了如何在lambda calculus中處理數據類型，和各種encoding之間的關係。
這裡打個廣告，寫這篇文章的起因是最近在用scala寫一個個人項目，lambda calculus的REPL。在設計標準庫的時候涉及到了一些與本文相關的知識。已經實現了tokenizer、parser、beta reducer、eta converter、pretty printer等模塊，單純調用API來處理lambda term是沒有問題了。目前正在設計核心的REPL的Extension API、library的dependencies管理、lam文件（library的源文件）的語法、標準庫等。如果有興趣參與開發，歡迎聯繫我！
https://github.com/yuxuanchiadm/lamcalcj
參考
Lambda calculus
Church encoding
Mogensen–Scott encoding
推薦閱讀：