“减少Eta"指的是“减少".并不总是在Haskell举行? [英] "Eta reduce" is not always held in Haskell?

问题描述

我发现我可以说

  {-#语言RankNTypes#-}f1 ::(forall b.b-> b)->(全部抄送-> c)f1 f = id f 

(而HLint告诉我我可以在这里进行减少Eta"操作)，但是

  f2 ::(forall b.b-> b)->(全部抄送-> c)f2 = id 

无法编译:

 无法匹配预期的类型`c->C'实际类型为"forall" b.b->b'预期类型:(全部b.b-> b)->c->C实际类型:(全部b.b-> b)->永远b.b->b在表达式中:id在f2的等式中:f2 = id 

实际上，在更复杂的情况下我也遇到类似的问题，但这是我能想到的最简单的例子.因此，或者HLint无法在此处提供适当的建议，或者编译器将检测到这种情况，是吗?

更新

但是为什么会有这样的限制?为什么计算机不能自动将等级1和等级2统一(忘记类型推断，所有类型都可以用符号表示)?

解决方案

我不确定HLint是否完全了解 RankNTypes .

启用该扩展名后，通常不可能实现eta减少.GHC不能只是统一 a-> a 和(forall b.b-> b)->(forall c.c-> c)，否则它将完全破坏Rank1-code ¹ 的类型推断能力.OTOH，将(forall b.b-> b)与 a 参数统一起来不是问题；结果确定为(forall b.b-> b)与(forall c.c-> c)匹配.

---

¹ 考虑地图ID [(+1)，(* 2)] .如果允许 id 具有您要处理的类型，则编译器最终可能会为多态的 Num 函数产生不同的实例选择，这当然是不可能的.还是应该?我不确定，正在考虑...

无论如何，我很确定它证明了RankNTypes不可能进行全类型推断，因此至少要在Rank1子集GHC中获取它，必须通常默认为不太可能的多态选择.

I found that I can say

{-# LANGUAGE RankNTypes #-}
f1 :: (forall b.b -> b) -> (forall c.c -> c)
f1 f = id f

(and HLint tell me I can do "Eta reduce" here), but

f2 :: (forall b.b -> b) -> (forall c.c -> c)
f2 = id

fail to compile:

Couldn't match expected type `c -> c'
            with actual type `forall b. b -> b'
Expected type: (forall b. b -> b) -> c -> c
  Actual type: (forall b. b -> b) -> forall b. b -> b
In the expression: id
In an equation for `f2': f2 = id

Actually I have a similar problem in a more complicated situation but this is the simplest example I can think of. So either HLint is fail to provide proper advise here, or the compiler shall detect this situation, is it?

UPDATE

Another revelent question looks similar. However although both answers are quite useful, neither satisfy me, since they seems not touching the heart of the question.

For example, I am not even allowed to assign id with the proposed rank 2 type:

f2 :: (forall b.b -> b) -> (forall c.c -> c)
f2 = id :: (forall b.b -> b) -> (forall c.c -> c)

If the problem is just about type inference, an explicit type notation shall solve it (id have type a -> a, and it has been constrained to (forall b.b -> b) -> (forall c.c -> c). Therefore to justify this use, (forall b.b -> b) must match (forall c.c -> c) and that is true). But the above example shows this is not the case. Thus, this IS a true exception of "eta reduce": you have to explicitly add parameters to both sides to convert a rank 1 typed value in to rank 2 typed value.

But why there is such a limitation? Why the computer cannot unify rank 1 type and rank 2 type automatically (forget about type inference, all types can be given by notations)?

解决方案

I'm not sure HLint is aware of RankNTypes at all, perhaps not.

Indeed eta reduction is often impossible with that extension on. GHC can't just unify a->a and (forall b.b -> b) -> (forall c.c -> c), otherwise it would completely mess up its type inference capability for Rank1-code¹. OTOH, it's not a problem to unify (forall b.b -> b) with the a argument; the result is confimed to be (forall b.b -> b) which matches with (forall c.c -> c).

---

¹Consider map id [(+1), (*2)]. If id were allowed to have the type you're dealing with, the compiler could end up producing different instance choice for the polymorphic Num functions, which certainly shouldn't be possible. Or should it? I'm not sure, thinking about it...

At any rate, I'm pretty sure its proven that with RankNTypes, full type inference is not possible, so to get it at least in the Rank1 subset GHC must usually default to this as a less-than-possible polymorphic choice.

这篇关于“减少Eta"指的是“减少".并不总是在Haskell举行?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！