haskell - 类型良好的函数的 eta 减少如何导致类型错误？

Question

我在玩 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-reduce get至

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 中的错误/限制还是更高级别类型的一些基本问题？

Answer 1

我想说原因不在于 η 减少本身，问题在于 RankNTypes你输了principal types和类型推断。

高阶类型推断的问题在于推断 λ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 类型。