Changes between Version 6 and Version 7 of TypeNats/SingletonsAndExistentials


Ignore:
Timestamp:
Apr 17, 2012 8:51:12 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/SingletonsAndExistentials

    v6 v7  
    5555== Hiding the Arrays Size with an Existential ==
    5656
     57We may also define a type for array whose sizes
     58are not known statically.  Such arrays have
     59two components: a pointer to data, and a number
     60storing how many elements there are in the array.
    5761
    58 
     62There are two different ways to define such arrays,
     63and the difference between these two choices is
     64the central point of this example:
     65{{{
    5966data ArrayS :: * -> * where
    6067  ArrS :: Sing n -> ArrPtr n a -> ArrayS a
     
    6269data ArrayD :: * -> * where
    6370  ArrD :: SingI n => ArrPtr n a -> ArrayD a
     71}}}
     72The difference between the two is how we
     73store the size of the array: in `ArrayS` we
     74are using an explicit singleton values,
     75while in `ArrayD` the size is stored
     76in an implicit ''dictionary'' field.
    6477
    65 
     78Both representations have the size of the
     79array, so we can use them with the functions
     80that we already defined for arrays of statically
     81known sizes:
     82{{{
    6683memsetS :: Storable a => ArrayS a -> a -> IO ()
    6784memsetS (ArrS s p) a = memset_c p a s
     
    6986memsetD :: Storable a => ArrayD a -> a -> IO ()
    7087memsetD (ArrD p) a = memset p a
     88}}}
    7189
     90The interesting difference between the two
     91is the `ArrayD` is (in some sense) ''more static''.
     92In particular, we can always convert
     93an `ArrayD` into an `ArrayS`, but we cannot
     94define the inverse function:
     95{{{
    7296fromArrD :: ArrayD a -> ArrayS a
    7397fromArrD (ArrD p) = ArrS sing p
     98}}}
    7499
    75100
     101
     102
     103== Creating Dynamically Sized Arrays ==
     104
     105{{{
    76106-- Unsafe, in general.
    77107uncheckedSing :: Integral a => a -> Sing (n :: Nat)
     
    85115             memsetS arr (0 :: Int)
    86116             return arr
     117}}}