haskell - 什么是 Levity 多态性

Question

正如问题标题所示，我想知道什么是 Levity 多态性以及它的动机是什么？我知道this page其中有一些细节，但其中的大部分解释都超出了我的理解范围。 :)

同时this page有点友好，我仍然无法理解其背后的动机。

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

这不应该起作用。还记得($)的返回类型吗？它是多态的，多态类型具有 * 类型，而不是 #!那么为什么它有效呢？首先，它是a bug ，然后是 hack (摘自 ghc-dev 邮件列表上的 a mail by Ryan Scott):

So why is this happening?

The long answer is that prior to GHC 8.0, in the type signature ($) :: (a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind. OpenKind is an awful hack that allows both lifted (kind *) and unlifted (kind #) types to inhabit it, which is why (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

种类的量化is also fairly new和 integration of dependent types in Haskell 的一部分.

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

_{顺便说一下，你并不是唯一一个有这个问题的人。偶Simon Peyton Jones said that there's a need for a Levity wiki page和 Richard E.(当前的实现者)stated that the wiki page needs an update在当前进程上。}

引用文献

• Levity Polymorphism In Dependent Haskell ; Richard A. Eisenberg 在 ICFP 2015 上的演讲。强烈推荐。
• Levity Polymorphism (extended version)作者:理查德·A·艾森伯格和西蒙·佩顿·琼斯
• GHC.Types ，是 GHC 附带的 ghc-prim 库的一部分。
• 讨论:
  • 关于ghc-dev的讨论.
  • 关于haskell-cafe的讨论.