Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Vector

Description

Vec and its combinator analog VecT represent lists of known length, characterized by the index (n :: N) in Vec n a or VecT n f a.

The classic example used ad nauseum for type-level programming.

The operations on Vec and VecT correspond to the type level arithmetic operations on the kind N.

Documentation

data VecT n f :: k -> * where Source #

Constructors

ØV :: VecT Z f a
(:*) :: !(f a) -> !(VecT n f a) -> VecT (S n) f a infixr 4

Instances

Traversable1 l l (VecT l n) Source #
Methods traverse1 :: Applicative h => (forall a. f a -> h (g a)) -> t f b -> h (t g b) Source #
Foldable1 l l (VecT l n) Source #
Methods foldMap1 :: Monoid m => (forall a. f a -> m) -> t f b -> m Source #
Functor1 l l (VecT l n) Source #
Methods map1 :: (forall a. f a -> g a) -> t f b -> t g b Source #
Witness ØC (Known N Nat n) (VecT k n f a) Source #
Associated Types type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (VecT k n f a) :: Constraint Source # Methods (\\) :: ØC => (Known N Nat n -> r) -> VecT k n f a -> r Source #
(Monad f, Known N Nat n) => Monad (VecT * n f) Source #
Methods (>>=) :: VecT * n f a -> (a -> VecT * n f b) -> VecT * n f b # (>>) :: VecT * n f a -> VecT * n f b -> VecT * n f b # return :: a -> VecT * n f a # fail :: String -> VecT * n f a #
Functor f => Functor (VecT * n f) Source #
Methods fmap :: (a -> b) -> VecT * n f a -> VecT * n f b # (<$) :: a -> VecT * n f b -> VecT * n f a #
(Applicative f, Known N Nat n) => Applicative (VecT * n f) Source #
Methods pure :: a -> VecT * n f a # (<>) :: VecT n f (a -> b) -> VecT * n f a -> VecT * n f b # (>) :: VecT n f a -> VecT * n f b -> VecT * n f b # (<) :: VecT n f a -> VecT * n f b -> VecT * n f a #
Foldable f => Foldable (VecT * n f) Source #
Methods fold :: Monoid m => VecT * n f m -> m # foldMap :: Monoid m => (a -> m) -> VecT * n f a -> m # foldr :: (a -> b -> b) -> b -> VecT * n f a -> b # foldr' :: (a -> b -> b) -> b -> VecT * n f a -> b # foldl :: (b -> a -> b) -> b -> VecT * n f a -> b # foldl' :: (b -> a -> b) -> b -> VecT * n f a -> b # foldr1 :: (a -> a -> a) -> VecT * n f a -> a # foldl1 :: (a -> a -> a) -> VecT * n f a -> a # toList :: VecT * n f a -> [a] # null :: VecT * n f a -> Bool # length :: VecT * n f a -> Int # elem :: Eq a => a -> VecT * n f a -> Bool # maximum :: Ord a => VecT * n f a -> a # minimum :: Ord a => VecT * n f a -> a # sum :: Num a => VecT * n f a -> a # product :: Num a => VecT * n f a -> a #
Traversable f => Traversable (VecT * n f) Source #
Methods traverse :: Applicative f => (a -> f b) -> VecT * n f a -> f (VecT * n f b) # sequenceA :: Applicative f => VecT * n f (f a) -> f (VecT * n f a) # mapM :: Monad m => (a -> m b) -> VecT * n f a -> m (VecT * n f b) # sequence :: Monad m => VecT * n f (m a) -> m (VecT * n f a) #
Eq (f a) => Eq (VecT k n f a) Source #
Methods (==) :: VecT k n f a -> VecT k n f a -> Bool # (/=) :: VecT k n f a -> VecT k n f a -> Bool #
(Num (f a), Known N Nat n) => Num (VecT k n f a) Source #
Methods (+) :: VecT k n f a -> VecT k n f a -> VecT k n f a # (-) :: VecT k n f a -> VecT k n f a -> VecT k n f a # (*) :: VecT k n f a -> VecT k n f a -> VecT k n f a # negate :: VecT k n f a -> VecT k n f a # abs :: VecT k n f a -> VecT k n f a # signum :: VecT k n f a -> VecT k n f a # fromInteger :: Integer -> VecT k n f a #
Ord (f a) => Ord (VecT k n f a) Source #
Methods compare :: VecT k n f a -> VecT k n f a -> Ordering # (<) :: VecT k n f a -> VecT k n f a -> Bool # (<=) :: VecT k n f a -> VecT k n f a -> Bool # (>) :: VecT k n f a -> VecT k n f a -> Bool # (>=) :: VecT k n f a -> VecT k n f a -> Bool # max :: VecT k n f a -> VecT k n f a -> VecT k n f a # min :: VecT k n f a -> VecT k n f a -> VecT k n f a #
Show (f a) => Show (VecT k n f a) Source #
Methods showsPrec :: Int -> VecT k n f a -> ShowS # show :: VecT k n f a -> String # showList :: [VecT k n f a] -> ShowS #
type WitnessC ØC (Known N Nat n) (VecT k n f a) Source #
type WitnessC ØC (Known N Nat n) (VecT k n f a) = ØC

(*:) :: f a -> f a -> VecT (S (S Z)) f a infix 5 Source #

elimVecT :: p Z -> (forall x. f a -> p x -> p (S x)) -> VecT n f a -> p n Source #

elimV :: p Z -> (forall x. a -> p x -> p (S x)) -> Vec n a -> p n Source #

type Vec n = VecT n I Source #

pattern (:+) :: forall a n. a -> Vec n a -> Vec (S n) a infixr 4 Source #

(+:) :: a -> a -> Vec (S (S Z)) a infix 5 Source #

(.++) :: VecT x f a -> VecT y f a -> VecT (x + y) f a infixr 5 Source #

vrep :: forall n f a. Known Nat n => f a -> VecT n f a Source #

head' :: VecT (S n) f a -> f a Source #

tail' :: VecT (S n) f a -> VecT n f a Source #

onTail :: (VecT m f a -> VecT n f a) -> VecT (S m) f a -> VecT (S n) f a Source #

vDel :: Fin n -> VecT n f a -> VecT (Pred n) f a Source #

imap :: (Fin n -> f a -> g b) -> VecT n f a -> VecT n g b Source #

ifoldMap :: Monoid m => (Fin n -> f a -> m) -> VecT n f a -> m Source #

itraverse :: Applicative h => (Fin n -> f a -> h (g b)) -> VecT n f a -> h (VecT n g b) Source #

index :: Fin n -> VecT n f a -> f a Source #

index' :: Fin n -> Vec n a -> a Source #

vmap :: (f a -> g b) -> VecT n f a -> VecT n g b Source #

vap :: (f a -> g b -> h c) -> VecT n f a -> VecT n g b -> VecT n h c Source #

vfoldr :: (f a -> b -> b) -> b -> VecT n f a -> b Source #

vfoldMap' :: (b -> b -> b) -> b -> (f a -> b) -> VecT n f a -> b Source #

vfoldMap :: Monoid m => (f a -> m) -> VecT n f a -> m Source #

withVecT :: [f a] -> (forall n. VecT n f a -> r) -> r Source #

withV :: [a] -> (forall n. Vec n a -> r) -> r Source #

findV :: Eq a => a -> Vec n a -> Maybe (Fin n) Source #

findVecT :: Eq (f a) => f a -> VecT n f a -> Maybe (Fin n) Source #

newtype M ns a Source #

Constructors

M
Fields getMatrix :: Matrix ns a

Instances

Eq (Matrix ns a) => Eq (M ns a) Source #
Methods (==) :: M ns a -> M ns a -> Bool # (/=) :: M ns a -> M ns a -> Bool #
Num (Matrix ns a) => Num (M ns a) Source #
Methods (+) :: M ns a -> M ns a -> M ns a # (-) :: M ns a -> M ns a -> M ns a # (*) :: M ns a -> M ns a -> M ns a # negate :: M ns a -> M ns a # abs :: M ns a -> M ns a # signum :: M ns a -> M ns a # fromInteger :: Integer -> M ns a #
Ord (Matrix ns a) => Ord (M ns a) Source #
Methods compare :: M ns a -> M ns a -> Ordering # (<) :: M ns a -> M ns a -> Bool # (<=) :: M ns a -> M ns a -> Bool # (>) :: M ns a -> M ns a -> Bool # (>=) :: M ns a -> M ns a -> Bool # max :: M ns a -> M ns a -> M ns a # min :: M ns a -> M ns a -> M ns a #
Show (Matrix ns a) => Show (M ns a) Source #
Methods showsPrec :: Int -> M ns a -> ShowS # show :: M ns a -> String # showList :: [M ns a] -> ShowS #

type family Matrix (ns :: [N]) :: * -> * where ... Source #

Equations

Matrix Ø = I
Matrix (n :< ns) = VecT n (Matrix ns)

vgen_ :: Known Nat n => (Fin n -> f a) -> VecT n f a Source #

vgen :: Nat n -> (Fin n -> f a) -> VecT n f a Source #

mgen_ :: Known (Prod Nat) ns => (Prod Fin ns -> a) -> M ns a Source #

mgen :: Prod Nat ns -> (Prod Fin ns -> a) -> M ns a Source #

onMatrix :: (Matrix ms a -> Matrix ns b) -> M ms a -> M ns b Source #

diagonal :: VecT n (VecT n f) a -> VecT n f a Source #

vtranspose :: Known Nat n => VecT m (VecT n f) a -> VecT n (VecT m f) a Source #

transpose :: Known Nat n => M (m :< (n :< ns)) a -> M (n :< (m :< ns)) a Source #

m0 :: M Ø Int Source #

m1 :: M '[N2] Int Source #

m2 :: M '[N2, N4] Int Source #

m3 :: M '[N2, N3, N4] (Int, Int, Int) Source #

m4 :: M '[N2, N3, N4, N5] (Int, Int, Int, Int) Source #

ppVec :: (VecT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VecT n f a -> ShowS Source #

ppMatrix :: forall ns a. (Show a, Known Length ns) => M ns a -> IO () Source #

ppMatrix' :: Show a => Length ns -> Matrix ns a -> ShowS Source #

mzipWith :: Monoid a => (a -> a -> b) -> [a] -> [a] -> [b] Source #

zipLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS Source #

compose :: Foldable f => f (a -> a) -> a -> a Source #