Changes between Version 5 and Version 6 of TypeNats/SingletonsAndExistentials


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

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/SingletonsAndExistentials

    v5 v6  
    1313import Foreign(Ptr, pokeElemOff, Storable, mallocArray)
    1414}}}
     15
     16== Arrays with Statically Known Sizes ==
    1517
    1618We start by defining a type for pointers to a ''sequence''
     
    3133    pokeElemOff p (fromIntegral i) a
    3234}}}
     35
    3336Because the size of the array is statically known, we may
    3437define an overloaded function, that will use the correct
     
    3942}}}
    4043
     44Here is an example of how we might use these types:
     45{{{
     46clearPage :: ArrPtr 4096 Word8 -> IO ()
     47clearPage p = memset p 0
     48}}}
     49Note that because of the way we wrote the code,
     50there is no danger of accidentally passing the
     51incorrect size for an array.
    4152
     53
     54
     55== Hiding the Arrays Size with an Existential ==
    4256
    4357