Data.Type.Vector

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

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

The operations on V and VT correspond to the type level arithmetic operations on the kind N.

Documentation

data VT n f :: k -> * where

Constructors

ØV :: VT Z f a

(:*) :: !(f a) -> !(VT n f a) -> VT (S n) f a infixr 4

Instances

Witness ØC (Known N Nat n) (VT k n f a)

(Monad f, Known N Nat n) => Monad (VT * n f)

Functor f => Functor (VT * n f)

(Applicative f, Known N Nat n) => Applicative (VT * n f)

Foldable f => Foldable (VT * n f)

Traversable f => Traversable (VT * n f)

Eq (f a) => Eq (VT k n f a)

(Num (f a), Known N Nat n) => Num (VT k n f a)

Ord (f a) => Ord (VT k n f a)

Show (f a) => Show (VT k n f a)

type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC

elimVT :: p Z -> (forall x. f a -> p x -> p (S x)) -> VT n f a -> p n

elimV :: p Z -> (forall x. a -> p x -> p (S x)) -> V n a -> p n

type V n = VT n I

pattern (:+) :: a -> V n a -> V (S n) a infixr 4

(.++) :: VT x f a -> VT y f a -> VT (x + y) f a infixr 5

vrep :: forall n f a. Known Nat n => f a -> VT n f a

head' :: VT (S n) f a -> f a

tail' :: VT (S n) f a -> VT n f a

onTail :: (VT m f a -> VT n f a) -> VT (S m) f a -> VT (S n) f a

vDel :: Fin n -> VT n f a -> VT (Pred n) f a

imap :: (Fin n -> f a -> g b) -> VT n f a -> VT n g b

ifoldMap :: Monoid m => (Fin n -> f a -> m) -> VT n f a -> m

itraverse :: Applicative h => (Fin n -> f a -> h (g b)) -> VT n f a -> h (VT n g b)

index :: Fin n -> VT n f a -> f a

vmap :: (f a -> g b) -> VT n f a -> VT n g b

vap :: (f a -> g b -> h c) -> VT n f a -> VT n g b -> VT n h c

vfoldr :: (f a -> b -> b) -> b -> VT n f a -> b

vfoldMap' :: (b -> b -> b) -> b -> (f a -> b) -> VT n f a -> b

vfoldMap :: Monoid m => (f a -> m) -> VT n f a -> m

withVT :: [f a] -> (forall n. VT n f a -> r) -> r

withV :: [a] -> (forall n. V n a -> r) -> r

findV :: Eq a => a -> V n a -> Maybe (Fin n)

findVT :: Eq (f a) => f a -> VT n f a -> Maybe (Fin n)

newtype M ns a

Constructors

M

Fields

getMatrix :: Matrix ns a

Instances

Eq (Matrix ns a) => Eq (M ns a)

Num (Matrix ns a) => Num (M ns a)

Ord (Matrix ns a) => Ord (M ns a)

Show (Matrix ns a) => Show (M ns a)

type family Matrix ns :: * -> *

Equations

Matrix Ø = I

Matrix (n :< ns) = VT n (Matrix ns)

vgen_ :: Known Nat n => (Fin n -> f a) -> VT n f a

vgen :: Nat n -> (Fin n -> f a) -> VT n f a

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

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

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

diagonal :: VT n (VT n f) a -> VT n f a

vtranspose :: Known Nat n => VT m (VT n f) a -> VT n (VT m f) a

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

m0 :: M Ø Int

m1 :: M `[N2]` Int

m2 :: M `[N2, N4]` Int

m3 :: M `[N2, N3, N4]` (Int, Int, Int)

m4 :: M `[N2, N3, N4, N5]` (Int, Int, Int, Int)

ppVec :: (VT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VT n f a -> ShowS

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

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

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

zipLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS

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