Version 5 (modified by diatchki, 3 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)

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)

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