1 | | Consider a type for arrays with a statically known size. |
| 1 | This example illustrates some choices that come up when |
| 2 | using existential types in combination with singleton types. |
| 3 | The choices are illustrated with an example, which |
| 4 | defines a typed interface for working with array. |
| 5 | (Constructors with existential types are written in |
| 6 | GADT notation.) |
| 7 | |
| 8 | {{{ |
| 9 | {-# LANGUAGE DataKinds, GADTs, KindSignatures #-} |
| 10 | |
| 11 | import Control.Monad(forM_) |
| 12 | import GHC.TypeLits |
| 13 | import Foreign(Ptr, pokeElemOff, Storable, mallocArray) |
| 14 | }}} |
| 15 | |
| 16 | We start by defining a type for pointers to a ''sequence'' |
| 17 | of adjecent elements in memory. The number of elements |
| 18 | is statically known at compile time, which is why |
| 19 | we add it to the type of the pointer: |
| 20 | |
23 | | }}} |
| 50 | |
| 51 | |
| 52 | memsetS :: Storable a => ArrayS a -> a -> IO () |
| 53 | memsetS (ArrS s p) a = memset_c p a s |
| 54 | |
| 55 | memsetD :: Storable a => ArrayD a -> a -> IO () |
| 56 | memsetD (ArrD p) a = memset p a |
| 57 | |
| 58 | fromArrD :: ArrayD a -> ArrayS a |
| 59 | fromArrD (ArrD p) = ArrS sing p |
| 60 | |
| 61 | |
| 62 | -- Unsafe, in general. |
| 63 | uncheckedSing :: Integral a => a -> Sing (n :: Nat) |
| 64 | uncheckedSing a = Sing (toInteger a) |
| 65 | |
| 66 | mallocS :: Storable a => Int -> IO (ArrayS a) |
| 67 | mallocS n = do p <- mallocArray n |
| 68 | return (ArrS (uncheckedSing n) (ArrPtr p)) |
| 69 | |
| 70 | example = do arr <- mallocS 10 |
| 71 | memsetS arr (0 :: Int) |
| 72 | return arr |