- (>>) : LinearBind io => (1 _ : L io ()) -> (1 _ : L io b) -> L io b
-
Fixity Declaration: infixl operator, level 1 - (>>=) : LinearBind io => (1 _ : L io a) -> (1 _ : ContType io u_act u_k a b) -> L io b
-
Fixity Declaration: infixl operator, level 1 - ContType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
-
- 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
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
- L0 : (Type -> Type) -> Type -> Type
-
- L1 : (Type -> Type) -> Type -> Type
-
- 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
- LinearIO : (Type -> Type) -> Type
-
- data Usage : Type
Required usage on the result value of a computation
Totality: total
Constructors:
- None : Usage
- Linear : Usage
- Unrestricted : Usage
- bindL : LinearBind io => (1 _ : io a) -> (1 _ : (a -> io b)) -> io b
-
- delay : (1 _ : L io b) -> ContType io u_act u_k () b
-
- fromInteger : (x : Integer) -> Either (x = 0) (x = 1) => Usage
-
- pure0 : (0 _ : a) -> L io a
-
- pure1 : (1 _ : a) -> L io a
-
- 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