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

问题描述

我刚读完论文Levity Polymorphism.

我有一个问题，为什么 undefined 在用作未装箱类型时可以是 levity-polymorphic.

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

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

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 是具有 boxed 值的类型示例.

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# 和 Char# 来自 GHC.Prim 模块是具有 unboxed 值的类型示例.

unboxed 值不能是 thunk.未装箱类型的函数参数必须按值传递.

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.

lifted 类型具有超出正常元素的额外元素，表示非终止计算.

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

例如Bool类型为lifted，表示Bool有3个不同的值:True、False 和 ⊥(底部).

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

所有提升类型必须装箱.

未提升

• unlifted 类型是严格的.

元素 ⊥ 不存在于 unlifted 类型中.

The element ⊥ does not exist in an unlifted type.

Int# 和 Char# 是 unlifted 类型的示例.

Int# and Char# are examples of unlifted types.

本文继续解释 GHC 8 如何提供允许类型变量具有多态性的功能.

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

这允许您编写一个 levity-polymorphic undefined 具有以下类型:

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

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

这表示 undefined 应该适用于 any 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 在用作未提升类型时实际上不是 ⊥ 吗?我是不是误解了这篇论文(或 boxity 或 levity)?

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)?

推荐答案

这里是Levity Polymorphism"论文的作者.

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.

确实，在设计 levity 多态性时，我们与 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.

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