什么是Levity多态性

正如问题的标题所示，我想知道什么是Levity多态性，它的动机是什么？ 我知道这个页面里面有一些细节，但是大部分的解释都在我头上。 🙂

虽然这个页面有点友好，但我仍然无法理解它背后的动机。

Answer 1

注意：这个答案是基于最近关于Levity讨论的观察。 关于Levity多态性的一切目前只在GHC 8.0版本的候选版本中实现，因此可以改变（例如参见＃11471 ）。

---

TL; DR ：这是一种通过提升和不提升types来实现函数多态的方法，这对于常规函数来说是不可能的。 例如，下面的代码没有使用正则多态性进行types检查，因为Int#具有kind # ，但id的typesvariables有* ：

 {-# 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 

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

---

在我开始回答这个问题之前，让我们回过头来看看最常用的函数之一($) 。

什么是($)的types？ 那么，根据Hackage和报告，这是

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

但是，这不是100％完成。 这是一个方便的小谎言。 问题是多态types（如a和b ）有* 。 然而，（库）开发人员想要使用($)不仅适用于types* ，还适用于types# ，例如

 unwrapInt :: Int -> Int# 

虽然Int有* （可以是底部），但是Int#有kind（并且根本不可能是底部）。 不过，下面的代码typechecks：

 unwrapInt $ 42 

这不应该工作。 记住($)的返回types？ 它是多态的，多态types有* ，而不是# ！ 那么为什么它工作？ 首先，这是一个bug ，然后是一个黑客 （ Ryan Scott在ghc-dev邮件列表中的一段邮件摘录）：

那为什么会这样呢？

长的回答是，在GHC 8.0之前，在types签名($) :: (a -> b) -> a -> b ， b实际上不是实物，而是OpenKind 。 OpenKind是一个非常糟糕的黑客攻击，它允许提升（kind * ）和unlifted（kind # ）types居住它，这就是为什么(unwrapInt $ 42) typechecks。

那么什么是($)在GHC 8.0中的新types？ 它的

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

要了解它，我们必须看看Levity ：

 data Levity = Lifted | Unlifted 

现在我们可以把($)看成是以下两种types之一，因为w只有两种select：

 -- 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中依赖types集成的一部分。

Levity多态性的名字来源于这样一个事实，即你现在可以在提取和未提取的types上编写多态函数，这是以前的多态性限制所不允许的/可能的。 它同时也摆脱了OpenKind入侵。 这是真正的“正义”，处理这两种types。

_{顺便说一下，你并不孤单，你的问题。 甚至西蒙·佩顿·琼斯（Simon Peyton Jones）也表示需要一个Levity wiki页面 ，Richard E.（当前的实现者） 指出，wiki页面需要对当前进程进行更新 。}

参考

• 依赖于Haskell的Levity多态性 ; 理查德·A·艾森伯格（Richard A. Eisenberg）在ICFP 2015上的发言。非常推荐。
• 理查德·A·艾森伯格（Richard A. Eisenberg）和西蒙·佩顿·琼斯（Simon Peyton Jones ）的“ Levity Polymorphism”（扩展版）
• GHC.Types是GHC附带的ghc-prim库的一部分。
• 讨论：
  • 关于ghc-dev的讨论。
  • 关于haskell-cafe的讨论。