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
|
.. _type-level-literals:
Type-Level Literals
===================
GHC supports numeric and string literals at the type level, giving
convenient access to a large number of predefined type-level constants.
Numeric literals are of kind ``Nat``, while string literals are of kind
``Symbol``. This feature is enabled by the :extension:`DataKinds` language
extension.
The kinds of the literals and all other low-level operations for this
feature are defined in module ``GHC.TypeLits``. Note that the module
defines some type-level operators that clash with their value-level
counterparts (e.g. ``(+)``). Import and export declarations referring to
these operators require an explicit namespace annotation (see
:ref:`explicit-namespaces`).
Here is an example of using type-level numeric literals to provide a
safe interface to a low-level function: ::
import GHC.TypeLits
import Data.Word
import Foreign
newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)
clearPage :: ArrPtr 4096 Word8 -> IO ()
clearPage (ArrPtr p) = ...
Here is an example of using type-level string literals to simulate
simple record operations: ::
data Label (l :: Symbol) = Get
class Has a l b | a l -> b where
from :: a -> Label l -> b
data Point = Point Int Int deriving Show
instance Has Point "x" Int where from (Point x _) _ = x
instance Has Point "y" Int where from (Point _ y) _ = y
example = from (Point 1 2) (Get :: Label "x")
.. _typelit-runtime:
Runtime Values for Type-Level Literals
--------------------------------------
Sometimes it is useful to access the value-level literal associated with
a type-level literal. This is done with the functions ``natVal`` and
``symbolVal``. For example: ::
GHC.TypeLits> natVal (Proxy :: Proxy 2)
2
These functions are overloaded because they need to return a different
result, depending on the type at which they are instantiated. ::
natVal :: KnownNat n => proxy n -> Integer
-- instance KnownNat 0
-- instance KnownNat 1
-- instance KnownNat 2
-- ...
GHC discharges the constraint as soon as it knows what concrete
type-level literal is being used in the program. Note that this works
only for *literals* and not arbitrary type expressions. For example, a
constraint of the form ``KnownNat (a + b)`` will *not* be simplified to
``(KnownNat a, KnownNat b)``; instead, GHC will keep the constraint as
is, until it can simplify ``a + b`` to a constant value.
It is also possible to convert a run-time integer or string value to the
corresponding type-level literal. Of course, the resulting type literal
will be unknown at compile-time, so it is hidden in an existential type.
The conversion may be performed using ``someNatVal`` for integers and
``someSymbolVal`` for strings: ::
someNatVal :: Integer -> Maybe SomeNat
SomeNat :: KnownNat n => Proxy n -> SomeNat
The operations on strings are similar.
.. _typelit-tyfuns:
Computing With Type-Level Naturals
----------------------------------
GHC 7.8 can evaluate arithmetic expressions involving type-level natural
numbers. Such expressions may be constructed using the type-families
``(+), (*), (^)`` for addition, multiplication, and exponentiation.
Numbers may be compared using ``(<=?)``, which returns a promoted
boolean value, or ``(<=)``, which compares numbers as a constraint. For
example:
.. code-block:: none
GHC.TypeLits> natVal (Proxy :: Proxy (2 + 3))
5
At present, GHC is quite limited in its reasoning about arithmetic: it
will only evaluate the arithmetic type functions and compare the
results--- in the same way that it does for any other type function. In
particular, it does not know more general facts about arithmetic, such
as the commutativity and associativity of ``(+)``, for example.
However, it is possible to perform a bit of "backwards" evaluation. For
example, here is how we could get GHC to compute arbitrary logarithms at
the type level:
.. code-block:: none
lg :: Proxy base -> Proxy (base ^ pow) -> Proxy pow
lg _ _ = Proxy
GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8))
3
|
