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.