Modulelinear-base-0.8.1

Data.V.Linear.Internal

1 type
2 classes
13 values

Packagelinear-base-0.8.1
Exports17
LicenceMIT

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

valuecons :: a %1 -> V (n - 1) a %1 -> V n a

valueconsume :: V 0 a %1 -> ()

valuedupV :: (KnownNat n, Dupable a) => a %1 -> V n a

valueelim

:: (n ~ PeanoToNat (NatToPeano n), Elim (NatToPeano n) a b, IsFunN a b f, f ~ FunN (NatToPeano n) a b, n ~ Arity b f)
=> f
-> V n a
-> b

valueempty :: V 0 a

valuefromReplicator :: KnownNat n => Replicator a %1 -> V n a

value

make :: (n ~ PeanoToNat (NatToPeano n), Make (NatToPeano n) (NatToPeano n) a, IsFunN a (V n a) f, f ~ FunN (NatToPeano n) a (V n a), n ~ ArityV f) => f

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

valuepure :: KnownNat n => a -> V n a

valuetheLength :: KnownNat n => Int

valueuncons :: 1 <= n => V n a %1 -> (a, V (n - 1) a)

valueuncons# :: 1 <= n => V n a %1 -> (# a, V (n - 1) a #)

familytype family ArityV f :: Natural where

Equations

ArityV (V _1 _2) = 0
ArityV (a %1 -> f) = 1 + ArityV f
ArityV f = TypeError (('Text "Arity: " ':<>: 'ShowType f) ':<>: 'Text " isn't a linear function with head (V _ _)")

classclass Elim (n :: Peano) a b where

Instances2Elim

Elim 'Z a bDefined in linear-base-0.8.1 · Data.V.Linear.Internal
(1 <= (1 + PeanoToNat n), ((1 + PeanoToNat n) - 1) ~ PeanoToNat n, Elim n a b) => Elim ('S n) a bDefined in linear-base-0.8.1 · Data.V.Linear.Internal

classclass Make (m :: Peano) (n :: Peano) a where

Instances2Make

Make 'Z n aDefined in linear-base-0.8.1 · Data.V.Linear.Internal
(((1 + PeanoToNat m) - 1) ~ PeanoToNat m, Make m n a) => Make ('S m) n aDefined in linear-base-0.8.1 · Data.V.Linear.Internal

newtypenewtype V (n :: Nat) a

Constructors

V (Vector a)

Instances13Foldable, Functor, Applicative, Traversable, Eq, Ord, …

Functor (V n)Defined in linear-base-0.8.1 · Data.V.Linear.Internal
KnownNat n => Applicative (V n)Defined in linear-base-0.8.1 · Data.V.Linear.Internal.Instances · orphan
Foldable (V n)Defined in linear-base-0.8.1 · Data.V.Linear.Internal
Traversable (V n)Defined in linear-base-0.8.1 · Data.V.Linear.Internal
Functor (V n)Defined in linear-base-0.8.1 · Data.V.Linear.Internal.Instances · orphan
KnownNat n => Applicative (V n)Defined in linear-base-0.8.1 · Data.V.Linear.Internal.Instances · orphan
KnownNat n => Traversable (V n)Defined in linear-base-0.8.1 · Data.V.Linear.Internal.Instances · orphan
Eq a => Eq (V n a)Defined in linear-base-0.8.1 · Data.V.Linear.Internal
Ord a => Ord (V n a)Defined in linear-base-0.8.1 · Data.V.Linear.Internal
Show a => Show (V n a)Defined in linear-base-0.8.1 · Data.V.Linear.Internal
Consumable (V 0 a)Defined in linear-base-0.8.1 · Data.Unrestricted.Linear.Internal.Instances · orphan
(KnownNat n, Consumable a) => Consumable (V n a)Defined in linear-base-0.8.1 · Data.Unrestricted.Linear.Internal.Instances · orphan
(KnownNat n, Dupable a) => Dupable (V n a)Defined in linear-base-0.8.1 · Data.Unrestricted.Linear.Internal.Instances · orphan