This example illustrates some choices that come up when using existential types in combination with singleton types. The choices are illustrated with an example, which defines a typed interface for working with array. (Constructors with existential types are written in GADT notation.) {{{ {-# LANGUAGE DataKinds, GADTs, KindSignatures #-} import Control.Monad(forM_) import GHC.TypeLits import Foreign(Ptr, pokeElemOff, Storable, mallocArray) }}} == Arrays with Statically Known Sizes == We start by defining a type for pointers to a ''sequence'' of adjacent elements in memory. The number of elements is statically known at compile time, which is why we add it to the type of the pointer: {{{ newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a) }}} Now we can define a function which sets all elements in the array to a specific value: {{{ memset_c :: Storable a => ArrPtr n a -> a -> Sing n -> IO () memset_c (ArrPtr p) a n = forM_ [ 1 .. fromSing n - 1 ] $ \i -> pokeElemOff p (fromIntegral i) a }}} Because the size of the array is statically known, we may define an overloaded function, that will use the correct size automatically, based on the type: {{{ memset :: (Storable a, SingI n) => ArrPtr n a -> a -> IO () memset p a = withSing (memset_c p a) }}} Here is an example of how we might use these types: {{{ clearPage :: ArrPtr 4096 Word8 -> IO () clearPage p = memset p 0 }}} Note that because of the way we wrote the code, there is no danger of accidentally passing the incorrect size for an array. == Hiding the Array Size with an Existential == We may also define a type for array whose sizes are not known statically. Such arrays have two components: a pointer to data, and a number storing how many elements there are in the array. There are two different ways to define such arrays, and the difference between these two choices is the central point of this example: {{{ data ArrayS :: * -> * where ArrS :: Sing n -> ArrPtr n a -> ArrayS a data ArrayD :: * -> * where ArrD :: SingI n => ArrPtr n a -> ArrayD a }}} The difference between the two is how we store the size of the array: in `ArrayS` we are using an explicit singleton values, while in `ArrayD` the size is stored in an implicit ''dictionary'' field. Both representations have the size of the array, so we can use them with the functions that we already defined for arrays of statically known sizes: {{{ memsetS :: Storable a => ArrayS a -> a -> IO () memsetS (ArrS s p) a = memset_c p a s memsetD :: Storable a => ArrayD a -> a -> IO () memsetD (ArrD p) a = memset p a }}} The interesting difference between the two is that `ArrayD` is (in some sense) ''more static''. In particular, we can always convert an `ArrayD` into an `ArrayS`, but we cannot define the inverse function: {{{ fromArrD :: ArrayD a -> ArrayS a fromArrD (ArrD p) = ArrS sing p }}} == Creating Dynamically Sized Arrays == {{{ -- Unsafe, in general. uncheckedSing :: Integral a => a -> Sing (n :: Nat) uncheckedSing a = Sing (toInteger a) mallocS :: Storable a => Int -> IO (ArrayS a) mallocS n = do p <- mallocArray n return (ArrS (uncheckedSing n) (ArrPtr p)) example = do arr <- mallocS 10 memsetS arr (0 :: Int) return arr }}}