Changes between Version 24 and Version 25 of TypeNats/Basics
 Timestamp:
 Mar 21, 2012 1:07:26 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v24 v25 21 21 tNat :: NatI n => TNat n 22 22 tNatInteger :: TNat n > Integer 23 24  Convenient derived functions 25 tNatThat :: NatI n => (Integer > Bool) > Maybe (TNat n) 26 withTNat :: NatI n => (TNat n > a) > a 23 27 }}} 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:28 The only "interesting" value of type {{{TNat n}}} is the number {{{n}}}. Technically, there is also an undefined element. 29 The value of a singleton type may be named using {{{tNat}}}, which is a bit like a "smart" constructor for {{{TNat n}}}. 30 Note that because {{{tNat}}} is polymorphic, we may have to use a type signature to specify which singleton we mean. For example: 27 31 {{{ 28 32 > :set XDataKinds … … 31 35 }}} 32 36 33 One may think of the smart constructor ''tNat'' as being a method of a special builtin class, ''NatI'':37 One may think of the smart constructor {{{tNat}}} as being a method of a special builtin class, {{{NatI}}}: 34 38 {{{ 35 39 class NatI n where … … 48 52 == Examples == 49 53 50 Here is how we can use the basic primitives to define a `Show`instance for singleton types:54 Here is how we can use the basic primitives to define a {{{Show}}} instance for singleton types: 51 55 {{{ 52 56 instance Show (TNat n) where … … 54 58 }}} 55 59 56 A more interesting example is to define a function which maps integers into singleton types: 57 {{{ 58 integerToMaybeNat :: NatI n => Integer > Maybe (TNat n) 59 integerToMaybeNat x = tNatThat (== x) 60 }}} 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. 62 63 The implementation of `integerToMaybeNat` is a little subtle: by using 64 the helper function `check`, we ensure that the two occurrences of 65 `nat` (aka `y`) both have the same type, namely `Nat n`. There are other 66 ways to achieve the same, for example, by using scoped type variables, 67 thus: 68 {{{ 69 integerToMaybeNat :: forall n. NatI n => Integer > Maybe (Nat n) 70 integerToMaybeNat x 71  x == natToInteger (nat :: Nat n) = Just nat 72  otherwise = Nothing 73 }}} 74 75 Now, we can use `integerToNat` to provide a `Read` instance for singleton types: 60 Here is how to define a {{{Read}}} instance: 76 61 {{{ 77 62 instance NatI n => Read (Nat n) where 78 63 readsPrec p x = do (x,xs) < readsPrec p x 79 case integerToMaybeNat xof64 case tNatThat (== x) of 80 65 Just n > [(n,xs)] 81 66 Nothing > [] 82 67 }}} 68 69 The derived function {{{tNatThat}}} is similar to {{{tNat}}} except that it succeeds only if the integer representation 70 of the singleton type matches the given predicate. So, in the {{{Read}}} instance we parse an integer and then we check 71 if it is the expected integer for the singleton that we are trying to parse. 72 83 73 84 74 == Implicit vs. Explicit Parameters == … … 92 82 One approach is to use an explicit parameter of type {{{TNat n}}}. For example: 93 83 {{{ 94 memset :: Storable a => ArrPtr n a > a > TNat n > IO ()95 memset (ArrPtr p) a n = mapM_ (\i > pokeElemOff p i a) [ 0 .. fromIntegral (tNatInteger n  1) ]84 memset_c :: Storable a => ArrPtr n a > a > TNat n > IO () 85 memset_c (ArrPtr p) a n = mapM_ (\i > pokeElemOff p i a) [ 0 .. fromIntegral (tNatInteger n  1) ] 96 86 }}} 97 87 98 88 This style is, basically, a more typed version of what is found in many standard C libraries. 99 89 Callers of this function have to pass the size of the array explicitly, and the type system checks that the 100 size matches that of the array. Note that in the implementation of {{{memset }}} we used {{{tNatInteger}}}90 size matches that of the array. Note that in the implementation of {{{memset_c}}} we used {{{tNatInteger}}} 101 91 to get the concrete integer associated with the singleton type. 102 92 103 93 Another approach is to let the system infer the parameter by using the class {{{NatI}}}. For example: 104 94 {{{ 105 memset Auto:: (Storable a, NatI n) => ArrPtr n a > a > IO ()106 memset Auto ptr a = withTNat (memsetarr a)95 memset :: (Storable a, NatI n) => ArrPtr n a > a > IO () 96 memset ptr a = withTNat (memset_c arr a) 107 97 }}} 108 98 … … 115 105 (i.e., GHC does not know which integer it should use). Another common mistake is to forget that 'tNat' is a polymorphic value and so every time it is used it may refer to a different value. 116 106 117 An easy way to avoid such problems is to implement the implicit style functions in terms of the explicit ones. The118 ba119 {{{120 memsetAuto arr val = memset arr val nat121 }}}