如何减少井型功能导致类型错误？ [英] How can eta-reduction of a well typed function result in a type error?

问题描述

<$ p $

{ - ＃LANGUAGE RankNTypes＃ - }

导入Control.Applicative

类型Lens ca = 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 :: Lens ca  - > c  - > a 
 get = getWith id 
  

然后GHC（7.4.2）抱怨

 无法匹配预期类型`Lens c a'
，其实际类型为'（a0  - > Const b0 a0） - > c0  - > Const b0 c0'
预期类型：Lens c a  - > c  - > a 
实际类型：（（a0-> Const b0 a0） - > c0  - > Const b0 c0）
  - > c0  - > b0 
在`getWith'
调用的返回类型中：getWith id 
  

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

什么原因导致GHC拒绝eta-reduced形式，这是GHC中的一个错误/限制或者一些基本问题等级类型？

解决方案

我会说，原因不在于η减少本身，问题在于 RankNTypes 您将失去主体类型和类型推断。

高级别类型推断的问题是推导λx.M符合规则的类型

  Γ，x：σ|  -  M：ρ
 ---------------------- 
Γ|  - λx：σ.M：σ →ρ
  

我们不知道应该为 x选择什么类型的σ 。在Hindley-Milner类型系统的情况下，我们将自己限制为 x 的无类型量词的类型，并且推理是可能的，但不适用于任意排序类型。所以即使使用 RankNTypes ，当编译器遇到一个没有明确类型信息的术语时，它会诉诸于Hindley-Milner并推断它的一级主要类型。然而，在你的情况下，你需要的类型 getWith id 是rank-2，所以编译器不能自己推断它。

您的明确情况

  get lens = getWith id lens 
  

对应于已经明确给出 x 的类型λ的情况（X：σ）.MX 。在检查 getWith id lens 之前，编译器知道 lens 的类型。

$

  get = getWith id 
   / pre> 
 
 
编译器必须自行推断出 getWidth id 的类型，所以它坚持使用Hindley- Milner并推断排名不足的类型。
 
I was playing around with van Laarhoven lenses and ran into a problem where the type-checker rejects the eta-reduced form of a well-typed function:
{-# 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
The above type-checks but if I eta-reduce get to
get :: Lens c a -> c -> a
get = getWith id
Then GHC (7.4.2) complains that
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
I can understand that if the function didn't have an explicit type-signature then eta-reduction in combination with the monomorphism restriction might confuse the type inference, especially when we are dealing with higher rank types, but in this case I'm not sure what's going on.

What causes GHC to reject the eta-reduced form and is this a bug/limitation in GHC or some fundamental problem with higher rank types?
解决方案
I'd say that the reason isn't in the η-reduction itself, the problem is that with RankNTypes you lose principal types and type inference.

The problem with type inference with higher-order ranks is when inferring the type of λx.M to obey the rule
     Γ, x:σ |- M:ρ
----------------------
  Γ |- λx:σ.M : σ→ρ
we don't know what type σ we should choose for x. In the case of Hindley-Milner type system, we limit ourselves to type-quantifier-free types for x and the inference is possible, but not with arbitrary ranked types.

So even with RankNTypes, when the compiler encounters a term without explicit type information, it resorts to Hindley-Milner and infers its rank-1 principal type. However, in your case the type you need for getWith id is rank-2 and so compiler can't infer it by itself.

Your explicit case
get lens = getWith id lens
corresponds to the situation where the type of x is already given explicitly λ(x:σ).Mx. The compiler knows the type of lens before type-checking getWith id lens.

In the reduced case
get = getWith id
the compiler has to infer the type of getWidth id on it's own, so it sticks with Hindley-Milner and infers the inadequate rank-1 type.

                        
这篇关于如何减少井型功能导致类型错误？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！