如何输入简单类型的lambda演算术语(SKK)

Question

我试图实现一个简单类型的lambda演算类型检查器.运行完整性测试时,我尝试输入(SKK),我的类型检查器抛出此错误:

TypeMismatch {firstType = t -> t, secondType = t -> t -> t}

违规术语显然是(SKK)

(\x:t -> t -> t.\y:t -> t.\z:t.x z (y z)) (\x:t.\y:t.x) (\\x:t.\y:t.x)

我认为问题源于缺乏多态性,因为当我输入检查这个haskell代码时它工作正常:

k x y = x
s x y z = x z (y z)
test = s k k -- type checks

但如果我专注于这种类型:

k :: () -> () -> ()
k x y = x
s :: (() -> () -> ()) -> (() -> ()) -> () -> ()
s x y z = x z (y z)
test = s k k -- doesn't type check 

仅供参考,我的类型系统很简单:

data Type = T | TArr Type Type

完整的来源

Answer 1

我将窃取我之前的答案中的想法,以展示如何向你提出问题.但首先我要稍微重新阐述你的问题.

在Haskell,我们有

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: a -> b -> a

我们想问的问题是"在类型检查后这些类型是什么样的s k k？".更重要的是,如果我们用不同的统一变量重写它们,

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: d -> e -> d
k :: f -> g -> f
s k k :: h

那么这个问题就变成了统一问题:我们试图统一s它所使用的类型 - 即(d -> e -> d) -> (f -> g -> f) -> h.现在我们手头有一个统一问题,我们可以用我的其他答案中显示的格式询问:

> :{
| :t undefined
| ::   ((a -> b -> c) -> (a -> b) -> (a -> c))
|    ~ ((d -> e -> d) -> (f -> g -> f) -> h)
| => (a, b, c, d, e, f, g, h)
| :}
undefined
::   ((a -> b -> c) -> (a -> b) -> (a -> c))
   ~ ((d -> e -> d) -> (f -> g -> f) -> h)
=> (a, b, c, d, e, f, g, h)
  :: (f, g -> f, f, f, g -> f, f, g, f -> f)

现在我们可以看到为什么你的版本不起作用:在你的版本中,你已经将所有多态变量实例化为基类型T; 但是,因为b ~ g -> f,e ~ g -> f并且h ~ f -> f显然是箭头类型,这肯定是行不通的!但是,如果我们尊重上述替代,任何选择f和g将会奏效; 特别是如果我们选择f ~ T和g ~ T,那么我们有

s :: (T -> (T -> T) -> T) -> (T -> (T -> T)) -> (T -> T)
k1 :: T -> (T -> T) -> T
k2 :: T -> T -> T
s k1 k2 :: T -> T