Changes between Version 33 and Version 34 of TypeNats/Basics
 Timestamp:
 Apr 9, 2012 2:13:08 AM (3 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v33 v34 127 127 128 128 129 130 131 132 133 134 == Examples ==135 136 Here is how we can use the basic primitives to define a {{{Show}}} instance for singleton types:137 {{{138 instance Show (TNat n) where139 showsPrec p n = showsPrec p (tNatInteger n)140 }}}141 142 Here is how to define a {{{Read}}} instance:143 {{{144 instance NatI n => Read (Nat n) where145 readsPrec p x = do (x,xs) < readsPrec p x146 case tNatThat (== x) of147 Just n > [(n,xs)]148 Nothing > []149 }}}150 151 The derived function {{{tNatThat}}} is similar to {{{tNat}}} except that it succeeds only if the integer representation152 of the singleton type matches the given predicate. So, in the {{{Read}}} instance we parse an integer and then we check153 if it is the expected integer for the singleton that we are trying to parse.154 155 156 129 == Implicit vs. Explicit Parameters == 157 130 158 There are two different styles of writing functions which need the integer corresponding to a type level natural.131 There are two different styles of writing functions that use singleton types. 159 132 To illustrate the two style consider a type for working with Cstyle arrays: 160 133 {{{ … … 162 135 }}} 163 136 164 One approach is to use an explicit parameter of type {{{TNat n}}}. For example: 137 Now consider the definition of the function `memset`, which sets all elemnts 138 of the array to a given fixed value. 139 140 One approach is to use an explicit singleton parameter. For example: 165 141 {{{ 166 memset_c :: Storable a => ArrPtr n a > a > TNatn > IO ()167 memset_c (ArrPtr p) a n = mapM_ (\i > pokeElemOff p i a) [ 0 .. fromIntegral (tNatInteger n 1) ]142 memset_c :: Storable a => ArrPtr n a > a > Sing n > IO () 143 memset_c (ArrPtr p) a size = mapM_ (\i > pokeElemOff p i a) [ 0 .. fromIntegral (fromSing size  1) ] 168 144 }}} 169 145 170 146 This style is, basically, a more typed version of what is found in many standard C libraries. 171 147 Callers of this function have to pass the size of the array explicitly, and the type system checks that the 172 size matches that of the array. Note that in the implementation of {{{memset_c}}} we used {{{tNatInteger}}} 173 to get the concrete integer associated with the singleton type. 148 size matches that of the array. Note that in the implementation of `memset_c` we used `fromSing` 149 to get the concrete integer associated with the singleton type, so that we know how many elements 150 to set with the given value/ 174 151 175 While the explicit {{{TNat}}}parameter is convenient when we define the function, it is a bit176 tedious to have to provide it all the timeit is easier to let the systeminfer the value,152 While the explicit `Sing` parameter is convenient when we define the function, it is a bit 153 tedious to have to provide it all the timeit is easier to let the compiler infer the value, 177 154 based on the type of the array: 178 155 {{{ 179 memset :: (Storable a, NatI n) => ArrPtr n a > a > IO ()180 memset ptr a = with TNat(memset_c ptr a)156 memset :: (Storable a, SingI n) => ArrPtr n a > a > IO () 157 memset ptr a = withSing (memset_c ptr a) 181 158 }}} 182 183 The function {{{withTNat}}} is useful when converting from the "explicit" to the "implicit" style184 because it avoids ambiguity errors, scoped typevariables and other complications.