16

我在玩 van Laarhoven 镜头时遇到了一个问题，即类型检查器拒绝了良好类型函数的 eta 缩减形式：

{-# LANGUAGE RankNTypes #-}

import Control.Applicative

type Lens c a = forall f . Functor f => (a -> f a) -> (c -> f c)

getWith :: (a -> b) -> ((a -> Const b a) -> (c -> Const b c)) -> (c -> b)
getWith f l = getConst . l (Const . f)

get :: Lens c a -> c -> a
get lens = getWith id lens

上述类型检查，但如果我 eta-reduceget到

get :: Lens c a -> c -> a
get = getWith id

然后 GHC (7.4.2) 抱怨说

Couldn't match expected type `Lens c a'
            with actual type `(a0 -> Const b0 a0) -> c0 -> Const b0 c0'
Expected type: Lens c a -> c -> a
  Actual type: ((a0 -> Const b0 a0) -> c0 -> Const b0 c0)
               -> c0 -> b0
In the return type of a call of `getWith'
In the expression: getWith id

我可以理解，如果函数没有明确的类型签名，那么 eta-reduction 与单态限制相结合可能会混淆类型推断，尤其是当我们处理更高级别的类型时，但在这种情况下我不是确定发生了什么。

是什么导致 GHC 拒绝 eta-reduced 形式，这是 GHC 中的错误/限制还是更高级别类型的一些基本问题？

4

2 回答 2

12

我想说原因不在于 η-reduction 本身，问题在于RankNTypes您失去了主要类型和类型推断。

具有高阶等级的类型推断的问题是在推断类型时λx.M遵守规则

     Γ, x:σ |- M:ρ
----------------------
  Γ |- λx:σ.M : σ→ρ

我们不知道应该选择什么类型的 σ x。在 Hindley-Milner 类型系统的情况下，我们将自己限制为无类型量词的类型，x并且推断是可能的，但不适用于任意排序的类型。

因此，即使使用RankNTypes，当编译器遇到没有明确类型信息的术语时，它也会求助于 Hindley-Milner 并推断其 rank-1 主要类型。但是，在您的情况下，您需要的类型getWith id是 rank-2，因此编译器无法自行推断。

你的明确案例

get lens = getWith id lens

对应于类型x已经明确给出的情况λ(x:σ).Mx。编译器lens在类型检查之前知道 的类型getWith id lens。

在减少的情况下

get = getWith id

编译器必须自己推断类型getWidth id，因此它坚持使用 Hindley-Milner 并推断不适当的 rank-1 类型。

于 2013-05-06T20:11:19.423 回答
5

实际上这很简单：GHC 推断每个表达式的类型，然后开始将它们统一起来=。当周围只有 rank-1 类型时，这总是很好的，因为选择了最多态的类型（这是明确定义的）；所以任何可能的统一都会成功。

但即使有可能，它也不会选择更一般的 rank-2 类型，因此getWith id推断为 is((a -> Const a a) -> c -> Const a c) -> (c -> a)而不是(forall f . Functor f => (a -> f a) -> c -> f c) -> (c -> a)。我想如果 GHC 确实做了这样的事情，传统的 rank-1 类型推断将不再适用。或者它永远不会终止，因为不存在一种定义明确的最多态的 rank-n 类型。

这并不能解释为什么它不能从get的签名中看出它需要在这里选择 rank-2，但大概也有一个很好的理由。

于 2013-05-06T16:46:26.963 回答