组合器的类型签名与其等效 Lambda 函数的类型签名不匹配

Question

考虑这个组合器：

S (S K)

将其应用于参数 X Y：

S (S K) X Y

它的合同是：

X Y

我将 S (S K) 转换为对应的 Lambda 项，得到了这样的结果：

(\x y -> x y)

我使用 Haskell WinGHCi 工具获取 (\x y -> x y) 的类型签名并返回：

(t1 -> t) -> t1 -> t

这对我来说很有意义。

接下来，我使用 WinGHCi 来获取 s (s k) 的类型签名并返回：

((t -> t1) -> t) -> (t -> t1) -> t

这对我来说没有意义。为什么类型签名不同？

注意：我将 s、k 和 i 定义为：

s = (\f g x -> f x (g x))
k = (\a x -> a)
i = (\f -> f)

Answer 1

我们从k和s的类型开始

k :: t1 -> t2 -> t1
k = (\a x -> a)

s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5
s = (\f g x -> f x (g x))

所以将k作为s的第一个参数传递，我们将k的类型与s的第一个参数的类型统一起来，在类型上使用s

s :: (t1 -> t2 -> t1) -> (t1 -> t2) -> t1 -> t1

因此我们得到

s k :: (t1 -> t2) -> t1 -> t1
s k = (\g x -> k x (g x)) = (\g x -> x)

那么在s (s k)中，外层s用在类型(t3 = t1 -> t2,t4 = t5 = t1)

s :: ((t1 -> t2) -> t1 -> t1) -> ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

将其应用于s k 会删除第一个参数的类型并留给我们

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

总结一下：在 Haskell 中，s (s k) 的类型源自其组成子表达式的类型，而不是其对其参数的影响。因此，它的类型不如表示s (s k) 效果的 lambda 表达式。

Answer 2

您使用的类型系统与简单类型的 lambda 演算基本相同（您没有使用任何递归函数或递归类型）。简单类型的 lambda 演算并不完全通用。它不是图灵完备的，不能用于编写一般递归。 SKI 组合子演算是图灵完备的，可用于编写定点组合子和一般递归；因此，SKI 组合子演算的全部力量不能用简单类型的 lambda 演算来表达（尽管它可以用无类型的 lambda 演算）。

Answer 3

感谢所有回答我问题的人。我研究了你的回答。为了确保我理解我所学到的东西，我已经写了我自己对我的问题的答案。如果我的回答不正确，请告诉我。

我们从k和s的类型开始：

   k  :: t1 -> t2 -> t1 
   k  =  (\a x -> a) 

   s  :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
   s  =  (\f g x -> f x (g x)) 

让我们首先确定(s k)的类型签名。

回忆s的定义：

s = (\f g x -> f x (g x))

将k 替换为f 会导致(\f g x -> f x (g x)) 与：

(\g x -> k x (g x))

重要 g和x的类型必须与k的类型签名一致。

回想一下k 有这个类型签名：

   k :: t1 -> t2 -> t1

所以，对于这个函数定义k x (g x)我们可以推断：

• x的类型是k的第一个参数的类型，也就是t1的类型。

• k的第二个参数的类型是t2，所以(g x)的结果一定是t2。

• g 具有 x 作为其参数，我们已经确定其类型为 t1。所以(g x)的类型签名是(t1 -> t2)。

• k的结果类型是t1，所以(s k)的结​​果是t1。

所以，(\g x -> k x (g x)) 的类型签名是这样的：

   (t1 -> t2) -> t1 -> t1

接下来，k 被定义为始终返回其第一个参数。所以这个：

k x (g x)

与此签订合同：

x

还有这个：

(\g x -> k x (g x))

与此签订合同：

(\g x -> x)

好的，现在我们已经弄清楚了(s k)：

   s k  :: (t1 -> t2) -> t1 -> t1 
   s k  =  (\g x -> x)

现在让我们确定s (s k) 的类型签名。

我们以同样的方式进行。

回忆s的定义：

s = (\f g x -> f x (g x))

将(s k) 替换为f 会导致(\f g x -> f x (g x)) 与：

(\g x -> (s k) x (g x))

重要g和x的类型必须与(s k)的类型签名一致。

回想一下(s k) 有这个类型签名：

   s k :: (t1 -> t2) -> t1 -> t1

所以，对于这个函数定义(s k) x (g x)我们可以推断：

• x的类型是(s k)的第一个参数的类型，也就是(t1 -> t2)的类型。

• (s k)的第二个参数的类型是t1，所以(g x)的结果一定是t1。

• g 有x 作为它的参数，我们已经确定它的类型是(t1 -> t2)。 所以(g x)的类型签名是((t1 -> t2) -> t1)。

• (s k)的结果类型是t1，所以s (s k)的结果是t1。

所以，(\g x -> (s k) x (g x)) 的类型签名是这样的：

   ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

之前我们确定s k 有这个定义：

   (\g x -> x)

也就是说，它是一个接受两个参数并返回第二个参数的函数。

因此，这个：

   (s k) x (g x)

对此的合同：

   (g x)

还有这个：

   (\g x -> (s k) x (g x))

与此签订合同：

   (\g x -> g x)

好的，现在我们找到了s (s k)。

   s (s k)  :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 
   s (s k)  =  (\g x -> g x)

最后，比较s (s k)的类型签名和这个函数的类型签名：

   p = (\g x -> g x)

p 的类型是：

   p :: (t1 -> t) -> t1 -> t

p 和 s (s k) 具有相同的定义 (\g x -> g x) 那么为什么它们有不同的类型签名呢？

s (s k) 与p 具有不同类型签名的原因是p 没有约束。我们看到(s k) 中的s 被约束为与k 的类型签名一致，而s (s k) 中的第一个s 被约束为与(s k) 的类型签名一致。因此，s (s k) 的类型签名因其参数而受到限制。尽管p 和s (s k) 具有相同的定义，但g 和x 的约束不同。