{-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE StandaloneDeriving #-} module Data.TypeNat.Vect ( Vect(..) , vectMap , vectSnoc , vectToList , listToVect , showVect , module Data.TypeNat.Nat ) where import Data.TypeNat.Nat -- | Nat-indexed list, where the nat determines the length. data Vect :: Nat -> * -> * where VNil :: Vect Z a VCons :: a -> Vect n a -> Vect (S n) a deriving instance Eq a => Eq (Vect n a) deriving instance Show a => Show (Vect n a) instance Functor (Vect n) where fmap :: (a -> b) -> Vect n a -> Vect n b fmap = (a -> b) -> Vect n a -> Vect n b forall a b (n :: Nat). (a -> b) -> Vect n a -> Vect n b vectMap instance Foldable (Vect n) where foldr :: (a -> b -> b) -> b -> Vect n a -> b foldr a -> b -> b f b b Vect n a vect = case Vect n a vect of Vect n a VNil -> b b VCons a x Vect n a rest -> a -> b -> b f a x ((a -> b -> b) -> b -> Vect n a -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr a -> b -> b f b b Vect n a rest) instance Traversable (Vect n) where traverse :: (a -> f b) -> Vect n a -> f (Vect n b) traverse a -> f b f Vect n a vect = case Vect n a vect of Vect n a VNil -> Vect 'Z b -> f (Vect 'Z b) forall (f :: * -> *) a. Applicative f => a -> f a pure Vect 'Z b forall a. Vect 'Z a VNil VCons a x Vect n a rest -> b -> Vect n b -> Vect ('S n) b forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a VCons (b -> Vect n b -> Vect ('S n) b) -> f b -> f (Vect n b -> Vect ('S n) b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> f b f a x f (Vect n b -> Vect ('S n) b) -> f (Vect n b) -> f (Vect ('S n) b) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> (a -> f b) -> Vect n a -> f (Vect n b) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse a -> f b f Vect n a rest -- | A kind of fmap for Vect. vectMap :: (a -> b) -> Vect n a -> Vect n b vectMap :: (a -> b) -> Vect n a -> Vect n b vectMap a -> b f Vect n a vect = case Vect n a vect of Vect n a VNil -> Vect n b forall a. Vect 'Z a VNil VCons a x Vect n a v -> b -> Vect n b -> Vect ('S n) b forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a VCons (a -> b f a x) ((a -> b) -> Vect n a -> Vect n b forall a b (n :: Nat). (a -> b) -> Vect n a -> Vect n b vectMap a -> b f Vect n a v) -- | VCons to the end of a Vect. vectSnoc :: a -> Vect n a -> Vect (S n) a vectSnoc :: a -> Vect n a -> Vect ('S n) a vectSnoc a x Vect n a vect = case Vect n a vect of Vect n a VNil -> a -> Vect 'Z a -> Vect ('S 'Z) a forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a VCons a x Vect 'Z a forall a. Vect 'Z a VNil VCons a y Vect n a v -> a -> Vect ('S n) a -> Vect ('S ('S n)) a forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a VCons a y (a -> Vect n a -> Vect ('S n) a forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a vectSnoc a x Vect n a v) -- | Show a Vect. showVect :: Show a => Vect l a -> String showVect :: Vect l a -> String showVect Vect l a VNil = String "VNil" showVect (VCons a x Vect n a xs) = a -> String forall a. Show a => a -> String show a x String -> ShowS forall a. [a] -> [a] -> [a] ++ String " , " String -> ShowS forall a. [a] -> [a] -> [a] ++ Vect n a -> String forall a (n :: Nat). Show a => Vect n a -> String showVect Vect n a xs -- | Drop the length index from a Vect, giving a typical list. vectToList :: Vect n a -> [a] vectToList :: Vect n a -> [a] vectToList Vect n a v = case Vect n a v of Vect n a VNil -> [] VCons a x Vect n a xs -> a x a -> [a] -> [a] forall a. a -> [a] -> [a] : Vect n a -> [a] forall (n :: Nat) a. Vect n a -> [a] vectToList Vect n a xs -- | Used to implement listToVect through natRecursion. newtype MaybeVect a n = MV { MaybeVect a n -> Maybe (Vect n a) unMV :: Maybe (Vect n a) } -- | Try to produce a Vect from a list. The nat index must be fixed somehow, -- perhaps with the help of ScopedTypeVariables. listToVect:: IsNat n => [a] -> Maybe (Vect n a) listToVect :: [a] -> Maybe (Vect n a) listToVect = MaybeVect a n -> Maybe (Vect n a) forall a (n :: Nat). MaybeVect a n -> Maybe (Vect n a) unMV (MaybeVect a n -> Maybe (Vect n a)) -> ([a] -> MaybeVect a n) -> [a] -> Maybe (Vect n a) forall b c a. (b -> c) -> (a -> b) -> a -> c . [a] -> MaybeVect a n forall (n :: Nat) a. IsNat n => [a] -> MaybeVect a n listToVect' where listToVect':: IsNat n => [a] -> MaybeVect a n listToVect' :: [a] -> MaybeVect a n listToVect' = (forall (m :: Nat). [a] -> MaybeVect a m -> MaybeVect a ('S m)) -> ([a] -> MaybeVect a 'Z) -> ([a] -> [a]) -> [a] -> MaybeVect a n forall (n :: Nat) b (a :: Nat -> *). IsNat n => (forall (m :: Nat). b -> a m -> a ('S m)) -> (b -> a 'Z) -> (b -> b) -> b -> a n natRecursion forall a (m :: Nat). [a] -> MaybeVect a m -> MaybeVect a ('S m) forall (m :: Nat). [a] -> MaybeVect a m -> MaybeVect a ('S m) inductive [a] -> MaybeVect a 'Z forall a. [a] -> MaybeVect a 'Z base [a] -> [a] forall a. [a] -> [a] reduce inductive :: [a] -> MaybeVect a m -> MaybeVect a (S m) inductive :: [a] -> MaybeVect a m -> MaybeVect a ('S m) inductive [a] xs MaybeVect a m maybeVect = case MaybeVect a m maybeVect of MV Maybe (Vect m a) Nothing -> Maybe (Vect ('S m) a) -> MaybeVect a ('S m) forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n MV Maybe (Vect ('S m) a) forall a. Maybe a Nothing MV (Just Vect m a vect) -> case [a] xs of [] -> Maybe (Vect ('S m) a) -> MaybeVect a ('S m) forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n MV Maybe (Vect ('S m) a) forall a. Maybe a Nothing (a x : [a] _) -> Maybe (Vect ('S m) a) -> MaybeVect a ('S m) forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n MV (Vect ('S m) a -> Maybe (Vect ('S m) a) forall a. a -> Maybe a Just (a -> Vect m a -> Vect ('S m) a forall a (n :: Nat). a -> Vect n a -> Vect ('S n) a VCons a x Vect m a vect)) base :: [a] -> MaybeVect a Z base :: [a] -> MaybeVect a 'Z base [a] xs = case [a] xs of [] -> Maybe (Vect 'Z a) -> MaybeVect a 'Z forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n MV (Vect 'Z a -> Maybe (Vect 'Z a) forall a. a -> Maybe a Just Vect 'Z a forall a. Vect 'Z a VNil) [a] _ -> Maybe (Vect 'Z a) -> MaybeVect a 'Z forall a (n :: Nat). Maybe (Vect n a) -> MaybeVect a n MV Maybe (Vect 'Z a) forall a. Maybe a Nothing reduce :: [a] -> [a] reduce :: [a] -> [a] reduce [a] xs = case [a] xs of [] -> [] (a x : [a] xs) -> [a] xs