什么是Levity多态性

Question

正如问题的标题所示,我想知道什么是Levity多态性及其动机是什么？我知道这个页面里面有一些细节,但大部分的解释都是我的头脑.:)

虽然这个页面更友好,但我仍然无法理解它背后的动机.

Answer 1

注意:这个答案是基于最近对Levity讨论的观察.有关Levity多态性的所有内容目前仅在GHC 8.0发布候选版中实现,因此可能会发生变化(例如,请参阅#11471).

TL; DR:这是一种使函数在提升和未提升类型上具有多态性的方法,这对于常规函数是不可能的.例如,以下代码不使用常规多态性进行类型检查,因为Int#有类型#,但类型变量id有类型*:

{-# LANGUAGE MagicHash #-}

import GHC.Prim

example :: Int# -> Int# 
example = id            -- does not work, since id :: a -> a

Couldn't match kind ‘*’ with ‘#’
When matching types
  a0 :: *
  Int# :: #
Expected type: Int# -> Int#
  Actual type: a0 -> a0
In the expression: id

请注意,(->)仍然使用一些魔法.

在我开始回答这个问题之前,让我们退后一步,转到最常用的功能之一($).

什么是($)类型？好吧,根据Hackage和报告,它是

($) :: (a -> b) -> a -> b

但是,这不是100%完成.这是一个方便的小谎言.问题是多态类型(如a和b)有类型*.但是,(库)开发人员($)不仅希望用于有类型的类型*,还要用于那些类型的类型#,例如

unwrapInt :: Int -> Int#

虽然Int有种*(它可以是底部),Int#但有种#(并且根本不可能是底部).仍然,以下代码类型检查:

unwrapInt $ 42

那应该不行.还记得退货类型($)吗？它是多态的,多态类型有种类*,不是#!那它为什么有效呢？首先,这是一个错误,然后它是一个黑客(Ryan Scott在ghc-dev邮件列表上的一封邮件的摘录):

那为什么会这样呢？

长期的答案是,在GHC 8.0之前,在类型签名中($) :: (a -> b) -> a -> b,b实际上并不是实物*,而是OpenKind. OpenKind是一个可怕的黑客,允许提升(善良*)和未提升(种类#)类型居住它,这就是为什么(unwrapInt $ 42) typechecks.

那么($)GHC 8.0中的新类型是什么？它的

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b
-- will likely change according to Richard E.

要理解它,我们必须看看Levity:

data Levity = Lifted | Unlifted

现在,我们可以认为($)有以下任何一种类型,因为只有两种选择w:

-- pseudo types
($) :: forall a (b :: TYPE   Lifted). (a -> b) -> a -> b
($) :: forall a (b :: TYPE Unlifted). (a -> b) -> a -> b

TYPE是一个神奇的常数,它重新定义了种*和#作为

type * = TYPE Lifted
type # = TYPE Unlifted

对种类的量化也是相当新的,也是Haskell中依赖类型集成的一部分.

Levity多态性的名称来自于您现在可以在提升和未提升类型上编写多态函数的事实,这是先前的多态性限制所不允许/不可能的.它同时也摆脱了OpenKind黑客攻击.它真的"只是"这个,处理两种类型.

_{顺便说一句,你并不孤单.甚至Simon Peyton Jones也表示需要一个Levity wiki页面,而Richard E.(当前的实现者)表示wiki页面需要更新当前流程.}

参考

• 依赖Haskell中的Levity多态性 ; Richard A. Eisenberg在ICFP 2015上的讲话.非常推荐.
• Levity Polymorphism(扩展版)由Richard A. Eisenberg和Simon Peyton Jones撰写
• GHC.Types,ghc-primGHC附带的库的一部分.
• 讨论:
  • 关于ghc-dev的讨论.
  • 关于haskell-cafe的讨论.