HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

Modulelinear-base-0.4.0Haskell2010

Data.V.Linear

This module defines vectors of known length which can hold linear values.

Having a known length matters with linear types, because many common vector operations (like zip) are not total with linear types.

Make these vectors by giving any finite number of arguments to make and use them with elim:

Example7 expressions
:set -XLinearTypes:set -XTypeApplications:set -XDataKinds:set -XTypeFamiliesimport Prelude.Linearimport qualified Data.V.Linear as V:{ doSomething :: Int %1-> Int %1-> Bool doSomething x y = x + y > 0:}
Example1 expression
:{ isTrue :: Bool isTrue = V.elim doSomething (build 4 9)   where     build :: Int %1-> Int %1-> V.V 2 Int     build = V.make:}

A much more expensive library of vectors of known size (including matrices and tensors of all dimensions) is the linear library on Hackage (that's linear in the sense of linear algebra, rather than linear types).

  • 1 type
  • 2 classes
  • 13 values
newtypenewtype V (n :: Nat) a
#

V n a represents an immutable sequence of n elements of type a (like a n-tuple), with a linear Applicative instance.

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

Returns an empty V.

valuemap :: (a %1 -> b) -> V n a %1 -> V n b
#
value(<*>) :: V n (a %1 -> b) %1 -> V n a %1 -> V n b
#
valueuncons# :: 1 <= n => V n a %1 -> (# a, V (n - 1) a #)
#

Splits the head and tail of the V, returning an unboxed tuple.

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

Splits the head and tail of the V, returning a boxed tuple.

classclass Elim (n :: Peano) a b where
#

Elim n a b is used to implement elim without recursion so that we can guarantee that elim will be inlined and unrolled.

Elim is solely used in the signature of elim.

Instances2Elim
valueelim
  1. :: (n ~ PeanoToNat (NatToPeano n), Elim (NatToPeano n) a b, IsFunN a b f, f ~ FunN (NatToPeano n) a b, n ~ Arity b f)
  2. => f
  3. -> V n a
  4. -> b
#

Takes a function of type a %1 -> a %1 -> ... %1 -> a %1 -> b, and returns a b . The V n a is used to supply all the items of type a required by the function.

For instance:

elim @1 :: (a %1 -> b) %1 -> V 1 a %1 -> b
elim @2 :: (a %1 -> a %1 -> b) %1 -> V 2 a %1 -> b
elim @3 :: (a %1 -> a %1 -> a %1 -> b) %1 -> V 3 a %1 -> b

It is not always necessary to give the arity argument. It can be inferred from the function argument.

About the constraints of this function (they won't get in your way):

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

Prepends the given element to the V.

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

Make m n a is used to avoid recursion in the implementation of make so that make can be inlined.

Make is solely used in the signature of that function.

Instances2Make
  • Make 'Z n aDefined in linear-base-0.4.0 · Data.V.Linear.Internal
  • (((1 + PeanoToNat m) - 1) ~ PeanoToNat m, Make m n a) => Make ('S m) n aDefined in linear-base-0.4.0 · Data.V.Linear.Internal
valuemake :: (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
#

Builds a n-ary constructor for V n a (i.e. a function taking n linear arguments of type a and returning a V n a).

myV :: V 3 Int
myV = make 1 2 3

About the constraints of this function (they won't get in your way):

Type-level helpers for staging

1 declaration