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