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

Sing n -> ArrPtr n a -> ArrayS a

data ArrayD :: * -> * where

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