什么是 Levity 多态性 [英] What is Levity polymorphism

问题描述

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

As the title of the question indicates, I want to know what is Levity polymorphism and what is its motivation ? I know this page has some details in it, but most of the explanations there go over the top of my head. :)

虽然这个页面更友好一些，但我仍然没有能够理解其背后的动机.

While this page is a little friendlier, I'm still not able to understand the motivation behind it.

推荐答案

注意:此答案基于对 Levity 讨论的最新观察结果.有关 Levity 多态性的所有内容目前仅在 GHC 8.0 候选版本中实现，因此可能会发生变化(参见 #11471 例如).

Note: This answer is based on very recent observations on Levity discussions. Everything concerning Levity polymorphism is currently only implemented in the GHC 8.0 release candidates and as such subject to change (see #11471 for example).

TL;DR:这是一种使函数在提升和未提升类型上多态的方法，这是常规函数无法实现的.例如，以下代码不会使用常规 poly­mor­phi­sms 进行类型检查，因为 Int# 具有种类 #，但是 id 中的类型变量 有种 *:

TL;DR: It's a way to make functions polymorphic over lifted and unlifted types, which is not possible with regular functions. For example the following code doesn't type check with regular poly­mor­phi­sms, since Int# has kind #, but the type variables in id have kind *:

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

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

Note that (->) still uses some magic.

在我开始回答这个问题之前，让我们退后一步，回到最常用的函数之一，($).

Before I start to answer this question, let us take a step back and go to one of the most often used functions, ($).

($) 的类型是什么?好吧，根据 Hackage 和报告，这是

What is ($)'s type? Well, according to Hackage and the report, it's

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

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

However, that's not 100% complete. It's a convenient little lie. The problem is that polymorphic types (like a and b) have kind *. However, (library) developers wanted to use ($) not only for types with kind *, but also for those of kind #, e.g.

unwrapInt :: Int -> Int#

虽然 Int 有种类 *(可以是底部)，Int# 有种类 #(和根本不可能是底部).尽管如此，以下代码类型检查:

While Int has kind * (it can be bottom), Int# has kind # (and cannot be bottom at all). Still, the following code typechecks:

unwrapInt $ 42

那应该行不通.还记得 ($) 的返回类型吗?它是多态的，多态类型有 *，而不是 #！那么它为什么起作用呢?首先，它是一个错误，然后是一个hack(摘自 Ghc-dev 邮件列表中 Ryan Scott 的一封邮件:

That shouldn't work. Remember the return type of ($)? It was polymorphic, and polymorphic types have kind *, not #! So why did it work? First, it was a bug, and then it was a hack (excerpt of a mail by Ryan Scott on the ghc-dev mailing list):

为什么会发生这种情况?

So why is this happening?

长答案是，在 GHC 8.0 之前，在类型签名中 ($) :: (a -> b) ->->b，b 实际上不是*，而是OpenKind.OpenKind 是一个可怕的 hack，它允许提升 (kind *) 和unlifted (kind #) 类型来栖息它，这就是为什么 (unwrapInt $ 42)类型检查.

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 中的新类型是什么?这是

So what is ($)'s new type in GHC 8.0? It's

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

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

To understand it, we must look at Levity:

data Levity = Lifted | Unlifted

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

Now, we can think of ($) as having either one of the following types, since there are only two choices of w:

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

TYPE 是一个神奇的常量，它重新定义了 * 和 # 类型为

TYPE is a magical constant, and it redefines the kinds * and # as

type * = TYPE Lifted
type # = TYPE Unlifted

对种类的量化也是相当新的，并且是Haskell 中依赖类型的集成.

The quantification over kinds is also fairly new and part of the integration of dependent types in Haskell.

Levity 多态性 这个名字来自这样一个事实，即您现在可以在提升和未提升类型上编写多态函数，这是以前的多态限制不允许/不可能的.它还同时摆脱了 OpenKind hack.这真的很只是"，处理这两种类型.

The name Levity polymorphism comes from the fact that you now can write polymorphic functions over both lifted and unlifted types, something that wasn't allowed/possible with the previous poly­mor­phism restrictions. It also gets rid of the OpenKind hack at the same time. It's really "just" about this, handling both kinds of kinds.

_{顺便说一下，您的问题并不孤单.甚至 Simon Peyton Jones 说需要一个 Levity 维基页面 和 Richard E.(当前的实现者)指出维基页面需要更新当前进程.}

_{By the way, you're not alone with your question. Even Simon Peyton Jones said that there's a need for a Levity wiki page, and Richard E. (the current implementer of this) stated that the wiki page needs an update on the current process.}

• 依赖 Haskell 中的 Levity 多态性；Richard A. Eisenberg 在 ICFP 2015 上的演讲.非常推荐.
• Levity 多态性(扩展版本)，作者:Richard A. Eisenberg 和 Simon Peyton Jones
• GHC.Types，GHC 附带的 ghc-prim 库的一部分.
• 讨论:
  • 关于ghc-dev的讨论.
  • 关于haskell-cafe的讨论.
  • Levity Polymorphism In Dependent Haskell; talk by Richard A. Eisenberg on ICFP 2015. Very recommended.
  • Levity Polymorphism (extended version) by Richard A. Eisenberg and Simon Peyton Jones
  • GHC.Types, part of the ghc-prim library that's shipped with GHC.
  • Discussions:
    • The discussion on ghc-dev.
    • The discussion on haskell-cafe.

    这篇关于什么是 Levity 多态性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！