6.4.12. Levity polymorphism¶
In order to allow full flexibility in how kinds are used, it is necessary
to use the kind system to differentiate between boxed, lifted types
(normal, everyday types like
[Bool]) and unboxed, primitive
types (Unboxed types and primitive operations) like
Int#. We thus have so-called levity
Here are the key definitions, all available from
TYPE :: RuntimeRep -> Type -- highly magical, built into GHC data RuntimeRep = LiftedRep -- for things like `Int` | UnliftedRep -- for things like `Array#` | IntRep -- for `Int#` | TupleRep [RuntimeRep] -- unboxed tuples, indexed by the representations of the elements | SumRep [RuntimeRep] -- unboxed sums, indexed by the representations of the disjuncts | ... type Type = TYPE LiftedRep -- Type is just an ordinary type synonym
The idea is that we have a new fundamental type constant
is parameterised by a
RuntimeRep. We thus get
Int# :: TYPE 'IntRep
Bool :: TYPE 'LiftedRep. Anything with a type of the form
TYPE x can appear to either side of a function arrow
->. We can
thus say that
-> has type
TYPE r1 -> TYPE r2 -> TYPE 'LiftedRep. The result is always lifted
because all functions are lifted in GHC.
22.214.171.124. No levity-polymorphic variables or arguments¶
If GHC didn’t have to compile programs that run in the real world, that would be the end of the story. But representation polymorphism can cause quite a bit of trouble for GHC’s code generator. Consider
bad :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2). (a -> b) -> a -> b bad f x = f x
This seems like a generalisation of the standard
$ operator. If we
think about compiling this to runnable code, though, problems appear.
In particular, when we call
bad, we must somehow pass
bad. How wide (that is, how many bits) is
x? Is it a pointer?
What kind of register (floating-point or integral) should
x go in?
It’s all impossible to say, because
a :: TYPE r1 is
levity polymorphic. We thus forbid such constructions, via the
following straightforward rule:
No variable may have a levity-polymorphic type.
bad because the variable
x would have a
However, not all is lost. We can still do this:
($) :: forall r (a :: Type) (b :: TYPE r). (a -> b) -> a -> b f $ x = f x
b is levity polymorphic. There are no variables
with a levity-polymorphic type. And the code generator has no
trouble with this. Indeed, this is the true type of GHC’s
slightly more general than the Haskell 98 version.
Because the code generator must store and move arguments as well as variables, the logic above applies equally well to function arguments, which may not be levity-polymorphic.
126.96.36.199. Printing levity-polymorphic types¶
RuntimeRepparameters as they appear; otherwise, they are defaulted to
Most GHC users will not need to worry about levity polymorphism
or unboxed types. For these users, seeing the levity polymorphism
in the type of
$ is unhelpful. And thus, by default, it is suppressed,
by supposing all type variables of type
RuntimeRep to be
when printing, and printing
TYPE 'LiftedRep as
StarIsType is on).
Should you wish to see levity polymorphism in your types, enable
-fprint-explicit-runtime-reps. For example,
ghci> :t ($) ($) :: (a -> b) -> a -> b ghci> :set -fprint-explicit-runtime-reps ghci> :t ($) ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b