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

Question

我刚读完Levity Polymorphism这篇论文.

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

首先,让我们从论文的一些盒子定义开始:

• 盒装:

  • 甲装箱值由指针到堆中表示.

  • Int并且Bool是具有盒装值的类型的示例.

• 未装箱:

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

  • Int#和Char#从所述GHC.Prim模块是类型与实例装箱值.

  • 未装箱的值不能是thunk.必须通过值传递未装箱类型的函数参数.

本文遵循一些轻浮的定义:

• 举起:

  • 甲抬起类型是一个是懒.

  • 甲解除类型具有超出了正常的人额外元件上,表示非终止计算.

  • 例如,该类型Bool被提升,这意味着存在用于三个不同的值Bool:True,False,和?(底部).

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

• 未提升

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

  • 该元素?不存在于未提升类型中.

  • Int#并且Char#是未提升类型的例子.

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

这允许您undefined使用以下类型编写levity-polymorphic :

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不是真正?为未提升类型时？我是否误解了论文(或盒子或轻浮)？

Answer 1

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

首先,我想澄清一些上述错误观念:

• Bool确实是一个提升的盒装类型.但是,它仍然只有2个值: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,您只需调用一个抛出异常的函数,不会造成任何麻烦.

事实上,在设计levity多态性时,我们已经挣扎undefined了很长一段时间,各种各样的恶作剧使它成功.然后,当我们意识到undefined有HasCallStack约束时,我们看到我们可以完全避开这个问题.老实说,如果没有看似无关紧要的用户便利,我们不知道我们会做些什么HasCallStack.