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

问题描述

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

此页有点友善，我仍然无法理解背后的动机。

注意：这个答案是基于最近关于Levity讨论的观察。关于Levity多态性的所有内容目前仅在GHC 8.0版本候选版本中实现，因此可能会发生变化（请参阅＃11471 ）。

---

TL; DR ：这是一个通过正常函数不可能的方式来实现提升和未提升类型的多态函数。例如，以下代码不会键入与常规poly­ mor­ phi­ sms进行检查，因为 Int＃有类型＃，但是 id 中的类型变量具有类型 * ：

  { - ＃LANGUAGE MagicHash＃ - } 
 
 import GHC.Prim 
 
示例:: Int＃ - > Int＃
 example = id  - 不起作用，因为id :: a  - > a 
  

 不能匹配种类'*'和'＃'
匹配类型
 a0 :: * 
 Int＃::＃
预期类型：Int＃ - > Int＃
实际类型：a0  - > a0 
在表达式中：id 
  

请注意（ - > ;）仍然使用一些魔法。

---

在我开始回答这个问题之前，让我们退后一步，转到最常用的函数之一（$）。

什么是（$）的类型？那么，根据Hackage和报告，它是 $ b

 （$）::（a  - > b） - > a  - > b 
  

但是，这并非100％完整。这是一个方便的小谎言。问题是多态类型（例如 a 和 b ）具有类型 * 。然而，（库）开发人员不仅希望使用（$）来处理类型为 * 的类型，还要为那些＃，例如

  unwrapInt :: Int  - > Int＃
  

Int has kind * （可以是底部）， Int＃ has kind ＃ （并且根本不可能）。尽管如此，下面的代码类型检查：

  unwrapInt $ 42 
  

这不应该起作用。请记住（$）的返回类型？它是多态的，多态类型有 * ，而不是＃！那为什么它工作？首先，它是一个bug ，然后它是一个破解（摘自 Ryan Scott在ghc-dev邮件列表中的一封邮件）：

那么为什么会发生这种情况？

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

那么什么是GHC 8.0中的（$）的新类型？它是

 （$）:: forall（w :: Levity）a（b :: TYPE w）。 （a  - > b） - > a  - > b 
  - 根据理查德E.可能会改变
  

为了理解它，我们必须看看 Levity ：

 数据Levity = Lifted |取消
  

现在，我们可以考虑（$） w ：

   - 伪类型
（$）:: 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多态性来自于这样一个事实，即您现在可以在提升和未提升类型上编写多态函数，这是以前的poly­ mor­ phism限制所不允许/可能实现的。它同时也摆脱了 OpenKind hack。这是真正的正义，处理这两种类型。

_{顺便说一下，你并不孤单与你的问题。即使 Simon Peyton Jones表示需要一个Levity wiki页面和理查德E.（目前这个实施者）表示维基页面需要更新当前进程。}

引用

• 依赖Haskell的Levity多态性; Richard A. Eisenberg在ICFP 2015上发表演讲。非常值得推荐。 Levity Polymorphism（扩展版）由Richard A. Eisenberg和Simon Peyton Jones撰写
=https://github.com/ghc/ghc/blob/master/libraries/ghc-prim/GHC/Types.hs =noreferrer> GHC.Types ，这是GHC附带的 ghc-prim 库的一部分。 讨论：




• 关于 ghc-dev 。


• 关于 haskell-cafe 。

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.

解决方案

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: 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, ($).

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

($) :: (a -> b) -> 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#

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

unwrapInt $ 42

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?

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.

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.

To understand it, we must look at Levity:

data Levity = Lifted | Unlifted

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 is a magical constant, and it redefines the kinds * and # as

type * = TYPE Lifted
type # = TYPE Unlifted

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

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.

_{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.}

References

• 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屋！