TypeNat- Some Nat-indexed types for GHC

Safe HaskellSafe-Inferred




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

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


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

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

A kind of fmap for Vect.

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

VCons to the end of a Vect.

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

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

listToVect :: IsNat n => [a] -> Maybe (Vect a n) 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 a l -> String Source