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

TypeNats/Basics
v21 v22 36 36 tNat :: TNat n 37 37 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"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... 41 41 etc. 42 42 }}} … … 85 85 86 86 There are two different styles of writing functions which need the integer corresponding to a type level natural. 87 To illustrate the two style consider a type for working with Cstyle arrays: 88 {{{ 89 newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a) 90 }}} 87 91 88 One approach is to use an explicit parameter of type `Nat n`. For example:92 One approach is to use an explicit parameter of type {{{TNat n}}}. For example: 89 93 {{{ 90 memset :: Storable a => ArrPtr n a > a > Nat n > IO ()94 memset :: Storable a => ArrPtr n a > a > TNat n > IO () 91 95 memset = ... 92 96 }}} 93 97 94 98 This style is, basically, a more typed version of what is found in many standard C libraries. 95 Callers of this function have to pass the size of the array explicitly, and the type system checks that the size matches that of the array. 96 When defining `memset` we can just use `natToInteger` on the `Nat n` parameter to get the actual value of the array size. 99 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. When defining {{{memset}}} we can just use {{{tNatInteger}}}` on the {{{TNat n}}} 101 parameter to get the actual value of the array size. 97 102 98 103 Another approach is to let the system infer the parameter by using the class `NatI`. For example: 99 104 {{{ 100 105 memsetAuto :: (Storable a, NatI n) => ArrPtr n a > a > IO () 106 memsetAuto = ... 101 107 }}} 102 108 103 109 In this style, the caller of the function does not need to provide the size of the array explicitly. 104 110 Instead, it is computed automatically from the type of the array. 105 When defining `memsetAuto` we can use `nat`, the method of `NatI`, to get access to the value corresponding to the type level natural. 111 When defining {{{memsetAuto}}} we can use {{{{tNat}}}, the method of {{{NatI}}}, to get access to the value 112 corresponding to the type level natural. 106 113 107 When using the implicit style, it is important that the type of `nat`is specified precisely. Failing to do so typically results in ambiguity errors108 (i.e., GHC does not know which integer it should use). Another common mistake is to forget that ' nat' is a polymorphic value and so every time it is used it may refer to a different value.114 When using the implicit style, it is important that the type of {{{tNat}}} is specified precisely. Failing to do so typically results in ambiguity errors 115 (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. 109 116 110 An easy way to avoid such problems is to implement the implicit style functions in terms of the explicit ones. For example, we can implement `memsetAuto` like this: 117 An easy way to avoid such problems is to implement the implicit style functions in terms of the explicit ones. The 118 ba 111 119 {{{ 112 120 memsetAuto arr val = memset arr val nat 113 121 }}} 114