如何通过减少良好类型的函数来减少类型错误？

我正在玩van Laarhoven镜头并遇到一个问题,其中类型检查器拒绝了et-reduced形式的良好类型的功能:

{-# 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减少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减少形式,这是GHC中的错误/限制或更高等级类型的一些基本问题？

我要说的原因不在于η-减少本身,问题在于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类型.

实际上它非常简单:GHC推断每个表达式的类型,然后开始统一它们=.当只有rank-1类型时,这总是很好,因为选择了最多态的(这是明确定义的); 所以任何可能的统一都会成功.

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

这并没有解释为什么它不能从get签名中看出它需要在这里选择排名-2,但可能也有一个很好的理由.