序

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

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

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

引

“程序就是類型的證明”

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

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

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

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

正文

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

Qi/Shen

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

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

（注：其中 =====這個東西是個語法糖，是

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

與

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

的合寫。）

如果熟悉Sequent calculus的話，上面的寫法簡直就是對著公式畫下來的~而且在上面類型定義的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)，當然Haskell的不同版本在上面都有不同的類型系統(tǒng)擴展。
下面就是這篇文章中比較好玩的地方，如何利用SK Combinator來論證Haskell類型系統(tǒng)的圖靈完全性。

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

data K0 data S0 data App x y data Other a 

接下來聲明一個用來歸約結(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

當然還得聲明一個真正用來歸約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)得到了一個可以直接表示 X -> Y計算的類型了，光有類型聲明是跑不起來的，最后輔上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就做成來了，它在類型推導上已經(jīng)可以正確的歸約，接下來，你就可以造出整個世界了。

延伸

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

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

例如，Haskell不能處理遞歸的定義，就比如\x -> x x，haskell是不支持的，因為在匿名函數(shù)類型推斷上屬于簡單類型的lambda演算，不額外引入μ算符的話是無法處理的。這樣，眾所周知的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) 

（注：可詳見我的 另一篇博文）

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

對于這段代碼：

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

Haskell無法通過編譯，Ocaml則可以~