为什么美元（$）操作符在GHC 8.0.1中如此复杂？ [英] Why dollar ($) operator is so complex in GHC 8.0.1?

问题描述

 前奏> ：我（$）
（$）:: 
 forall（r :: GHC.Types.RuntimeRep）a（b :: TYPE r）。 
（a  - > b） - > a  - > b 
  - 定义于'GHC.Base'
 infixr 0 $ 
  

它与（a - > b） - >有什么不同？ a - > B'/ code>？有没有适合新型签名的 b ？

>在8.0之前，typechecker中有一个特殊情况，使得 $ 到 unlifted 类型的应用程序可以工作。这也意味着你无法定义自己的功能，可以同时使用提升和未提升的类型。现在，这个所谓的 Levity Polymorphsim （'levity'指''

<$ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ （*））

ap :: forall（TYPE，RuntimeRep（..））
导入Data.Kind a :: *）（b :: *）。 （a - > b） - > （a - > b）
ap f x = f x

ap_LP :: forall（a :: *）（b :: TYPE r）。 （a - > b） - > （a - > b）
ap_LP fx = fx

事实上 $ 函数现在被定义为与 ap_LP 相同，在类型检查器中不需要特殊情况来使 $ 使用返回未提升类型的函数（在类型检查器中还有一个特殊情况，用于制作多态应用程序，即 runST $ ... 工作，但这与轻度多态性无关）。这实际上是增加了复杂性的原因 - 现在类型系统中的黑客较少，GHC的用户可以通过给函数适当的类型来利用轻量级多态性（请注意，从未推断出轻量级多态类型，据我所知）。在轻量级多态性之前，如果您想编写一个多态函数，可以在提取和未提取类型上工作，您有义务使用不同类型签名编写两个相同的函数副本。

新类型与旧类型不同之处在于新类型比旧类型更具一般性：

   -  ok 
 ap':: forall（a :: *）（b :: *）。 （a  - > b） - > （a  - > b）
 ap'= ap_LP 
 
  - 类型错误：
  -  *无法将提升类型与未提升类型
 ap_LP':: forall（a :: *）（b :: TYPE r）。 （a  - > b） - > （a  - > b）
 ap_LP'= ap 
  

换句话说， code> b 这个'符合'旧签名必须（根据定义）适合新的签名类型（所以这个改变完全向后兼容！）。

---

另请注意，以下是不可能的：

  ap'':: forall（a :: TYPE r）（b :: *）。 （a  - > b） - > （a  - > b）
 ap''fx = fx 
  

产生的错误是

 这里不允许表示多态类型：
类型：a 
类型：TYPE r 
在活页夹'x'的类型中
  

和SPJ解释了限制这里：

（$）的第二个参数不能有一个
的非盒装类型是绝对正确的。因为（$）的代码必须在
（传给函数）时移动这个参数，所以它必须知道它的宽度，指针等等。但实际上调用结果（f $ x）可以是
，因为（$）的代码不会混淆结果;它
只是尾调用f。

这就是说，并不是每个轻量级多态类型都有一个有效的居民 - 这涉及到拆箱和盒装类型之间的操作区别，只能在某些情况下统一处理，并且类型检查工具确保它。

Prelude> :i ($)
($) ::
  forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
  (a -> b) -> a -> b
        -- Defined in ‘GHC.Base’
infixr 0 $

How is it different from (a -> b) -> a -> b? Is there any b that does not fit the new type signature?

解决方案

Before 8.0, there was a special case in the typechecker to make applications of $ to unlifted kinds work. This also meant that you couldn't define your own functions which could work with both lifted and unlifted kinds. Now that this so-called Levity Polymorphsim ('levity' refers to 'the degree to which something is lifted' - or 'lifted-ness', because of 'unlifted' and 'lifted' types) is built into the typechecker, this is possible:

import GHC.Exts (TYPE, RuntimeRep(..)) 
import Data.Kind (type (*))

ap :: forall (a :: *) (b :: *) . (a -> b) -> (a -> b) 
ap f x = f x 

ap_LP :: forall (a :: *) (b :: TYPE r) . (a -> b) -> (a -> b) 
ap_LP f x = f x

and indeed the $ function is now defined identically to ap_LP, with no special case needed in the typechecker to make $ work with functions returning unlifted types (there is a still a special case in the typechecker to make polymorphic application, i.e. runST $ ... work, but this is unrelated to levity polymorphism). This is essentially the reason for the added complexity - there are fewer 'hacks' in the type system now, and users of GHC can take advantage of levity polymorphism just by giving a function the appropriate type (note that levity-polymorphic types are never inferred, as far as I can tell). Before levity polymorphism, if you wanted to write a polymorphic function which could possible work on both lifted and unlifted kinds, you were obligated to write two identical copies of the function with different type signatures.

The new type differs from the old one in that the new type is strictly more general than the old one:

-- ok 
ap' :: forall (a :: *) (b :: *) . (a -> b) -> (a -> b) 
ap' = ap_LP 

-- type error: 
--    * Couldn't match a lifted type with an unlifted type
ap_LP' :: forall (a :: *) (b :: TYPE r) . (a -> b) -> (a -> b) 
ap_LP' = ap 

In other words, every b which 'fit' the old signature must (by definition) fit the new type signature (and so this change is perfectly backwards-compatible!).

---

Also note that the following is not possible:

ap'' :: forall (a :: TYPE r) (b :: *) . (a -> b) -> (a -> b)
ap'' f x = f x 

The error produced is

A representation-polymorphic type is not allowed here:
  Type: a
  Kind: TYPE r
In the type of binder `x'

and SPJ explains the reason for the restriction here:

It's absolutely right that the second argument to ($) must not have an unboxed kind. Because the code for ($) must move that argument around (pass to the function), so it must know its width, pointerhood ect.

But actually it would be ok for the result of the call (f $ x) to be unboxed, because the code for ($) doesn't mess with the result; it just tail-calls f.

This is to say that not every levity-polymorphic type has a valid inhabitant - and this relates to the operational distinction between unboxed and boxed types, which can only be treated uniformly in certain cases, and the typechecker makes sure of it.

这篇关于为什么美元（$）操作符在GHC 8.0.1中如此复杂？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！