1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
.. _runtime-rep:
Representation 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 ``Int`` and ``[Bool]``) and unboxed, primitive
types (:ref:`primitives`) like ``Int#``. We thus have so-called representation
polymorphism.
Here are the key definitions, all available from ``GHC.Exts``: ::
TYPE :: RuntimeRep -> Type -- highly magical, built into GHC
data Levity = Lifted -- for things like `Int`
| Unlifted -- for things like `Array#`
data RuntimeRep = BoxedRep Levity -- for anything represented by a GC-managed pointer
| 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 LiftedRep = BoxedRep Lifted
type Type = TYPE LiftedRep -- Type is just an ordinary type synonym
The idea is that we have a new fundamental type constant ``TYPE``, which
is parameterised by a ``RuntimeRep``. We thus get ``Int# :: TYPE 'IntRep``
and ``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.
Levity polymorphism
-------------------
A special case of representation polymorphism is levity polymorphism,
where we abstract over a variable of kind ``Levity``, such as: ::
example :: forall (l :: Levity) (a :: TYPE (BoxedRep l)). (Int -> a) -> a
example f = f 42
With :extension:`UnliftedDatatypes`, we can even declare levity-polymorphic
data types: ::
type PEither :: Type -> Type -> TYPE (BoxedRep l)
data PEither l r = PLeft l | PRight r
.. _representation-polymorphism-restrictions:
No representation-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 ``x`` into
``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 ``x``'s type, ``a :: TYPE r1`` is
representation-polymorphic. We thus forbid such constructions, via the
following straightforward rule:
No variable may have a representation-polymorphic type.
This eliminates ``bad`` because the variable ``x`` would have a
representation-polymorphic type.
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
Here, only ``b`` is representation-polymorphic. There are no variables
with a representation-polymorphic type. And the code generator has no
trouble with this. Indeed, this is the true type of GHC's ``$`` operator,
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 representation-polymorphic.
Representation-polymorphic bottoms
----------------------------------
We can use representation polymorphism to good effect with ``error``
and ``undefined``, whose types are given here: ::
undefined :: forall (r :: RuntimeRep) (a :: TYPE r).
HasCallStack => a
error :: forall (r :: RuntimeRep) (a :: TYPE r).
HasCallStack => String -> a
These functions do not bind a representation-polymorphic variable, and
so are accepted. Their polymorphism allows users to use these to conveniently
stub out functions that return unboxed types.
.. _printing-representation-polymorphic-types:
Printing representation-polymorphic types
-----------------------------------------
.. ghc-flag:: -fprint-explicit-runtime-reps
:shortdesc: Print ``RuntimeRep`` variables in types which are
runtime-representation polymorphic.
:type: dynamic
:reverse: -fno-print-explicit-runtime-reps
:category: verbosity
Print ``RuntimeRep`` parameters as they appear; otherwise, they are
defaulted to ``LiftedRep``.
Most GHC users will not need to worry about representation polymorphism
or unboxed types. For these users, seeing the representation polymorphism
in the type of ``$`` is unhelpful. And thus, by default, it is suppressed,
by supposing all type variables of type ``RuntimeRep`` to be ``LiftedRep``
when printing, and printing ``TYPE LiftedRep`` as ``Type`` (or ``*`` when
:extension:`StarIsType` is on).
Should you wish to see representation polymorphism in your types, enable
the flag :ghc-flag:`-fprint-explicit-runtime-reps`. For example,
.. code-block:: none
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
|
