Changes between Version 6 and Version 7 of TypeNats/SingletonsAndExistentials
- Timestamp:
- 04/17/12 13:51:12 (13 months 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 }}}
