haskell - 为什么将未定义函数与未装箱类型一起使用时是多态的？

Question

我刚看完论文Levity Polymorphism .

我有一个关于为什么 undefined 的问题当用作未装箱类型时，可以是轻量多态的。

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

盒装 :

一个 盒装值由指向堆的指针表示。

Int和 Bool是具有 的类型的示例盒装值(value)观。

未装箱 :

一个 未装箱值由值本身表示(不是指向堆的指针)。

Int# 和 Char# 来自 GHC.Prim 模块是 类型的示例未装箱值(value)观。

一个 未装箱 value 不能是 thunk。未装箱类型的函数参数必须按值传递。

论文随后给出了一些轻浮的定义:

解除 :

一个 解除 type 是一种懒惰的类型。

一个 解除 type 具有超出正常元素的额外元素，表示非终止计算。

例如，类型 Bool是 解除 ，这意味着 Bool 有三个不同的值: True , False , 和 ⊥ (底部)。

全部 解除类型必须是 盒装 .

未吊装

一个 未吊装 type 是一种严格的类型。

元素 ⊥不存在于 中未吊装类型。

Int#和 Char#是 的示例未吊装类型。

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

这允许您编写一个轻量多态的 undefined 具有以下类型:

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

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

这是使用 undefined 的示例作为未装箱、未提升 Int#在 GHCi 中:

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

我一直在想 undefined与 ⊥ 相同(底部)。然而，论文说，“元素 ⊥ 不存在于未提升的类型中。”

这里发生了什么？是 undefined实际上不是 ⊥当用作未提升类型时？我是否误解了这篇论文(或盒子或轻浮)？

Answer 1

“Levity Polymorphism”论文的作者在这里。

首先，我想澄清一下上面提到的一些误解:

Bool确实是一种提升、盒装的类型。但是，它仍然只有 2 个值:True和 False .表达式 ⊥ 根本不是一个值。它是一个表达式，一个变量可以绑定(bind)到 ⊥，但这不会使 ⊥ 成为一个值。也许更好的说法是，如果 x :: Bool ，然后评估 x可能导致三种不同的结果: 评估为 True , 评估为 False ，和⊥。在这里，⊥ 表示任何不会正常终止的计算，包括抛出异常(undefined 确实如此)和永远循环。

与最后一点类似，undefined不是一个值。它是任何类型的居民，但它不是一个值。值是在求值时什么都不做的东西——但 undefined不符合那个规范。

根据你的看法，⊥ 可以存在于未提升的类型中。例如，采用以下定义:

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

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

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

那么，我们如何允许 undefined有一个未提升的类型？ @dfeuer 说得对: undefined暗地里是一个函数。它的完整类型签名是 undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a , 表示它是一个函数，就像 loop ， 以上。在运行时，它将当前调用堆栈作为参数。所以，每当你使用 undefined ，你只是在调用一个抛出异常的函数，不会造成任何麻烦。

确实，在设计 levity 多态性时，我们遇到了 undefined在相当长的一段时间里，用各种恶作剧让它成功。然后，当我们意识到 undefined有 HasCallStack约束，我们看到我们可以完全避开这个问题。如果没有 HasCallStack 看似无关紧要的用户便利，我真的不知道我们会做什么。 .