Changes between Version 20 and Version 21 of TypeNats/Basics


Ignore:
Timestamp:
Mar 21, 2012 12:39:35 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v20 v21  
    1010These types are linked to the value world by a small library with the following API:
    1111{{{
    12 module GHC.TypeNats where
     12module GHC.TypeLits where
    1313}}}
    1414
     
    1717We relate type-level natural numbers to run-time values via a family of singleton types:
    1818{{{
    19 data Nat (n :: Nat)
     19data TNat (n :: Nat)
    2020
    21 nat          :: NatI n => Nat n
    22 natToInteger :: Nat n -> Integer
     21tNat         :: NatI n => TNat n
     22tNatInteger  :: TNat n -> Integer
    2323}}}
    24 The only "interesting" value of type ''Nat n'' is the number ''n''.  Technically, there is also an undefined element.
    25 The value of a singleton type may be named using ''nat'', which is a bit like a "smart" constructor for ''Nat n''.
    26 Note that because ''nat'' is polymorphic, we may have to use a type signature to specify which singleton we mean.  For example:
     24The only "interesting" value of type ''TNat n'' is the number ''n''.  Technically, there is also an undefined element.
     25The value of a singleton type may be named using ''tNat'', which is a bit like a "smart" constructor for ''TNat n''.
     26Note that because ''tNat'' is polymorphic, we may have to use a type signature to specify which singleton we mean.  For example:
    2727{{{
    28 > natToInteger (nat :: Nat 3)
     28> :set -XDataKinds
     29> tNatInteger (tNat :: TNat 3)
    29303
    3031}}}
    3132
    32 One may think of the smart constructor ''nat'' as being a method of a special built-in class, ''NatI'':
     33One may think of the smart constructor ''tNat'' as being a method of a special built-in class, ''NatI'':
    3334{{{
    3435class NatI n where
    35   nat :: Nat n
     36  tNat :: TNat n
    3637
    37 instance NatI 0 where nat = "singleton 0 value"
    38 instance NatI 1 where nat = "singleton 1 value"
    39 instance NatI 2 where nat = "singleton 2 value"
     38instance NatI 0 where tNat = "singleton 0 value"
     39instance NatI 1 where tNat = "singleton 1 value"
     40instance NatI 2 where tNat = "singleton 2 value"
    4041etc.
    4142}}}
    4243
    4344The name ''NatI'' is a mnemonic for the different uses of the class:
    44   * It is the ''introduction'' construct for 'Nat' values,
    45   * It is an ''implicit'' parameter of kind 'Nat' (this is discussed in more detail bellow)
     45  * It is the ''introduction'' construct for 'TNat' values,
     46  * It is an ''implicit'' parameter of kind 'TNat' (this is discussed in more detail bellow)
    4647
    4748== Examples ==
     
    4950Here is how we can use the basic primitives to define a `Show` instance for singleton types:
    5051{{{
    51 instance Show (Nat n) where
    52   showsPrec p n = showsPrec p (natToInteger n)
     52instance Show (TNat n) where
     53  showsPrec p n = showsPrec p (tNatInteger n)
    5354}}}
    5455
    5556A more interesting example is to define a function which maps integers into singleton types:
    5657{{{
    57 integerToMaybeNat :: NatI n => Integer -> Maybe (Nat n)
    58 integerToMaybeNat x = check nat
    59   where check y = if x == natToInteger y then Just y else Nothing
     58integerToMaybeNat :: NatI n => Integer -> Maybe (TNat n)
     59integerToMaybeNat x = tNatThat (== x)
    6060}}}
    6161It checks that the value argument `x`, passed at runtime, matches the statically-expected value, returning `Nothing` if not, and a typed singleton if so.