Changes between Version 4 and Version 5 of TypeNats/SingletonsAndExistentials


Ignore:
Timestamp:
Apr 17, 2012 8:34:31 PM (3 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