15

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

illabout
  • 3,517
  • 1
  • 18
  • 39
  • 2
    I suppose that `⊥` is any computation that cannot terminate normally, including e.g. infinite loops. OTOH `undefined` is a known _value_ which is checked for at runtime. – 9000 Apr 23 '18 at 18:08
  • 4
    @9000 But the definition of unlifted types is explicitly that they do not have that known value as an inhabitant. I think this question is quite well-motivated, and I myself am curious about the answer. – Daniel Wagner Apr 23 '18 at 18:26
  • 2
    @DanielWagner: I fail to see a contradiction. «The element `⊥` does not exist in an unlifted type»; `undefined` ≠ `⊥`. I also don't think that `I# (undefined :: Int#)` actually "produces" an `undefined` of type `Int#`. I suppose that at the first moment strict evaluation touches an "undefined", it raises an exception, and this is special-cased, as opposed to adding an `undefined` to every type. – 9000 Apr 23 '18 at 18:35
  • 1
    @9000 Hm. `undefined` is synonymous with ⊥ in every discussion of Haskell semantics I know of; why do you believe they are not equal? Or, what equality relation are you using that does not conflate them, and why do you believe that is the equality intended by the discussion in the question above? – Daniel Wagner Apr 23 '18 at 18:39
  • 2
    @DanielWagner: I'm looking [at wikipedia](https://en.wikipedia.org/wiki/Bottom_type#Computer_science_applications) which states: «The bottom type is frequently used for the following purposes: To signal that a function or computation diverges; in other words, does not return a result to the caller.» That is, a bottom's meaning may be an infinite loop, a crash, an exit, etc. It therefore _can not_ be returned as a value. This is why it cannot inhabit a type of a strict / unlifted computation; in a lazy computation, it can be deferred. – 9000 Apr 23 '18 at 18:50
  • 2
    I _don't know_ if `undefined` is indeed a value (that is, something that can be strictly computed and returned). I can imagine that it's not; then it can represent the bottom value. But then it also cannot be "instantiated", as the OP tries to do. OTOH if it were a value that can be computed, then it won't be bottom. So I suppose that computation around `undefined` is special-cased in compiler and runtime. It can be cast to any type, but not actually touched, so an attempt to construct in for an unlifted type should fail immediately (this must be easy to check). – 9000 Apr 23 '18 at 18:50
  • 3
    @9000 This is the bottom value, not the bottom type. That said: yes, an infinite loop, a crash, an exit, an exception are all bottom (and semantically identical -- the fact that Haskell occasionally lets you distinguish them is cheating in some ways). `undefined` throws an exception, and is bottom in that way. – Daniel Wagner Apr 23 '18 at 19:14
  • 2
    Hence we seem to have an answer: `undefined` may be levity-polymorphic because it's special-cased. It cannot be computed, by definition, so it can take part in any lazy computation as long as it's lazy, but an attempt to construct it for an unlifted type (with which it is type-compatible) ends with a runtime error, "producing" the bottom value. – 9000 Apr 23 '18 at 19:18
  • 8
    One thing is that a variable (and even the dummy pattern `_`) can never be bound to a bottom value of an unlifted type. Given `f (x :: Int#) = ...`, if I call `f undefined`, execution will never reach the right-hand side. GHC will attempt to evaluate `undefined` *before* calling `f`. – dfeuer Apr 23 '18 at 19:25
  • 1
    @dfeuer: Yes, because a value of bottom type is basically a crashed (or hung) computation, so the computation will crash (with an exception) before binding. – 9000 Apr 23 '18 at 19:34
  • 4
    Another point: I'm quite confident you actually *can't* write `undefined` with the signature you indicate. Its `HasCallStack` constraint is necessary to satisfy the type checker. That makes it (effectively) a function rather than a value. – dfeuer Apr 23 '18 at 19:40
  • 1
    @dfeuer Good point about `HasCallStack`. I took it out, hoping to make the type signature for `undefined` a little easier to read. It makes sense that it is actually necessary! – illabout Apr 24 '18 at 02:12

1 Answers1

17

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.

Richard Eisenberg
  • 299
  • 2
  • 5