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