将有效的类型赋给let-bound变量时键入错误 [英] Type error when ascribing a valid forall type to a let-bound variable

问题描述

  Prelude>这是一个类型检查器中的错误吗？ let x（forall a。a  - > a）= id in x 3 
 
< interactive>：0：31：
无法匹配期望的类型`forall a。 a  - > a'
，其实际类型为'a0  - > a0'
在表达式中：id 
在模式绑定中：（x :: forall a。a  - > a）= id 
  

以上事实无法检查，但是这种扭曲成功：

 前奏>在x id 
 3 
 中设置（x ::（forall a。a→a）→> Int）=（\\ f→f 3） 

让我认为弱前额转换（请参阅​​这篇论文）可能会有某种关系。将一个 forall 嵌入到一个不能被浮动的逆变位置似乎可以避免这个奇怪的错误。

模式类型签名，它以明显的方式约束模式的类型。现在，在这个例子中，这种约束是否应该在泛化之前或之后发生并不明显，但是我们认为，这个失败的例子表明它在泛化之前就已经被应用了。

更具体地说：在一个let绑定 let x = id in ... 中，会发生什么是 id 的类型 forall a。 a-> a< / code>被实例化为单体型，例如 a0-> a0 ，然后将它分配为 x 的类型，然后将其推广为 forall a0。 a0 - > A0 。如果我认为在泛化之前检查了模式类型签名，它实质上是要求编译器验证单元型 a0 - > a0 比polytype forall a更一般。 a - >如果我们将类型签名移动到绑定级别， let x：，它不是。 ：forall a。 A->一个; x = id in ... 签名在泛化之后被检查（因为为了启用多态递归，这被明确地允许），并且没有类型错误发生。

我认为这是否是一个错误是一个意见。似乎没有一个实际的规范会告诉我们这里的正确行为是什么;只有我们的期望。我建议与GHC人讨论此事。

Is this a bug in the type checker?

Prelude> let (x :: forall a. a -> a) = id in x 3

<interactive>:0:31:
    Couldn't match expected type `forall a. a -> a'
                with actual type `a0 -> a0'
    In the expression: id
    In a pattern binding: (x :: forall a. a -> a) = id

The fact that the above fails to type check, but this contortion succeeds:

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id
3

leads me to think that "weak prenex conversion" (see page 23 of this paper) might be related somehow. Embedding a forall in a contravariant position where it can't be "floated out" seems to keep it safe from this weird error.

解决方案

What I think is happening here is this: In standard Damas–Milner type inference, let bindings are the only place where generalization of a type happens. The type signature that your failing example uses is a pattern type signature which "constrains the type of the pattern in the obvious way". Now, in this example, it is not "obvious" whether this constraining should happen before or after generalization, but your failing example demonstrates, I think, that it gets applied before generalization.

Put more concretely: in a let binding let x = id in ..., what happens is that id's type forall a. a->a gets instantiated into a monotype, say a0 -> a0, which is then assigned as x's type and is then generalized as forall a0. a0 -> a0. If, as I think, the pattern type signature is checked before generalization, it's essentially asking the compiler to verify that the monotype a0 -> a0 is more general than the polytype forall a. a -> a, which it isn't.

If we move the type signature to the binding level, let x :: forall a. a-> a; x = id in ... the signature is checked after generalization (since this is expressedly allowed in order to enable polymorphic recursion), and no type error ensues.

Whether it is a bug or not is, I think, a matter of opinion. There doesn't seem to be an actual spec that would tell us what the right behaviour here is; there's only our expectations. I would suggest discussing the matter with the GHC people.

这篇关于将有效的类型赋给let-bound变量时键入错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！