序

類型系統(tǒng)在編程語(yǔ)言中是極為重要，不單單是提供一個(gè)類型的標(biāo)注或是方便編譯，更多時(shí)候是減少出錯(cuò)的可能。當(dāng)類型系統(tǒng)強(qiáng)大到一定程度，就可以進(jìn)行所謂的“富類型編程”，比如在Haskell中只要編譯器不報(bào)錯(cuò)，大致上程序也是沒(méi)什么bug的。在常用的靜態(tài)類型語(yǔ)言中，C++/java/C#等，雖然在新標(biāo)準(zhǔn)與新版本中支持類型的自動(dòng)推導(dǎo)，但是對(duì)類型系統(tǒng)及其推導(dǎo)還是缺少更為直接的支持。

很多常用語(yǔ)言的類型系統(tǒng)都是圖靈完全的，比如C++，Scala，Haskell，Qi/Shen（一種Lisp方言），比如C++和Scala為什么是圖靈完全是很好理解的，它們依賴的是類型的模式匹配，C++中則對(duì)應(yīng)特化與偏特化，Scala可以使用類型的繼承關(guān)系等等。

既然是非專業(yè)研究，下面就用非專業(yè)手段論證有些類型系統(tǒng)的Turing Complete。

引

“程序就是類型的證明”

這句話結(jié)合Curry-Howard同構(gòu)揭露出來(lái)的東西是很深刻的。下表是一部分的對(duì)應(yīng)關(guān)系：

注：表格中倒數(shù)第二行call/cc (call with current continuation) ((α → β) → α) → α所代表的排中律，在簡(jiǎn)單類型lambda演算中是類型不居留的，這也是為什么用傳說(shuō)中的Lisp七大公理無(wú)法做出call/cc來(lái)的另一個(gè)角度的原因。

類型與推理系統(tǒng)則是與形式化語(yǔ)言最為接近的地方。類型系統(tǒng)從不同的角度可以分為很多種，靜態(tài)/動(dòng)態(tài)，強(qiáng)/弱，子類型類型系統(tǒng)，Duck Type，Dependent types，Union types等等。從類型推導(dǎo)的角度上，又有System F，HM類型系統(tǒng)等等。在Curry Howard同構(gòu)的意義上來(lái)說(shuō)，程序語(yǔ)言的語(yǔ)言構(gòu)造同構(gòu)為推理系統(tǒng)的推理規(guī)則，例如System F代表的二階直覺(jué)邏輯等等。

以著名的S組合子：S = λx. λy. λz. xz(yz)作為例子
它的類型是 (α → β → γ) → (α → β) → α ，對(duì)它的證明可以移步 wiki 。

正文

說(shuō)到圖靈完全，大家一定不陌生，我們每天都在用圖靈完全的語(yǔ)言來(lái)做各種事情（不是所有的語(yǔ)言都是圖靈完全的，比如HTML，正則）。而類型系統(tǒng)的圖靈完全，可以粗略的認(rèn)為是在Type Checker和Type Inference上可以理論做到所有的事情（不論寫起來(lái)丑不丑！）。

Qi/Shen

Qi語(yǔ)言是Shen語(yǔ)言的前身，屬于Lisp的方言，可以看成是擴(kuò)展了靜態(tài)類型系統(tǒng)與內(nèi)置Prolog、Patten Match、自定義求值策略等多個(gè)功能的CLisp擴(kuò)展。它的類型系統(tǒng)的顯著特點(diǎn)是采用了Dependent Type System，正如其字面意思，我們來(lái)看一個(gè)例子

(datatype t
 Name : String;
 Telephone : String;
 ====== 
[Name Telephone] : t;
 ) 

（注：其中 =====這個(gè)東西是個(gè)語(yǔ)法糖，是

(datatype t
 Name : String; 
Telephone : String;
 ---------- 
[Name Telephone] : t; ) 

與

(datatype t
 Name : String,
 Telephone : String; >> P 
--------- 
[Name Telephone] : t >> P ) 

的合寫。）

如果熟悉Sequent calculus的話，上面的寫法簡(jiǎn)直就是對(duì)著公式畫下來(lái)的~而且在上面類型定義的condition line中還支持if (element? X [0 1]這種寫法。

Sequent calculus是圖靈完全的，Qi/Shen的Type System基于Sequent calculus，自然也是圖靈完全的。

Haskell

Haskell的類型系統(tǒng)屬于著名的Hindley–Milner type system，是基于lambda演算與參數(shù)多態(tài)(parametric polymorphism)的經(jīng)典類型系統(tǒng)，當(dāng)然Haskell的不同版本在上面都有不同的類型系統(tǒng)擴(kuò)展。
下面就是這篇文章中比較好玩的地方，如何利用SK Combinator來(lái)論證Haskell類型系統(tǒng)的圖靈完全性。

與Qi/Shen語(yǔ)言不一樣，Haskell的類型推導(dǎo)規(guī)則是基于對(duì)謂詞(Predicate)的演繹求解，下面的內(nèi)容利用Haskell的Type Checker做出SK Combinator。為了做成不對(duì)應(yīng)實(shí)現(xiàn)的函數(shù)聲明，我們使用undefined與-fallow-undecidable-instances的ghc選項(xiàng)。
首先，先定義基本的SK Combinator的term和Application：

data K0 data S0 data App x y data Other a 

接下來(lái)聲明一個(gè)用來(lái)歸約結(jié)果的歸約函數(shù)的class和Instance：

 
data Done 
data More
class CombineDone d1 d2 d | d1 d2 -> d 
instance CombineDone Done Done Done 
instance CombineDone Done More More 
instance CombineDone More Done More 
instance CombineDone More More More

當(dāng)然還得聲明一個(gè)真正用來(lái)歸約term的歸約函數(shù)：

class Eval1 x y d | x -> y d 

然后在Instance中寫入歸約的規(guī)則：

instance Eval1 S0        S0         Done 
instance Eval1 K0        K0         Done 
instance Eval1 (Other a) (Other a)  Done  
instance Eval1 x x' d => Eval1 (App K0 x) (App K0 x') d 
instance Eval1 x x' d => Eval1 (App S0 x) (App S0 x') d 
instance ( Eval1 x x' d1
          , Eval1 y y' d2
          , CombineDone d1 d2 d
          ) => Eval1 (App (App S0 x) y) (App (App S0 x') y') d 
instance Eval1 x x' d => Eval1 (App (Other a) x) (App (Other a) x') d
 instance ( Eval1 x x' d1
          , Eval1 y y' d2
          , CombineDone d1 d2 d
          ) => Eval1 (App (App (Other a) x ) y )
                     (App (App (Other a) x') y') d 
instance ( Eval1 x x' d1
          , Eval1 y y' d2
          , Eval1 z z' d3
          , CombineDone d1 d2 d4
          , CombineDone d3 d4 d
          ) => Eval1 (App (App (App (Other a) x ) y ) z )
                     (App (App (App (Other a) x') y') z') d 

下面這是真正的S和K的定義：
S Combinator :   λx. λy. λz. xz(yz)

instance Eval1 (App (App (App S0 f) g) x)             (App (App f x) (App g x))             More 

K Combinator :   λx. λy. x

instance Eval1 (App (App K0 x) y)         x     More instance Eval1 (App (App (App K0 x) y) z) (App x z) More 

光有這些特化的規(guī)則還不夠，再加上不能被上述rules歸約的情景處理：

instance ( Eval1 (App (App (App p q) x) y)  a d )
                       => Eval1 (App (App (App (App p q) x) y) z) (App a z)  d 

再添加一些輔助的類型

class EvalAux x y q1 | x q1 -> y
 instance EvalAux x x Done 
instance (     Eval1   x y q
          ,    EvalAux y z q
          ) => EvalAux x z More  
class Eval x y | x -> y 
instance EvalAux x y More => Eval x y 

做到這里，我們已經(jīng)得到了一個(gè)可以直接表示 X -> Y計(jì)算的類型了，光有類型聲明是跑不起來(lái)的，最后輔上dummy types與undefined的method：

data P0 
data Q0 
data R0  
type P = Other P0 
type Q = Other Q0 
type R = Other R0  
eval1 :: Eval1 x y q => x -> y 
eval1 = undefined  
eval :: Eval x y => x -> y 
eval = undefined  
bot :: a bot = undefined 

這樣就可以做出最基本的例子：

type K x y   = App (App K0 x) y
type S f g x = App (App (App S0 f) g) x  
testK = eval (bot :: K P Q)   :: P 
testS = eval (bot :: S P Q R) :: App (App P R) (App Q R) 

這樣！高洋上的SK Combinator就做成來(lái)了，它在類型推導(dǎo)上已經(jīng)可以正確的歸約，接下來(lái)，你就可以造出整個(gè)世界了。

延伸

研究函數(shù)式編程與類型系統(tǒng)是很有意思的事情，不像很多常用的語(yǔ)言，總有一些“王八的屁股--規(guī)定”，比如Python莫名其妙的Scoping問(wèn)題，js莫名其妙的運(yùn)算結(jié)果等等。而正兒八經(jīng)設(shè)計(jì)出來(lái)的函數(shù)式語(yǔ)言大多數(shù)特性都是對(duì)其設(shè)計(jì)思路的延伸，F(xiàn)-algebras，F(xiàn)ix Point，F(xiàn)ree Monad，F(xiàn)oldable&Traversable等等，不僅僅是一種編程技巧，也代表了另一個(gè)方向上的Program Pattarn。

Haskell和Ocaml都是基于Hindley-Milner系統(tǒng)，但也都對(duì)類型系統(tǒng)打上了各式各樣的補(bǔ)丁，對(duì)程序?qū)懛ǖ闹С殖潭纫彩歉魇礁鳂印?/p>

例如，Haskell不能處理遞歸的定義，就比如\x -> x x，haskell是不支持的，因?yàn)樵谀涿瘮?shù)類型推斷上屬于簡(jiǎn)單類型的lambda演算，不額外引入μ算符的話是無(wú)法處理的。這樣，眾所周知的Y Combinator就只能寫成：

newtype Mu a = Mu (Mu a -> a) 
y :: (a -> a) -> a 
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x) 

（注：可詳見(jiàn)我的 另一篇博文）

Ocaml則有補(bǔ)丁應(yīng)對(duì)這種情景，加上了as語(yǔ)義，類型將被識(shí)別為（a -> a as a) -> a。

對(duì)于這段代碼：

data Sum a b = LeftSum a 
                       | RightSum b   
lengthxs list = case list of
                       LeftSum [] -> 0
                       RightSum (x:xs) -> 1 + lengthxs xs  

Haskell無(wú)法通過(guò)編譯，Ocaml則可以~