### 引

“程序就是类型的证明”

logic side　　program side
Hilbert-style deduction system　type system for combinatory logic
natural deduction　type system for lambda calculus
hypotheses　　free variables
deduction theorem　　abstraction elimination
．．．　　．．．
Peirce's law　　cal/cc
double-negation translation　　CPS translation

### 正文

#### 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是图灵完全的，Qi/Shen的Type System基于Sequent calculus，自然也是图灵完全的。

``data K0 data S0 data App x y data Other a ``

`` data Done data Moreclass 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``

``class Eval1 x y d | x -> y d ``

``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 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 ``

``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 ``

``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) ytype 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) ``

### 延伸

``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  ``