Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.V.Linear.Internal.V

Contents

Synopsis

newtype V (n :: Nat) (a :: Type) = V (Vector a)
type family FunN (n :: Nat) (a :: Type) (b :: Type) :: Type where ...
theLength :: forall n. KnownNat n => Int
elim :: forall n a b. KnownNat n => V n a %1 -> FunN n a b %1 -> b
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
caseNat :: forall n. KnownNat n => Either (n :~: 0) ((1 <=? n) :~: 'True)

Documentation

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

Constructors

Instances details

Functor (V n) Source #
Instance details 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) Source #
Instance details Defined in Data.V.Linear.Internal.Instances Methods fmap :: (a %1 -> b) -> V n a %1 -> V n b Source #
KnownNat n => Applicative (V n) Source #
Instance details Defined in Data.V.Linear.Internal.Instances Methods pure :: a -> V n a Source # (<*>) :: V n (a %1 -> b) %1 -> V n a %1 -> V n b Source # liftA2 :: (a %1 -> b %1 -> c) -> V n a %1 -> V n b %1 -> V n c Source #
KnownNat n => Traversable (V n) Source #
Instance details Defined in Data.V.Linear.Internal.Instances Methods traverse :: Applicative f => (a %1 -> f b) -> V n a %1 -> f (V n b) Source # sequence :: Applicative f => V n (f a) %1 -> f (V n a) Source #
Eq a => Eq (V n a) Source #
Instance details 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) Source #
Instance details 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 ... Source #

Equations

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

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

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) Source #

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

Type-level utilities