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 : (1 _ : io a) -> (1 _ : (a -> io b)) -> io b
Implementation: LinearBind IO
bindL : LinearBind io => (1 _ : io a) -> (1 _ : (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 => (1 _ : L io a) -> io a
Run a linear program exactly once, with unrestricted return value in the
underlying context
Visibility: export(>>=) : LinearBind io => (1 _ : L io a) -> (1 _ : ContType io u_act u_k a b) -> L io b
- Visibility: export
Fixity Declaration: infixl operator, level 1 delay : (1 _ : L io b) -> ContType io u_act u_k () b
- Visibility: export
(>>) : LinearBind io => (1 _ : L io ()) -> (1 _ : L io b) -> L io b
- Visibility: export
Fixity Declaration: infixl operator, level 1 pure0 : (0 _ : a) -> L io a
- Visibility: export
pure1 : (1 _ : a) -> L io a
- Visibility: export
LinearIO : (Type -> Type) -> Type
- Visibility: public export