haskelltypesundefinedforalltype-signature

What does type signature for `undefined` mean in Haskell?

I am a beginner in Haskell and I am taken aback by the undefined function's type signature.

I expected something more simple, but I found this on Hackage:

undefined :: forall (r :: RuntimeRep). forall (a :: TYPE r). HasCallStack => a

A special case of error. It is expected that compilers will recognize this and insert error messages which are more appropriate to the context in which undefined appears.

Could you please explain what does this signature mean?

Thanks!

Solution

  • For all regards a beginner needs to know, the signature is simply

    undefined :: a

    which means, as always with type variables (i.e. any lowercase letters) that a is universally quantified, which can also be made explicit:

    {-# LANGUAGE ExplicitForall #-}
undefined :: forall a. a

    ...or, as I prefer to write it

    {-# LANGUAGE ExplicitForall, UnicodeSyntax #-}
undefined :: ∀ a. a

    The quantification is infered to be over all types, i.e. all things with kind * (read: “type”, more accurate the kind of lifted types – lifted meaning it can be lazy thunk). Therefore, you can use undefined in any expression, no matter what type is required.

    Now, undefined is of course a “partial function” like thing, basically a function which zero arguments which is defined nowhere. (FTR, it's not a function, as a function by definition has argument[s].)
    You'd like to get a useful error message when it is actually evaluated, but GHC doesn't by default produce a call stack for everything (for performance reasons), so it used to be the case that the error message was almost completely useless. That's where the HasCallStack comes in: that's a constraint which essentially tells the context in which some code might incur undefined that it should note the place where it happens, in order for the error message to actually show it up. So,

    undefined :: ∀ a. HasCallStack => a

    It's a bit confusing that the HasCallStack appears after the ∀ a – this doesn't really have anything to do with a but with the context in which undefined will be used. Just, the form of signatures is always

    Identifier :: Quantifiers. Constraints => Type

    and HasCallStack is a constraint, that's why it appears in the middle. (More often, constraints actually apply to one of the type variables you've quantified over.)

    Finally, this RunTimeRep stuff is about levity polymorphism. I don't really understand that myself, but it's discussed in Why is the undefined function levity-polymorphic when using it with unboxed types?