Data.Linear.Copies

Definitions

data Copies : Nat -> (0 _ : a) -> Type

  Carries multiple linear copies of the same value. Usage: m `Copies` x
  reads as "m copies of value x". This data structure is necessary to implement
  algorithms that rely on linearity but also interact with Nat indicies, like
  Vect and Fin.
  This datastructure can be found in the paper "How to Take the Inverse of a Type" by
  Daniel Marshall and Dominic Orchard where it's described as an exponent operator

Totality: total
Visibility: public export
Constructors:

Nil : 0 `Copies` x

(::) : (1 x : a) -> (1 _ : n `Copies` x) -> S n `Copies` x

Fixity Declaration: infix operator, level 1

splitAt : (1 m : Nat) -> ((m + n) `Copies` x) -@ LPair (m `Copies` x) (n `Copies` x)

  Split copies into two

Totality: total
Visibility: export

(++) : (m `Copies` x) -@ ((n `Copies` x) -@ ((m + n) `Copies` x))

  Combine multiple copies into one

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

unzip : (m `Copies` (x # y)) -@ LPair (m `Copies` x) (m `Copies` y)

  Copies of pairs are like pairs of copies

Totality: total
Visibility: export

pure : (x : a) -> n `Copies` x

Totality: total
Visibility: export

(<*>) : (m `Copies` f) -@ ((m `Copies` x) -@ (m `Copies` f x))

  Applies m copies of a linear function to m arguments, resulting in m copies
  of the result.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 3

(<$>) : (f : a -@ b) -> (m `Copies` x) -@ (m `Copies` f x)

  Apply f to `m` copies of `x`, resulting in `m` copies of `f x`.
  
  Note that this is not quite `pure f <*> xs` because we don't actually
  need to know `m` to be able to define `(<$>)` as we can proceed by
  induction on xs.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 4

zip : (m `Copies` x) -@ ((m `Copies` y) -@ (m `Copies` (x # y)))

  Combine copies of two values into a pair of copies

Totality: total
Visibility: export

extract : (1 `Copies` x) -@ a

  If we have a single copy, we can extract its value

Totality: total
Visibility: export

pair : (2 `Copies` x) -@ LPair a a

  Extract 2 copies into a linear pair

Totality: total
Visibility: export