{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators#-}
{-# LANGUAGE ScopedTypeVariables #-}
module WithVector where
import Data.Maybe
import Data.Proxy
import GHC.TypeLits
import Unsafe.Coerce
data Vector :: Nat -> * -> * where
Nil :: Vector 0 a
(:>) :: a -> Vector n a -> Vector (n + 1) a
infixr 5 :>
data SNat :: Nat -> * where
SZero :: SNat 0
SSucc :: SNat n -> SNat (n + 1)
snat :: forall proxy n . KnownNat n => proxy n -> SNat n
snat = snat' . natVal
where
snat' :: Integer -> SNat m
snat' 0 = unsafeCoerce SZero
snat' n = unsafeCoerce (SSucc (snat' (n-1)))
vreplicate :: SNat n -> a -> Vector n a
vreplicate SZero _ = Nil
vreplicate (SSucc n) a = a :> vreplicate n a
asVector :: KnownNat n => proxy n -> [a] -> Vector n a
asVector s as = asVector' as (vreplicate (snat s) undefined)
where
asVector' :: [a] -> Vector m b -> Vector m a
asVector' _ Nil = Nil
asVector' [] (_ :> _ ) = error "static/dynamic mismatch"
asVector' (x:xs) (_ :> vs) = x :> asVector' xs vs
withVector :: forall a b . [a] -> (forall n . KnownNat n => Vector n a -> b) -> b
withVector xs f = case sn of SomeNat s -> f (asVector s xs)
where
sn = fromMaybe (error "static/dynamic mismatch") (someNatVal (toInteger (length xs)))
vlength :: forall n a . KnownNat n => Vector n a -> Integer
vlength _ = natVal (Proxy :: Proxy n)