Why is the undefined function levity-polymorphic when using it with unboxed types?

Question

I just got finished reading the paper Levity Polymorphism.

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:

• boxed:

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

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

• unboxed:

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

  • 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:

• lifted:

  • A lifted type is one that is lazy.

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

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

  • All lifted types MUST be boxed.

• unlifted

  • An unlifted type is one that is strict.

  • The element ⊥ does not exist in an unlifted type.

  • Int# and Char# are examples of unlifted types.

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

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

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

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

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

---

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."

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

Answer 1

Author of the "Levity Polymorphism" paper here.

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

• 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.

• 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
  

  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.

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

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.

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.