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 XDataKinds
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 Section 7.3.26.4, “Explicit namespaces in import/export”).
Here is an exampe 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")
Sometimes it is useful to access the value-level literal assocaited 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.
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:
GHC.TypeLits> natVal (Proxy :: Proxy (2 + 3)) 5
At present, GHC is quite limited in its reasoning about arithmetic:
it will only evalute 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:
lg :: Proxy base -> Proxy (base ^ pow) -> Proxy pow lg _ _ = Proxy GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8)) 3