如何键入简单键入的λ微积分项（S K K）

Question

冒犯性的术语显然是（S K K）

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

我认为问题产生于多态性的缺乏，因为当我键入check这个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 

Answer 1

我将从我以前的回答中偷取想法来展示如何问ghci你的问题。但首先我要稍微修改一下你的问题。

在哈斯克尔，我们有

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

我们想问的问题是“这些类型在类型检查s kk之后是什么样子？”更重要的是，如果我们用不同的统一变量重写它们，

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: d -> e -> d
k :: f -> g -> f
s k k :: 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)

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