Idris2Doc : Data.Linear.Interface

Data.Linear.Interface

Reexports

importpublic Data.Linear.Copies

Definitions

interfaceConsumable : Type->Type
  An interface for consumable types

Parameters: a
Methods:
consume : a-@ ()

Implementations:
ConsumableVoid
Consumable ()
ConsumableBool
Consumable ((!*)a)
ConsumableInt
consume : Consumablea=>a-@ ()
Totality: total
Visibility: public export
seq : Consumablea=>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
interfaceDuplicable : Type->Type
Parameters: a
Methods:
duplicate : (1v : a) ->2 `Copies` v

Implementations:
DuplicableVoid
Duplicable ()
DuplicableBool
Duplicable ((!*)a)
duplicate : Duplicablea=> (1v : a) ->2 `Copies` v
Totality: total
Visibility: public export
interfaceComonoid : 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 groupe 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-@LPairaa

Implementation: 
Comonoid ((!*)a)
counit : Comonoida=>a-@ ()
Totality: total
Visibility: public export
comult : Comonoida=>a-@LPairaa
Totality: total
Visibility: public export