Changes between Version 20 and Version 21 of TypeNats/Basics
 Timestamp:
 Mar 21, 2012 12:39:35 AM (6 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v20 v21 10 10 These types are linked to the value world by a small library with the following API: 11 11 {{{ 12 module GHC.Type Nats where12 module GHC.TypeLits where 13 13 }}} 14 14 … … 17 17 We relate typelevel natural numbers to runtime values via a family of singleton types: 18 18 {{{ 19 data Nat (n :: Nat)19 data TNat (n :: Nat) 20 20 21 nat :: NatI n =>Nat n22 natToInteger ::Nat n > Integer21 tNat :: NatI n => TNat n 22 tNatInteger :: TNat n > Integer 23 23 }}} 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:24 The only "interesting" value of type ''TNat n'' is the number ''n''. Technically, there is also an undefined element. 25 The value of a singleton type may be named using ''tNat'', which is a bit like a "smart" constructor for ''TNat n''. 26 Note that because ''tNat'' is polymorphic, we may have to use a type signature to specify which singleton we mean. For example: 27 27 {{{ 28 > natToInteger (nat :: Nat 3) 28 > :set XDataKinds 29 > tNatInteger (tNat :: TNat 3) 29 30 3 30 31 }}} 31 32 32 One may think of the smart constructor '' nat'' as being a method of a special builtin class, ''NatI'':33 One may think of the smart constructor ''tNat'' as being a method of a special builtin class, ''NatI'': 33 34 {{{ 34 35 class NatI n where 35 nat ::Nat n36 tNat :: TNat n 36 37 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"38 instance NatI 0 where tNat = "singleton 0 value" 39 instance NatI 1 where tNat = "singleton 1 value" 40 instance NatI 2 where tNat = "singleton 2 value" 40 41 etc. 41 42 }}} 42 43 43 44 The 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) 46 47 47 48 == Examples == … … 49 50 Here is how we can use the basic primitives to define a `Show` instance for singleton types: 50 51 {{{ 51 instance Show ( Nat n) where52 showsPrec p n = showsPrec p ( natToInteger n)52 instance Show (TNat n) where 53 showsPrec p n = showsPrec p (tNatInteger n) 53 54 }}} 54 55 55 56 A more interesting example is to define a function which maps integers into singleton types: 56 57 {{{ 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 58 integerToMaybeNat :: NatI n => Integer > Maybe (TNat n) 59 integerToMaybeNat x = tNatThat (== x) 60 60 }}} 61 61 It checks that the value argument `x`, passed at runtime, matches the staticallyexpected value, returning `Nothing` if not, and a typed singleton if so.