Data.Type.Vector

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

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)

Methods

traverse1 :: Applicative h => (forall a. f a -> h (g a)) -> t f b -> h (t g b)

Foldable1 l l (VecT l n)

Methods

foldMap1 :: Monoid m => (forall a. f a -> m) -> t f b -> m

Functor1 l l (VecT l n)

Methods

map1 :: (forall a. f a -> g a) -> t f b -> t g b

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

Associated Types

type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (VecT k n f a) :: Constraint

Methods

(\\) :: ØC => (Known N Nat n -> r) -> VecT k n f a -> r

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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

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

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

type Vec n = VecT n I

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

findVecT :: Eq (f a) => f a -> VecT 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)

Methods

(==) :: M ns a -> M ns a -> Bool

(/=) :: M ns a -> M ns a -> Bool

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

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)

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)

Methods

showsPrec :: Int -> M ns a -> ShowS

show :: M ns a -> String

showList :: [M ns a] -> ShowS

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

Equations

Matrix Ø = I

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

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

vgen :: Nat n -> (Fin n -> f a) -> VecT 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 :: VecT n (VecT n f) a -> VecT n f a

vtranspose :: Known Nat n => VecT m (VecT n f) a -> VecT n (VecT 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 :: (VecT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VecT 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