6.4.13. 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
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
(+)). Import and export declarations referring to
these operators require an explicit namespace annotation (see
Explicit namespaces in import/export).
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")
220.127.116.11. 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
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.
18.104.22.168. 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
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:
lg :: Proxy base -> Proxy (base ^ pow) -> Proxy pow lg _ _ = Proxy GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8)) 3