TypeNat-0.5.0.0: Some Nat-indexed types for GHC

Safe HaskellNone
LanguageHaskell2010

Data.TypeNat.Vect

Synopsis

Documentation

data Vect :: Nat -> * -> * where Source #

Nat-indexed list, where the nat determines the length.

Constructors

VNil :: Vect Z a 
VCons :: a -> Vect n a -> Vect (S n) a 

Instances

Functor (Vect n) Source # 

Methods

fmap :: (a -> b) -> Vect n a -> Vect n b #

(<$) :: a -> Vect n b -> Vect n a #

Foldable (Vect n) Source # 

Methods

fold :: Monoid m => Vect n m -> m #

foldMap :: Monoid m => (a -> m) -> Vect n a -> m #

foldr :: (a -> b -> b) -> b -> Vect n a -> b #

foldr' :: (a -> b -> b) -> b -> Vect n a -> b #

foldl :: (b -> a -> b) -> b -> Vect n a -> b #

foldl' :: (b -> a -> b) -> b -> Vect n a -> b #

foldr1 :: (a -> a -> a) -> Vect n a -> a #

foldl1 :: (a -> a -> a) -> Vect n a -> a #

toList :: Vect n a -> [a] #

null :: Vect n a -> Bool #

length :: Vect n a -> Int #

elem :: Eq a => a -> Vect n a -> Bool #

maximum :: Ord a => Vect n a -> a #

minimum :: Ord a => Vect n a -> a #

sum :: Num a => Vect n a -> a #

product :: Num a => Vect n a -> a #

Traversable (Vect n) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Vect n a -> f (Vect n b) #

sequenceA :: Applicative f => Vect n (f a) -> f (Vect n a) #

mapM :: Monad m => (a -> m b) -> Vect n a -> m (Vect n b) #

sequence :: Monad m => Vect n (m a) -> m (Vect n a) #

Eq a => Eq (Vect n a) Source # 

Methods

(==) :: Vect n a -> Vect n a -> Bool #

(/=) :: Vect n a -> Vect n a -> Bool #

Show a => Show (Vect n a) Source # 

Methods

showsPrec :: Int -> Vect n a -> ShowS #

show :: Vect n a -> String #

showList :: [Vect n a] -> ShowS #

vectMap :: (a -> b) -> Vect n a -> Vect n b Source #

A kind of fmap for Vect.

vectSnoc :: a -> Vect n a -> Vect (S n) a Source #

VCons to the end of a Vect.

vectToList :: Vect n a -> [a] Source #

Drop the length index from a Vect, giving a typical list.

listToVect :: IsNat n => [a] -> Maybe (Vect n a) Source #

Try to produce a Vect from a list. The nat index must be fixed somehow, perhaps with the help of ScopedTypeVariables.

showVect :: Show a => Vect l a -> String Source #

Show a Vect.