为什么在使用未装箱类型时，未定义的函数levity-polymorphic是多态的？

Question

我刚刚读完了轻松多态这篇论文。

我有一个问题，就是为什么当使用undefined作为非装箱类型时，它可以是轻松多态的。

首先，让我们从论文中一些关于装箱性的定义开始：

• boxed:

  • 指针指向堆中的值表示boxed值。

  • Int和Bool是具有boxed值的类型的示例。

• unboxed:

  • unboxed值由值本身表示（而不是指向堆的指针）。

  • GHC.Prim模块中的Int#和Char#是具有unboxed值的类型的示例。

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

接下来的论文介绍了一些levity的定义：

• lifted:

  • 一个lifted类型是指它是惰性的。

  • 一个lifted类型有一个额外的元素，超出了正常元素的范畴，表示一个非终止计算。

  • 例如，类型Bool是lifted的，这意味着Bool有三个不同的值：True、False和⊥（底部）。

  • 所有lifted类型都必须boxed。

• unlifted

  • 一个unlifted类型是指它是严格的。

  • 元素⊥在unlifted类型中不存在。

  • Int#和Char#是unlifted类型的例子。

该论文还解释了GHC 8提供的功能，允许类型变量具有多态的levity。

这使您可以编写以下类型的levity-polymorphic undefined：

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

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

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

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

---

我一直认为undefined与⊥(底部)相同。然而，论文中说："元素⊥在未提升的类型中不存在。"

这是怎么回事？当作为未提升的类型时，undefined实际上不是⊥吗？我是否误解了论文（或boxity或levity）的某些内容？

- illabout

---

但是，未提升类型的定义明确表示它们不具有已知值作为值。我认为这个问题非常有动机，我自己也很好奇答案是什么。 - Daniel Wagner

@DanielWagner：我正在查看维基百科（https://en.wikipedia.org/wiki/Bottom_type#Computer_science_applications），其中提到：“底部类型经常用于以下目的：发出函数或计算发散的信号；换句话说，不向调用者返回结果。”也就是说，底部的含义可能是无限循环、崩溃、退出等。因此，它不能作为一个值返回。这就是为什么它不能属于严格/未提升计算类型的原因；在惰性计算中，它可以被推迟。 - 9000

@9000 这是底部值，而不是底部类型。话虽如此：无限循环、崩溃、退出、异常都是底部（语义上相同——Haskell 偶尔让你区分它们的事实在某些方面是作弊）。undefined 抛出一个异常，在这方面是底部的。 - Daniel Wagner

一个要点是，变量（甚至是虚拟模式 _）永远不能被绑定到未lifted类型的底部值。如果给定 f (x :: Int#) = ...，那么如果我调用 f undefined，执行永远不会到达右侧。GHC 将在调用 f 之前尝试评估 undefined。 - dfeuer

另外一点：我相当自信你实际上无法用你所指示的签名来写出“undefined”。它的“HasCallStack”约束条件是必需的，以满足类型检查器的要求。这使得它（有效地）成为了一个函数而非值。 - dfeuer

Answer 1

我是《轻松多态性》论文的作者。

首先，我想澄清一下上面提到的几个误解：

• Bool 确实是一个被提升和封装的类型。然而，它仍然只有两个值：True 和 False。表达式 ⊥ 只不过不是一个值。它是一个表达式，变量可以绑定到 ⊥，但这并不会使 ⊥ 成为一个值。或许更好的说法是，如果 x :: Bool，那么求值 x 可能会得到三种不同的结果：求值为 True，求值为 False，以及 ⊥。在这里， ⊥ 表示任何不正常终止的计算，包括抛出异常（这就是 undefined 实际上所做的事情）和永久循环。

• 与上一个观点类似，undefined 不是一个值。它是任何类型的成员，但它不是一个值。一个值是指当求值时什么也不做的东西，但 undefined 并不符合这个规范。

• 根据你如何看待它， ⊥ 可以 存在于非提升的类型中。例如，看看这个定义：

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

这个定义被 GHC 接受。然而，loop () 是一个未解封的、未打包的 Int# 类型的 ⊥ 元素。在这方面，未解封类型和解封类型的区别在于没有办法将变量绑定到 loop ()。任何尝试这样做的行为（如 let z = loop() in ...）都会在变量被绑定之前循环。

请注意，这与未经管理的语言（如 C）中的无限递归函数没有任何不同。

那么，我们如何允许 undefined 具有未解封类型？@dfeuer 是正确的：undefined 是一个秘密函数。它的完整类型签名是 undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a，意味着它像上面的 loop 一样是一个函数。在运行时，它将当前调用堆栈作为参数。因此，无论何时你使用 undefined，你只是调用一个抛出异常的函数，不会引起任何麻烦。

事实上，在设计提亮多态性时，我们花费了相当长的时间来处理 undefined，使用了各种花招来解决它。然后，当我们意识到 undefined 具有 HasCallStack 约束时，我们看到我们可以完全规避这个问题。老实说，如果没有 seemingly inconsequential 的用户方便的 HasCallStack，我真不知道我们会怎么做。

- Richard Eisenberg