序

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

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

既然是非專業研究，下面就用非專業手段論證有些類型系統的Turing Complete。

引

“程序就是類型的證明”

這句話結合Curry-Howard同構揭露出來的東西是很深刻的。下表是一部分的對應關系：

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

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

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

正文

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

Qi/Shen

Qi語言是Shen語言的前身，屬于Lisp的方言，可以看成是擴展了靜態類型系統與內置Prolog、Patten Match、自定義求值策略等多個功能的CLisp擴展。它的類型系統的顯著特點是采用了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的類型系統屬于著名的Hindley–Milner type system，是基于lambda演算與參數多態(parametric polymorphism)的經典類型系統，當然Haskell的不同版本在上面都有不同的類型系統擴展。
下面就是這篇文章中比較好玩的地方，如何利用SK Combinator來論證Haskell類型系統的圖靈完全性。

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

data K0 data S0 data App x y data Other a 

接下來聲明一個用來歸約結果的歸約函數的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的歸約函數：

class Eval1 x y d | x -> y d 

然后在Instance中寫入歸約的規則：

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 

光有這些特化的規則還不夠，再加上不能被上述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 

做到這里，我們已經得到了一個可以直接表示 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就做成來了，它在類型推導上已經可以正確的歸約，接下來，你就可以造出整個世界了。

延伸

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

Haskell和Ocaml都是基于Hindley-Milner系統，但也都對類型系統打上了各式各樣的補丁，對程序寫法的支持程度也是各式各樣。

例如，Haskell不能處理遞歸的定義，就比如\x -> x x，haskell是不支持的，因為在匿名函數類型推斷上屬于簡單類型的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則有補丁應對這種情景，加上了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則可以~