Data.V.Linear.Internal.V

Documentation

newtype V (n :: Nat) (a :: Type)

Constructors

V (Vector a)

Instances

Functor (V n)

Defined in Data.V.Linear.Internal.V

Methods

fmap :: (a -> b) -> V n a -> V n b

(<$) :: a -> V n b -> V n a

Functor (V n)

Defined in Data.V.Linear.Internal.Instances

Methods

fmap :: (a %1 -> b) -> V n a %1 -> V n b

KnownNat n => Applicative (V n)

Defined in Data.V.Linear.Internal.Instances

Methods

pure :: a -> V n a

(<*>) :: V n (a %1 -> b) %1 -> V n a %1 -> V n b

liftA2 :: (a %1 -> b %1 -> c) -> V n a %1 -> V n b %1 -> V n c

KnownNat n => Traversable (V n)

Defined in Data.V.Linear.Internal.Instances

Methods

traverse :: Applicative f => (a %1 -> f b) -> V n a %1 -> f (V n b)

sequence :: Applicative f => V n (f a) %1 -> f (V n a)

Eq a => Eq (V n a)

Defined in Data.V.Linear.Internal.V

Methods

(==) :: V n a -> V n a -> Bool

(/=) :: V n a -> V n a -> Bool

Ord a => Ord (V n a)

Defined in Data.V.Linear.Internal.V

Methods

compare :: V n a -> V n a -> Ordering

(<) :: V n a -> V n a -> Bool

(<=) :: V n a -> V n a -> Bool

(>) :: V n a -> V n a -> Bool

(>=) :: V n a -> V n a -> Bool

max :: V n a -> V n a -> V n a

min :: V n a -> V n a -> V n a

type family FunN (n :: Nat) (a :: Type) (b :: Type) :: Type where ...

Equations

FunN 0 a b = b

FunN n a b = a %1 -> FunN (n - 1) a b

theLength :: forall n. KnownNat n => Int

elim :: forall n a b. KnownNat n => V n a %1 -> FunN n a b %1 -> b

This is like pattern-matching on a n-tuple. It will eventually be polymorphic the same way as a case expression.

make :: forall n a. KnownNat n => FunN n a (V n a)

iterate :: forall n a. (KnownNat n, 1 <= n) => (a %1 -> (a, a)) -> a %1 -> V n a

Type-level utilities

caseNat :: forall n. KnownNat n => Either (n :~: 0) ((1 <=? n) :~: 'True)