wiki:TypeNats/Basics

Version 27 (modified by diatchki, 2 years ago) (diff)

--

Type-Level Naturals

There is a new kind, Nat. It is completely separate from GHC's hierarchy of sub-kinds, so Nat is only a sub-kind of itself.

The inhabitants of Nat are an infinite family of (empty) types, corresponding to the natural numbers:

0, 1, 2, ... :: Nat

These types are linked to the value world by a small library with the following API:

module GHC.TypeLits where

Singleton Types

We relate type-level natural numbers to run-time values via a family of singleton types:

data TNat :: Nat -> *

tNat         :: NatI n => TNat n
tNatInteger  :: TNat n -> Integer

-- Convenient derived functions
tNatThat     :: NatI n => (Integer -> Bool) -> Maybe (TNat n)
withTNat     :: NatI n => (TNat n -> a) -> a

The only "interesting" value of type TNat n is the number n. Technically, there is also an undefined element. The value of a singleton type may be named using tNat, which is a bit like a "smart" constructor for TNat n. Note that because tNat is polymorphic, we may have to use a type signature to specify which singleton we mean. For example:

> :set -XDataKinds
> tNatInteger (tNat :: TNat 3)
3

One may think of the smart constructor tNat as being a method of a special built-in class, NatI:

class NatI n where
  tNat :: TNat n

instance NatI 0 where tNat = ...singleton 0 value...
instance NatI 1 where tNat = ...singleton 1 value...
instance NatI 2 where tNat = ...singleton 2 value...
etc.

The name NatI is a mnemonic for the different uses of the class:

  • It is the introduction construct for 'TNat' values,
  • It is an implicit parameter of kind 'TNat' (this is discussed in more detail bellow)

Examples

Here is how we can use the basic primitives to define a Show instance for singleton types:

instance Show (TNat n) where
  showsPrec p n = showsPrec p (tNatInteger n)

Here is how to define a Read instance:

instance NatI n => Read (Nat n) where
  readsPrec p x       = do (x,xs) <- readsPrec p x
                           case tNatThat (== x) of
                             Just n  -> [(n,xs)]
                             Nothing -> []

The derived function tNatThat is similar to tNat except that it succeeds only if the integer representation of the singleton type matches the given predicate. So, in the Read instance we parse an integer and then we check if it is the expected integer for the singleton that we are trying to parse.

Implicit vs. Explicit Parameters

There are two different styles of writing functions which need the integer corresponding to a type level natural. To illustrate the two style consider a type for working with C-style arrays:

newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)

One approach is to use an explicit parameter of type TNat n. For example:

memset_c :: Storable a => ArrPtr n a -> a -> TNat n -> IO ()
memset_c (ArrPtr p) a n = mapM_ (\i -> pokeElemOff p i a) [ 0 .. fromIntegral (tNatInteger n - 1) ]

This style is, basically, a more typed version of what is found in many standard C libraries. Callers of this function have to pass the size of the array explicitly, and the type system checks that the size matches that of the array. Note that in the implementation of memset_c we used tNatInteger to get the concrete integer associated with the singleton type.

While the explicit TNat parameter is convenient when we define the function, it is a bit tedious to have to provide it all the time---it is easier to let the system infer the value, based on the type of the array:

memset :: (Storable a, NatI n) => ArrPtr n a -> a -> IO ()
memset ptr a = withTNat (memset_c ptr a)

The function withTNat is useful when converting from the "explicit" to the "implicit" style because it avoids ambiguity errors, scoped type-variables and other complications.