module Data.VecN ( VecN(..)
, head
, tail) where
import Prelude hiding (head, tail)
import Data.Peano
import Data.Foldable
import Data.Monoid
import Control.Applicative
data VecN p a where
VecZero :: VecN Zero a
(:>) :: a -> VecN p a -> VecN (Succ p) a
instance (Eq a) => Eq (VecN Zero a) where
_ == _ = True
instance (Eq a, Eq (VecN p a)) => Eq (VecN (Succ p) a) where
(a :> as) == (b :> bs) = a == b && as == bs
instance (Ord a) => Ord (VecN Zero a) where
_ <= _ = True
instance (Ord a, Ord (VecN p a)) => Ord (VecN (Succ p) a) where
(a :> as) <= (b :> bs) = a <= b && as <= bs
instance (Show a) => Show (VecN Zero a) where
show _ = "VecZero"
instance (Show a, Show (VecN p a)) => Show (VecN (Succ p) a) where
show (a :> as) = show a ++ " :> " ++ show as
instance Functor (VecN Zero) where
fmap _ _ = VecZero
instance (Functor (VecN p)) => Functor (VecN (Succ p)) where
fmap f (a :> as) = f a :> fmap f as
instance Foldable (VecN Zero) where
foldMap _ VecZero = mempty
instance (Foldable (VecN p)) => Foldable (VecN (Succ p)) where
foldMap f (a :> as) = f a `mappend` foldMap f as
instance Applicative (VecN Zero) where
pure _ = VecZero
_ <*> _ = VecZero
instance (Applicative (VecN p)) => Applicative (VecN (Succ p)) where
pure a = a :> pure a
(f :> fs) <*> (a :> as) = f a :> (fs <*> as)
tail :: VecN (Succ p) a -> VecN p a
tail (_ :> as) = as
head :: VecN (Succ p) a -> a
head (a :> _) = a