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:

>>> :set -XLinearTypes
>>> :set -XTypeApplications
>>> :set -XTypeInType
>>> :set -XTypeFamilies
>>> import Prelude.Linear
>>> import qualified Data.V.Linear as V
>>> :{
 doSomething :: Int %1-> Int %1-> Bool
 doSomething x y = x + y > 0
:}

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

Documentation

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

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

Instances

Functor (V n)

Defined in Data.V.Linear.Internal

Methods

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

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

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

Functor (V n)

Defined in Data.V.Linear.Internal.Instances

Methods

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

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

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

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

(KnownNat n, Consumable a) => Consumable (V n a)

Defined in Data.Unrestricted.Linear.Internal.Instances

Methods

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

Consumable (V 0 a)

Defined in Data.Unrestricted.Linear.Internal.Instances

Methods

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

(KnownNat n, Dupable a) => Dupable (V n a)

Defined in Data.Unrestricted.Linear.Internal.Instances

Methods

dupR :: V n a %1 -> Replicator (V n a)

dup2 :: V n a %1 -> (V n a, V n a)

empty :: forall a. V 0 a

Returns an empty V.

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

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

pure :: forall n a. KnownNat n => a -> V n a

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

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

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

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

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

class Elim n a b

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.

Minimal complete definition

elim'

Instances

Elim 'Z a b

Defined in Data.V.Linear.Internal

Methods

elim' :: FunN 'Z a b %1 -> V (PeanoToNat 'Z) a %1 -> b

(1 <= (1 + PeanoToNat n), ((1 + PeanoToNat n) - 1) ~ PeanoToNat n, Elim n a b) => Elim ('S n) a b

Defined in Data.V.Linear.Internal

Methods

elim' :: FunN ('S n) a b %1 -> V (PeanoToNat ('S n)) a %1 -> b

elim :: forall (n :: Nat) a b f. (n ~ PeanoToNat (NatToPeano n), Elim (NatToPeano n) a b, IsFunN a b f, f ~ FunN (NatToPeano n) a b, n ~ Arity b f) => f %1 -> V n a %1 -> 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):

• 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).

cons :: forall n a. a %1 -> V (n - 1) a %1 -> V n a

Prepends the given element to the V.

fromReplicator :: forall n a. KnownNat n => Replicator a %1 -> V n a

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

dupV :: forall n a. (KnownNat n, Dupable a) => a %1 -> V n a

Produces a V n a from a Dupable value a.

theLength :: forall n. KnownNat n => Int

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

class Make m n a

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.

Minimal complete definition

make'

Instances

Make 'Z n a

Defined in Data.V.Linear.Internal

Methods

make' :: (V (PeanoToNat 'Z) a %1 -> V (PeanoToNat n) a) %1 -> FunN 'Z a (V (PeanoToNat n) a)

(((1 + PeanoToNat m) - 1) ~ PeanoToNat m, Make m n a) => Make ('S m) n a

Defined in Data.V.Linear.Internal

Methods

make' :: (V (PeanoToNat ('S m)) a %1 -> V (PeanoToNat n) a) %1 -> FunN ('S m) a (V (PeanoToNat n) a)

make :: forall (n :: Nat) a f. (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):

• 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).

Type-level helpers for staging

type family ArityV f where ...

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

Equations

ArityV (V _ _) = 0

ArityV (a %1 -> f) = 1 + ArityV f

ArityV f = TypeError (('Text "Arity: " :<>: 'ShowType f) :<>: 'Text " isn't a linear function with head (V _ _)")