序

类型系统在编程语言中是极为重要，不单单是提供一个类型的标注或是方便编译，更多时候是减少出错的可能。当类型系统强大到一定程度，就可以进行所谓的“富类型编程”，比如在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则可以~