Changes between Version 6 and Version 7 of TypeNats/SingletonsAndExistentials
 Timestamp:
 Apr 17, 2012 8:51:12 PM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/SingletonsAndExistentials
v6 v7 55 55 == Hiding the Arrays Size with an Existential == 56 56 57 We may also define a type for array whose sizes 58 are not known statically. Such arrays have 59 two components: a pointer to data, and a number 60 storing how many elements there are in the array. 57 61 58 62 There are two different ways to define such arrays, 63 and the difference between these two choices is 64 the central point of this example: 65 {{{ 59 66 data ArrayS :: * > * where 60 67 ArrS :: Sing n > ArrPtr n a > ArrayS a … … 62 69 data ArrayD :: * > * where 63 70 ArrD :: SingI n => ArrPtr n a > ArrayD a 71 }}} 72 The difference between the two is how we 73 store the size of the array: in `ArrayS` we 74 are using an explicit singleton values, 75 while in `ArrayD` the size is stored 76 in an implicit ''dictionary'' field. 64 77 65 78 Both representations have the size of the 79 array, so we can use them with the functions 80 that we already defined for arrays of statically 81 known sizes: 82 {{{ 66 83 memsetS :: Storable a => ArrayS a > a > IO () 67 84 memsetS (ArrS s p) a = memset_c p a s … … 69 86 memsetD :: Storable a => ArrayD a > a > IO () 70 87 memsetD (ArrD p) a = memset p a 88 }}} 71 89 90 The interesting difference between the two 91 is the `ArrayD` is (in some sense) ''more static''. 92 In particular, we can always convert 93 an `ArrayD` into an `ArrayS`, but we cannot 94 define the inverse function: 95 {{{ 72 96 fromArrD :: ArrayD a > ArrayS a 73 97 fromArrD (ArrD p) = ArrS sing p 98 }}} 74 99 75 100 101 102 103 == Creating Dynamically Sized Arrays == 104 105 {{{ 76 106  Unsafe, in general. 77 107 uncheckedSing :: Integral a => a > Sing (n :: Nat) … … 85 115 memsetS arr (0 :: Int) 86 116 return arr 117 }}}