wiki:TypeNats/SingletonsAndExistentials

Version 6 (modified by diatchki, 2 years ago) (diff)

--

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 adjecent 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 Arrays Size with an Existential

data ArrayS :: * -> * where

ArrS
Sing n -> ArrPtr? n a -> ArrayS a

data ArrayD :: * -> * where

ArrD
SingI n => ArrPtr? n a -> ArrayD a

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

fromArrD :: ArrayD a -> ArrayS a fromArrD (ArrD p) = ArrS sing p

-- 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