Data.Linear.ELift1

Reexports

Definitions

data ERes : Type -> List Type -> Type -> Type

  Result of a linear computation running in state thread
  `s` producing either a value of type `a` or an error of
  one of the types listed in `es`.

Totality: total
Visibility: public export
Constructors:

E : HSum es -> (1 _ : T1 s) -> ERes s es a

R : a -> (1 _ : T1 s) -> ERes s es a

0 E1 : Type -> List Type -> Type -> Type

  An alias similar to `F1 s a` but for linear computations that could
  fail with one of the errors listed.

Totality: total
Visibility: public export

0 E1' : Type -> List Type -> Type

  Alias for `E1 s es ()`

Totality: total
Visibility: public export

e1ToF1 : Monoid a => E1 s es a -> F1 s a

  Replaces all errors with `neutral`, running an `E1` as an `F1`.

Totality: total
Visibility: export

f1ToE1 : F1 s a -> E1 s es a

  Lifts a linear computation into an `E1 s a`.

Totality: total
Visibility: export

mapERes : (a -> b) -> (1 _ : ERes e es a) -> ERes e es b

Totality: total
Visibility: export

pattempt : (1 _ : ERes e es a) -> ERes e fs (Result es a)

Totality: total
Visibility: export

toResult : (1 _ : ERes s es a) -> R1 s (Result es a)

Totality: total
Visibility: export

toEither : (1 _ : ERes s [e] a) -> R1 s (Either e a)

Totality: total
Visibility: export

throw1 : Has e es => e -> E1 s es a

Totality: total
Visibility: export

fail1 : e -> E1 s [e] a

Totality: total
Visibility: export

interface ELift1 : Type -> (List Type -> Type -> Type) -> Type

  An interface for lifting stateful, linear computation into
  a monad with the potential of failure.

Parameters: s, f
Constraints: MErr f
Methods:

elift1 : E1 s es a -> f es a

Implementation: 

ELift1 s (Elin s)

elift1 : ELift1 s f => E1 s es a -> f es a

Totality: total
Visibility: public export

0 EIO1 : (List Type -> Type -> Type) -> Type

  Convenience alias for `ELift1 World`

Totality: total
Visibility: public export

liftInject1 : Has e es => ELift1 s f => E1 s [e] a -> f es a

Totality: total
Visibility: export

resultToERes : Result es a -> E1 s es a

Totality: total
Visibility: export

eitherToERes : Has e es => Either e a -> E1 s es a

Totality: total
Visibility: export

resultToE1 : F1 s (Result es a) -> E1 s es a

Totality: total
Visibility: export

eitherToE1 : Has e es => F1 s (Either e a) -> E1 s es a

Totality: total
Visibility: export

eliftResult : ELift1 s f => F1 s (Result es a) -> f es a

Totality: total
Visibility: export

eliftEither : Has e es => ELift1 s f => F1 s (Either e a) -> f es a

Totality: total
Visibility: export