Data.Linear.Interface

Reexports

Definitions

interface Consumable : Type -> Type

  An interface for consumable types

Parameters: a
Methods:

consume : a -@ ()

Implementations:

Consumable Void

Consumable ()

Consumable Bool

Consumable ((!*) a)

Consumable Int

consume : Consumable a => a -@ ()

Totality: total
Visibility: public export

seq : Consumable a => a -@ (b -@ b)

  We can sequentially compose a computation returning a value that is
  consumable with another computation. This is done by first consuming
  the result of the first computation and then returning the second one.

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

interface Duplicable : Type -> Type

Parameters: a
Methods:

duplicate : (1 v : a) -> 2 `Copies` v

Implementations:

Duplicable Void

Duplicable ()

Duplicable Bool

Duplicable ((!*) a)

duplicate : Duplicable a => (1 v : a) -> 2 `Copies` v

Totality: total
Visibility: public export

interface Comonoid : Type -> Type

  Comonoid is the dual of Monoid, it can consume a value linearly and duplicate a value linearly
  `comult` returns a pair instead of 2 copies, because we do not guarantee that the two values
  are identical, unlike with `duplicate`. For example if we build a comonoid out of a group, with
  comult returning both the element given and its inverse:
  comult x = x # inverse x
  It is not necessarily the case that x equals its inverse. For example the finite group of size
  3, has 1 and 2 as inverses of each other wrt to addition, but are not the same.

Parameters: a
Methods:

counit : a -@ ()

comult : a -@ LPair a a

Implementation: 

Comonoid ((!*) a)

counit : Comonoid a => a -@ ()

Totality: total
Visibility: public export

comult : Comonoid a => a -@ LPair a a

Totality: total
Visibility: public export