GitLab

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