RankNTypes和点运算符 [英] RankNTypes and the dot operator

问题描述

当我使用RankNTypes时，似乎（。）运算符不能很好地工作。

  { - ＃LANGUAGE RankNTypes，ImpredicativeTypes＃ - } 
 
f :: Int  - > （r r→r）
 f =未定义
 
 g ::（全部r→r→r）→> Int 
 g =未定义
 
 h :: Int  - > Int 
  -  h v = g（f v） - 效果很好
 h = g。 f  - 我不能用这种方式写它
  

我得到以下错误。

  [1 of 1]编译Main（test.hs，解释）
 
 test.hs：11：9： 
无法匹配类型'r0  - > r0'与'forall r。' r  - > r'
预期类型：Int  - >福尔尔河r  - > r 
实际类型：Int  - > r0  - > r0 
在'（。）'的第二个参数中，即'f'
在表达式中：g。 f 
失败，模块加载：无。 
  

解决方案

实际上， f 没有类型 Int - > （forall r。r - > r），因为GHC 漂浮在外 a>每个 forall 和类限制到范围的顶部。所以 f 的类型确实是 forall r。 Int - > r - > r 。

例如，以下的类型检测：

  f :: Int  - > （forall r。r  - > r）
 f =未定义
 
 f':: forall r。 Int  - > r  - > r 
 f'= f 
  

这使得 g。 （ r - > r 和之间的差异显示错误消息明确指出> f
$ b

GHC在发现<$ c $时抛出错误可能是更好的行为c> forall -s在错误的地方，而不是默默地将它们浮出。



多态返回类型（由于浮动 forall -s）是非法的） t允许在GHC中。有关详细信息，请参阅本文（特别是第4.6节）。简而言之，它们只有在坚定地支持暗含的实例化时才有意义，而GHC缺乏这种实例化。在没有预测性类型的情况下，浮动运算允许更多的术语进行类型检查，并且很少会在现实世界的代码中造成不便。


When I use RankNTypes, it seems that (.) operator doesn't work well. Where is this limitation documented?

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

f :: Int -> (forall r. r -> r)
f = undefined

g :: (forall r. r -> r) -> Int
g = undefined

h :: Int -> Int
-- h v = g (f v) -- It works well
h = g . f -- I can't write it in this way

I get following errors.

[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:11:9:
    Couldn't match type ‘r0 -> r0’ with ‘forall r. r -> r’
    Expected type: Int -> forall r. r -> r
      Actual type: Int -> r0 -> r0
    In the second argument of ‘(.)’, namely ‘f’
    In the expression: g . f
Failed, modules loaded: none.

解决方案

Actually, f doesn't have type Int -> (forall r. r -> r), because GHC floats out every forall and class constraint to the top of the scope. So f's type is really forall r. Int -> r -> r.

For example, the following typechecks:

f :: Int -> (forall r. r -> r)
f = undefined

f' :: forall r. Int -> r -> r
f' = f

This makes the g . f composition ill-typed (we can see that the error message points explicitly at the discrepancy between r -> r and forall r. r -> r).

It would be probably better behavior for GHC to throw errors upon finding forall-s in wrong places, instead of silently floating them out.

There are several reasons why polymorphic return types (which are outlawed by floating-out forall-s) aren't allowed in GHC. For details you can refer to this paper (section 4.6 specifically). In short, they only make sense if there is solid support for impredicative instantiation, which GHC lacks. In the absence of impredicative types, floating-out allows more terms to typecheck and rarely causes inconvenience in real world code.

这篇关于RankNTypes和点运算符的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！