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

Question

考虑这个组合子:

S (S K)

将其应用于参数XY:

S (S K) X Y

它签订合同:

X Y

我将S(SK)转换为相应的Lambda术语并得到了这个结果:

(\x y -> x y)

我使用Haskell WinGHCi工具获取(\ xy - > xy)的类型签名,并返回:

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

这对我来说很有意义.

接下来,我使用WinGHCi获取s(sk)的类型签名并返回:

((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)类型是从其组成子表达式的类型派生而来,而不是从它对其参数的影响.因此,它具有比表示效果的lambda表达式更少的通用类型s (s k).

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我们已经确定其参数为xtype 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。

• ghasx作为其参数，我们已经确定其类型为(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. 我们看到sin(s k)被约束为与 的类型签名一致k，并且第一个sins (s k)被约束为与 的类型签名一致(s k)。因此， 的类型签名s (s k)因其参数而受到限制。即使 和p具有相同的定义，但对和 的s (s k)约束是不同的。gx