30

以 Haskell 中不起眼的恒等函数为例，

id :: forall a. a -> a

鉴于 Haskell 应该支持隐含的多态性，我应该能够通过类型归属来“限制”id类型似乎是合理的。(forall a. a -> a) -> (forall b. b -> b)但这不起作用：

Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)

<interactive>:1:1:
    Couldn't match expected type `b -> b'
                with actual type `forall a. a -> a'
    Expected type: (forall a. a -> a) -> b -> b
      Actual type: (forall a. a -> a) -> forall a. a -> a
    In the expression: id :: (forall a. a -> a) -> (forall b. b -> b)
    In an equation for `it':
        it = id :: (forall a. a -> a) -> (forall b. b -> b)

当然可以使用所需的签名定义新的受限形式的身份函数：

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId x = x

然而，根据一般定义它是id行不通的：

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId = id -- Similar error to above

那么这里发生了什么？似乎它可能与不可预测性的困难有关，但启用-XImpredicativeTypes没有任何区别。

4

3 回答 3

9

为什么它期待一种(forall a. a -> a) -> b -> b

我认为该类型forall b.(forall a. a -> a) -> b -> b等同于您提供的类型。它只是它的规范表示，其中 forall 尽可能向左移动。

而且它不起作用的原因是给定类型实际上比 id :: forall c 的类型更具多态性。c -> c，它要求参数和返回类型相等。但是你的类型中的 forall a 有效地禁止 a 与任何其他类型统一。

于 2011-10-05T08:25:14.947 回答
2

你是绝对正确的，forall b. (forall a. a -> a) -> b -> b不等于(forall a. a -> a) -> (forall b. b -> b).

除非另有注释，否则类型变量在最外层进行量化。(a -> a) -> b -> b的简写也是如此(forall a. (forall b. (a -> a) -> b -> b))。在 System F 中，类型抽象和应用是明确的，这描述了一个类似f = Λa. Λb. λx:(a -> a). λy:b. x y. 对于不熟悉该表示法的人来说，要清楚的Λ是，lambda 是一个将类型作为参数的 lambda，与λ将术语作为参数不同。

的调用者f首先提供一个类型参数a，然后提供一个类型参数b，然后提供两个值x并y遵守所选类型。需要注意的重要一点是调用者选择a和b。因此，调用者可以执行一个应用程序f String Int length，例如生成一个 term String -> Int。

使用-XRankNTypes您可以通过显式放置全称量词来注释术语，它不必位于最外层。您restrictedId使用类型的术语(forall a. a -> a) -> (forall b. b -> b)可以在 System F 中粗略地举例说明为g = λx:(forall a. a -> a). if (x Int 0, x Char 'd') > (0, 'e') then x else id. 请注意g，被调用者如何应用于x两者0，并'e'首先使用类型对其进行实例化。

但是在这种情况下，调用者不能像以前那样选择类型参数f。您会注意到应用程序x Int和x Charlambda 内部。这会强制调用者提供多态函数，因此 likeg length是无效的，因为length不适用于Intor Char。

另一种思考方式是将f和的类型绘制g为一棵树。树 forf有一个全称量词作为根，而树 forg有一个箭头作为根。为了到达 中的箭头f，调用者实例化了两个量词。使用g，它已经是箭头类型，调用者无法控制实例化。这会强制调用者提供多态参数。

最后，请原谅我做作的例子。Gabriel Scherer 在System F over ML 的中等实际应用中描述了高阶多态性的一些更实际的应用。您还可以查阅 TAPL 的第 23 章和第 30 章，或者浏览编译器扩展的文档，以找到更详细或更好的高级多态性的实际示例。

于 2011-11-30T19:51:50.623 回答
-2

我不是不可预测类型的专家，所以这既是一个潜在的答案，也是尝试从评论中学习一些东西的尝试。

专攻没有意义

\/ a . a -> a                       (1)

至

(\/ a . a -> a) -> (\/ b . b -> b)  (2)

而且我不认为不可预测的类型是允许它的理由。量词通常具有使 (2) 不等价集的左侧和右侧表示的类型的效果。然而a -> ain (1) 暗示左侧和右侧是等价的集合。

例如，您可以将 (2) 具体化为 (int -> int) -> (string -> string)。但是通过任何系统，我知道这不是由 (1) 表示的类型。

错误消息看起来像是 Haskel 类型推断器尝试统一类型的结果id 

\/ a . a -> a

用你给的类型

\/ c . (c -> c) -> \/ d . (d -> d)

在这里，为了清楚起见，我将量化变量统一化。

类型推断器的工作是为 , ,找到一个最一般的赋值a，这会导致两个表达式在语法上相等。最终发现需要统一和. 由于它们是单独量化的，因此它处于死胡同并退出。cdcd

您可能会问这个问题，因为基本类型推断器（带有归属(c -> c) -> (d -> d)）只会向前推进并设置c == d。结果类型将是

(c -> c) -> (c -> c)

这只是简写

\/c . (c -> c) -> (c -> c)

x = x对于wherex被约束为具有相同域和共域的函数 的类型，这可证明是最不通用的类型（类型理论最小上界）表达式。

给定的“restrictedId”类型实际上过于笼统。虽然它永远不会导致运行时类型错误，但您给它的表达式描述了许多类型 - 就像前面提到的那样(int -> int) -> (string -> string)- 即使您的类型允许它们在操作上也是不可能的。

于 2013-09-04T00:29:31.393 回答