Data.V.Linear.Internal

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

Returns an empty V.

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

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

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.

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):

• n ~ PeanoToNat (NatToPeano n) is just there to help GHC, and will always be proved

• Elim (NatToPeano n) a b provides the actual implementation of elim; there is an instance of this class for any (n, a, b)

• IsFunN a b f, f ~ FunN (NatToPeano n) a b, n ~ Arity b f indicate the shape of f to the typechecker (see documentation of IsFunN).

Prepends the given element to the V.

Creates a V of the specified size by consuming a Replicator.

Produces a V n a from a Dupable value a.

Returns the type-level Nat of the context as a term-level integer.

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.

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):

• n ~ PeanoToNat (NatToPeano n) is just there to help GHC, and will always be proved

• Make (NatToPeano n) (NatToPeano n) a provides the actual implementation of make; there is an instance of this class for any (n, a)

• IsFunN a (V n a) f, f ~ FunN (NatToPeano n) a (V n a), n ~ ArityV f indicate the shape to the typechecker of f (see documentation of IsFunN).

The ArityV type family exists to help the type checker compute the arity n ~ Arity b f when b ~ V n a.