What does type signature for `undefined` mean in Haskell?
This is a continuation of @leftaroundabout's answer.
In Haskell, values have types. But types themselves also have types. When a type is acting as the type of another type, we call it a "kind".
The most important and common kind in Haskell is Type
, often denoted in signatures as *
. It is the kind of types that are "lifted", that is, whose values can be thunks that, when evaluated, can diverge, throw an error, etc... For example the type Int
has kind Type
.
There are also other types like Int#
that are not lifted. A value of type Int#
is never a thunk, it's always an actual value in memory.
In short, the in-memory representation of values is controlled by their type's kind.
RuntimeRep
is another kind. It is the kind of types like LiftedRep
and IntRep
. These types don't have any values, they exist merely to express things at the type level, as we shall see.
There is a super-magical type-level entity called TYPE
that, when parameterized with a type of kind RuntimeRep
(that is with a type that describes an in-memory representation) returns the kind of types whose values have that representation. For example, Type
is TYPE LiftedRep
, while the kind of Int#
is TYPE IntRep
.
ghci> :set -XMagicHash
ghci> import GHC.Prim
ghci> import GHC.Types
ghci> import Data.Kind
ghci> :kind (Int :: TYPE 'LiftedRep)
(Int :: TYPE 'LiftedRep) :: *
ghci> :kind Int#
Int# :: TYPE 'IntRep
Now we can get back to why undefined
has such a weird signature. The thing is, we want to be able to use undefined
in all functions, be it functions that return types of kind Type
, but also functions that return types of kind TYPE IntRep
(in other words: the Int#
type) or functions that return another unlifted type. Otherwise, we would need multiple different versions of undefined
, which would be annoying.
The solution is to make undefined
levity-polymorphic. The signature says: for any possible in-memory representation (RuntimeRep
) and for any possible type whose values have that representation, undefined
counts a member of that type.
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?