与未装箱类型一起使用时，为什么未定义函数levity是多态的? [英] Why is the undefined function levity-polymorphic when using it with unboxed types?

问题描述

我刚读完论文生活多态性.

我有一个问题，为什么要 在用作非装箱类型时可以是多态的.

I had a question about why undefined can be levity-polymorphic when used as an unboxed type.

首先，让我们从论文中对拳击性的一些定义开始:

First, let's start with some definitions of boxity from the paper:

• 已装箱:

• 装框的值由指向堆的指针表示.

• A boxed value is represented by a pointer into the heap.

Int和Bool是具有装箱的值的类型的示例.

Int and Bool are examples of types that have boxed values.

未装箱:

• 未装箱的值由值本身(不是指向堆的指针)表示.

• An unboxed value is represented by the value itself (not a pointer to the heap).

Int# 和 模块是具有 unboxed 值的类型的示例.

Int# and Char# from the GHC.Prim module are examples of types with unboxed values.

一个未装箱的值不能是一个笨拙的东西.未装箱类型的函数参数必须按值传递.

An unboxed value cannot be a thunk. Function arguments of unboxed types must be passed by value.

本文遵循一些关于高度性"的定义:

The paper follows with some definitions of levity:

• 抬起:

• 提升类型是一种惰性类型.

• A lifted type is one that is lazy.

提升类型具有超出普通元素的额外元素，表示无终止计算.

A lifted type has on extra element beyond the normal ones, representing a non-terminating computation.

例如，类型Bool被提升为 ，这意味着Bool具有三个不同的值:True，False和⊥(底部).

For example, the type Bool is lifted, meaning that there are three different values for Bool: True, False, and ⊥ (bottom).

所有提升类型都必须装箱.

未举起

• 未提升类型是严格的类型.

元素⊥在未提升类型中不存在.

Int#和Char#是未提升类型的示例.

本文继续说明GHC 8如何提供功能，使类型变量具有多态性.

The paper goes on to explain how GHC 8 provides functionality allowing type variables to have polymorphic levity.

这使您可以编写多态性 undefined 具有以下类型:

This allows you to write a levity-polymorphic undefined with the following type:

undefined :: forall (r :: RuntimeRep). forall (a :: TYPE r). a

这表示undefined应该适用于任何 RuntimeRep，甚至是未提升的类型.

This says that undefined should work for any RuntimeRep, even unlifted types.

这里是在GHCi中将undefined用作未装箱，未抬起的Int#的示例:

Here is an example of using undefined as an unboxed, unlifted Int# in GHCi:

> :set -XMagicHash
> import GHC.Prim
> import GHC.Exts
> I# (undefined :: Int#)
*** Exception: Prelude.undefined

---

我一直认为undefined与⊥相同(底部).但是，该论文说:元素⊥在未提升类型中不存在."

---

I've always thought of undefined as being the same as ⊥ (bottom). However, the paper says, "The element ⊥ does not exist in an unlifted type."

这是怎么回事? undefined用作展开类型时，实际上不是⊥吗?我是否对纸张有误解(或者是直角或浅色)?

What is going on here? Is undefined not actually ⊥ when used as an unlifted type? Am I misunderstanding something about the paper (or boxity or levity)?

推荐答案

此处是生命多态"论文的作者.

Author of the "Levity Polymorphism" paper here.

首先，我想清除上述一些误解:

First, I want to clear up a few misconceptions stated above:

• Bool实际上是一种提升的盒装类型.但是，它仍然只有2个值:True和False.表达式⊥根本不是值.它是一个表达式，并且变量可以绑定到⊥，但这并不能使⊥成为值.也许更好的说法是，如果x :: Bool，则对x求值可以得出三个不同的结果:对True求值，对False求值和⊥.在这里，⊥表示任何不会正常终止的计算，包括引发异常(undefined确实会发生这种情况)并永远循环.

• Bool is indeed a lifted, boxed type. However, it still has only 2 values: True and False. The expression ⊥ is simply not a value. It's an expression, and a variable can be bound to ⊥, but that doesn't make ⊥ a value. Perhaps a better way of saying this all is that, if x :: Bool, then evaluating x can lead to three different results: evaluating to True, evaluating to False, and ⊥. Here, ⊥ represents any computation that doesn't terminate normally, including throwing an exception (which is what undefined really does) and looping forever.

类似于最后一点，undefined不是值.它是任何类型的居民，但这不是价值.值是被评估时不起作用的东西，但是undefined不符合该规范.

Similar to that last point, undefined is not a value. It's an inhabitant of any type, but it's not a value. A value is something that, when evaluated, does nothing -- but undefined doesn't meet that specification.

取决于您的观看方式，⊥可以以未提升的类型存在.例如，采用以下定义:

Depending on how you look at it, ⊥ can exist in an unlifted type. For example, take this definition:

loop :: () -> Int#
loop x = loop x

GHC接受此定义.但是loop ()是未提升，未装箱类型Int#的⊥元素.在这方面，未提升类型和提升类型之间的区别在于，无法将变量绑定到loop ().任何尝试这样做的尝试(例如let z = loop () in ...)都会在变量绑定之前循环.

This definition is accepted by GHC. Yet loop () is a ⊥ element of the unlifted, unboxed type Int#. The difference between an unlifted type and a lifted type in this regard is that there is no way to bind a variable to loop (). Any attempt to do so (like let z = loop () in ...) will loop before the variable ever gets bound.

请注意，这与非托管语言(例如C)中的无限递归函数没什么不同.

Note that this is no different than an infinitely recursive function in an unmanaged language, like C.

那么，我们怎么允许undefined具有未提升的类型? @dfeuer正确:undefined是秘密函数.它的完整类型签名是undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a，这意味着它是一个函数，就像上面的loop一样.在运行时，它将当前调用堆栈作为参数.因此，每当使用undefined时，您只是在调用一个引发异常的函数，而不会引起任何麻烦.

So, how is it that we allow undefined to have an unlifted type? @dfeuer has it right: undefined is secretly a function. Its full type signature is undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a, meaning that it's a function, just like loop, above. At runtime, it will take the current call stack as a parameter. So, whenever you use undefined, you're just calling a function that throws an exception, causing no trouble.

的确，在设计高度多态性时，我们与undefined斗争了相当长的一段时间，并使用各种诡计使之得以解决.然后，当我们意识到undefined具有HasCallStack约束时，我们看到可以完全避开该问题.老实说，如果没有HasCallStack似乎无关紧要的用户方便性，我不知道该怎么办.

Indeed, when designing levity polymorphism, we struggled with undefined for quite some time, with all sorts of shenanigans to make it work out. Then, when we realized that undefined had the HasCallStack constraint, we saw that we could just dodge the problem entirely. I honestly don't know what we would have done without the seemingly inconsequential user convenience of HasCallStack.

这篇关于与未装箱类型一起使用时，为什么未定义函数levity是多态的?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！