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 (build 4 9) doSomething
   where
     -- GHC can't figure out this type equality, so this is needed.
     build :: Int %1-> Int %1-> V.V 2 Int
     build = V.make @2 @Int
:}

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)

Instances

Functor (V n)

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)

Defined in Data.V.Linear.Internal.Instances

Methods

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

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

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.V

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

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

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)

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

Type-level utilities

caseNat :: forall n. KnownNat n => Either (n :~: 0) ((1 <=? n) :~: 'True)