Changes between Version 4 and Version 5 of TypeNats/SingletonsAndExistentials


Ignore:
Timestamp:
Apr 17, 2012 8:34:31 PM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/SingletonsAndExistentials

    v4 v5  
    1 Consider a type for arrays with a statically known size. 
     1This example illustrates some choices that come up when 
     2using existential types in combination with singleton types. 
     3The choices are illustrated with an example, which 
     4defines a typed interface for working with array. 
     5(Constructors with existential types are written in 
     6GADT notation.) 
     7 
     8{{{ 
     9{-# LANGUAGE DataKinds, GADTs, KindSignatures #-} 
     10 
     11import Control.Monad(forM_) 
     12import GHC.TypeLits 
     13import Foreign(Ptr, pokeElemOff, Storable, mallocArray) 
     14}}} 
     15 
     16We start by defining a type for pointers to a ''sequence'' 
     17of adjecent elements in memory.  The number of elements 
     18is statically known at compile time, which is why 
     19we add it to the type of the pointer: 
     20 
    221{{{ 
    322newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a) 
     23}}} 
    424 
    5 memset_c :: ArrPtr n a -> a -> Sing n -> IO () 
     25Now we can define a function which sets all elements in 
     26the array to a specific value: 
     27{{{ 
     28memset_c :: Storable a => ArrPtr n a -> a -> Sing n -> IO () 
    629memset_c (ArrPtr p) a n = 
    730  forM_ [ 1 .. fromSing n - 1 ] $ \i -> 
    831    pokeElemOff p (fromIntegral i) a 
    9  
    10 memset :: SingI n => ArrPtr n a -> a -> IO () 
     32}}} 
     33Because the size of the array is statically known, we may 
     34define an overloaded function, that will use the correct 
     35size automatically, based on the type: 
     36{{{ 
     37memset :: (Storable a, SingI n) => ArrPtr n a -> a -> IO () 
    1138memset p a = withSing (memset_c p a) 
    1239}}} 
    1340 
    1441 
    15 {{{ 
     42 
     43 
     44 
    1645data ArrayS :: * -> * where 
    1746  ArrS :: Sing n -> ArrPtr n a -> ArrayS a 
    18 }}} 
    1947 
    20 {{{ 
    2148data ArrayD :: * -> * where 
    2249  ArrD :: SingI n => ArrPtr n a -> ArrayD a 
    23 }}} 
     50 
     51 
     52memsetS :: Storable a => ArrayS a -> a -> IO () 
     53memsetS (ArrS s p) a = memset_c p a s 
     54 
     55memsetD :: Storable a => ArrayD a -> a -> IO () 
     56memsetD (ArrD p) a = memset p a 
     57 
     58fromArrD :: ArrayD a -> ArrayS a 
     59fromArrD (ArrD p) = ArrS sing p 
     60 
     61 
     62-- Unsafe, in general. 
     63uncheckedSing :: Integral a => a -> Sing (n :: Nat) 
     64uncheckedSing a = Sing (toInteger a) 
     65 
     66mallocS :: Storable a => Int -> IO (ArrayS a) 
     67mallocS n = do p <- mallocArray n 
     68               return (ArrS (uncheckedSing n) (ArrPtr p)) 
     69 
     70example = do arr <- mallocS 10 
     71             memsetS arr (0 :: Int) 
     72             return arr