Control.Linear.LIO

Reexports

Definitions

interface LinearBind : (Type -> Type) -> Type

  Like `Monad`, but the action and continuation must be run exactly once
  to ensure that the computation is linear.

Parameters: io
Methods:

bindL : io a -@ ((a -> io b) -@ io b)

Implementation: 

LinearBind IO

bindL : LinearBind io => io a -@ ((a -> io b) -@ io b)

Visibility: public export

data Usage : Type

  Required usage on the result value of a computation

Totality: total
Visibility: public export
Constructors:

None : Usage

Linear : Usage

Unrestricted : Usage

fromInteger : (x : Integer) -> Either (x = 0) (x = 1) => Usage

Visibility: public export

0 ContType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type

Visibility: public export

data L : (Type -> Type) -> {default Unrestricted _ : Usage} -> Type -> Type

  A wrapper which allows operations to state the multiplicity of the value
  they return. For example, `L IO {use=1} File` is an IO operation which
  returns a file that must be used exactly once.

Totality: total
Visibility: export
Constructors:

Pure0 : (0 _ : a) -> L io a

Pure1 : (1 _ : a) -> L io a

PureW : a -> L io a

Action : (1 _ : io a) -> L io a

Bind : (1 _ : L io a) -> (1 _ : ContType io u_act u_k a b) -> L io b

Hints:

Applicative io => Applicative (L io)

Functor io => Functor (L io)

(LinearBind io, HasLinearIO io) => HasLinearIO (L io)

(Applicative m, LinearBind m) => Monad (L m)

L0 : (Type -> Type) -> Type -> Type

Visibility: public export

L1 : (Type -> Type) -> Type -> Type

Visibility: public export

run : Applicative io => LinearBind io => L io a -@ io a

  Run a linear program exactly once, with unrestricted return value in the
  underlying context

Visibility: export

(>>=) : LinearBind io => L io a -@ (ContType io u_act u_k a b -@ L io b)

Visibility: export
Fixity Declaration: infixl operator, level 1

delay : L io b -@ ContType io u_act u_k () b

Visibility: export

(>>) : LinearBind io => L io () -@ (L io b -@ L io b)

Visibility: export
Fixity Declaration: infixl operator, level 1

pure0 : (0 _ : a) -> L io a

Visibility: export

pure1 : a -@ L io a

Visibility: export

bang : L IO t -@ L1 IO ((!*) t)

  Shuffling around linearity annotations: a computation of an
  unrestricted value can be seen as a computation of a linear
  value that happens to be unrestricted.

Visibility: export

LinearIO : (Type -> Type) -> Type

Visibility: public export

die1 : LinearIO io => String -> L1 io a

  Linear version of `die`

Visibility: export