Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.V.Linear

Contents

Type-level helpers for staging

Description

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

Synopsis

data V (n :: Nat) (a :: Type)
empty :: forall a. V 0 a
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
uncons# :: 1 <= n => V n a %1 -> (# a, V (n - 1) a #)
uncons :: 1 <= n => V n a %1 -> (a, V (n - 1) a)
class Elim n a 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
cons :: forall n a. a %1 -> V (n - 1) a %1 -> V n a
fromReplicator :: forall n a. KnownNat n => Replicator a %1 -> V n a
dupV :: forall n a. (KnownNat n, Dupable a) => a %1 -> V n a
theLength :: forall n. KnownNat n => Int
class Make m 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
type family ArityV f where ...

Documentation

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

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

Instances

Instances details

Foldable (V n) Source #
Instance details Defined in Data.V.Linear.Internal Methods fold :: Monoid m => V n m -> m # foldMap :: Monoid m => (a -> m) -> V n a -> m # foldMap' :: Monoid m => (a -> m) -> V n a -> m # foldr :: (a -> b -> b) -> b -> V n a -> b # foldr' :: (a -> b -> b) -> b -> V n a -> b # foldl :: (b -> a -> b) -> b -> V n a -> b # foldl' :: (b -> a -> b) -> b -> V n a -> b # foldr1 :: (a -> a -> a) -> V n a -> a # foldl1 :: (a -> a -> a) -> V n a -> a # toList :: V n a -> [a] # null :: V n a -> Bool # length :: V n a -> Int # elem :: Eq a => a -> V n a -> Bool # maximum :: Ord a => V n a -> a # minimum :: Ord a => V n a -> a # sum :: Num a => V n a -> a # product :: Num a => V n a -> a #
Traversable (V n) Source #
Instance details Defined in Data.V.Linear.Internal Methods traverse :: Applicative f => (a -> f b) -> V n a -> f (V n b) # sequenceA :: Applicative f => V n (f a) -> f (V n a) # mapM :: Monad m => (a -> m b) -> V n a -> m (V n b) # sequence :: Monad m => V n (m a) -> m (V n a) #
KnownNat n => Applicative (V n) Source #
Instance details Defined in Data.V.Linear.Internal.Instances Methods pure :: a -> V n a # (<>) :: V n (a -> b) -> V n a -> V n b # liftA2 :: (a -> b -> c) -> V n a -> V n b -> V n c # (>) :: V n a -> V n b -> V n b # (<*) :: V n a -> V n b -> V n a #
Functor (V n) Source #
Instance details 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) Source #
Instance details Defined in Data.V.Linear.Internal.Instances Methods pure :: a -> V n a Source # (<*>) :: V n (a %1 -> b) %1 -> V n a %1 -> V n b Source # liftA2 :: (a %1 -> b %1 -> c) -> V n a %1 -> V n b %1 -> V n c Source #
Functor (V n) Source #
Instance details Defined in Data.V.Linear.Internal.Instances Methods fmap :: (a %1 -> b) -> V n a %1 -> V n b Source #
KnownNat n => Traversable (V n) Source #
Instance details Defined in Data.V.Linear.Internal.Instances Methods traverse :: Applicative f => (a %1 -> f b) -> V n a %1 -> f (V n b) Source # sequence :: Applicative f => V n (f a) %1 -> f (V n a) Source #
Show a => Show (V n a) Source #
Instance details Defined in Data.V.Linear.Internal Methods showsPrec :: Int -> V n a -> ShowS # show :: V n a -> String # showList :: [V n a] -> ShowS #
Eq a => Eq (V n a) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Data.Unrestricted.Linear.Internal.Instances Methods consume :: V n a %1 -> () Source #
Consumable (V 0 a) Source #
Instance details Defined in Data.Unrestricted.Linear.Internal.Instances Methods consume :: V 0 a %1 -> () Source #
(KnownNat n, Dupable a) => Dupable (V n a) Source #
Instance details Defined in Data.Unrestricted.Linear.Internal.Instances Methods dupR :: V n a %1 -> Replicator (V n a) Source # dup2 :: V n a %1 -> (V n a, V n a) Source #

empty :: forall a. V 0 a Source #

Returns an empty V.

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

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

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

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

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

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

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

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

class Elim n a b Source #

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

Instances details

Elim 'Z a b Source #
Instance details 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 Source #
Instance details 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 Source #

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 Source #

Prepends the given element to the V.

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

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

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

Produces a V n a from a Dupable value a.

theLength :: forall n. KnownNat n => Int Source #

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

class Make m n a Source #

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

Instances details

Make 'Z n a Source #
Instance details 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 Source #
Instance details 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 Source #

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

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 _ _)")