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
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 adata 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
memsetS :: Storable a => ArrayS a -> a -> IO ()memsetS (ArrS s p) a = memset_c p a smemsetD :: 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 afromArrD (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