5

考虑这个组合器：

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)
4

3 回答 3

9

我们从类型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统一，并使用at 类型kss

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 中， ofs (s k)的类型是从其组成子表达式的类型派生的，而不是从其对其参数的影响中派生的。因此，它的类型比表示s (s k).

于 2012-03-06T21:33:30.777 回答
7

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

于 2012-03-07T01:10:07.977 回答
2

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

我们从 和 的类型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第一个参数的类型，即 type t1。

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

  • ghasx作为我们已经确定的参数，它具有 type 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)第一个参数的类型，即 type (t1 -> t2)。

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

  • ghasx作为它的参数，我们已经确定它有 type (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，而 first sins (s k)被约束为与 的类型签名一致(s k)。因此， 的类型签名s (s k)由于其参数而受到限制。尽管p和s (s k)具有相同的定义，但约束g和x不同。

于 2012-03-10T20:12:52.510 回答