Control.App

(>>=) : SafeBind l l' => App e a -> (a -> App e b) -> App e b

Fixity Declaration: infixl operator, level 1

data App : {default MayThrow _ : Path} -> List Error -> Type -> Type

  A type supports throwing and catching exceptions. See `interface Exception err e` for details.
  @ l An implicit Path states whether the program's execution path is linear or might throw
  exceptions. The default value is `MayThrow` which represents that the program might throw.
  @ es A list of exception types that can be thrown. Constrained interfaces can be defined by
  parameterising with a list of errors `es`.

Totality: total
Constructor:

MkApp : (1 _ : ((1 _ : %World) -> AppRes (execTy l e t))) -> App e t

data App1 : {default One _ : Usage} -> List Error -> Type -> Type

Totality: total
Constructor:

MkApp1 : (1 _ : ((1 _ : %World) -> App1Res u t)) -> App1 e t

data AppHasIO : Type

  When type is present in app "errors" list, app is allowed to perform I/O.

Totality: total

Cont1Type : Usage -> Type -> Usage -> List Error -> Type -> Type

Error : Type

  `Error` is a type synonym for `Type`, specify for exception handling.

Exception : Error -> List Error -> Type

  An alias for `HasErr`.

data FileEx : Type

Totality: total
Constructors:

GenericFileEx : Int -> FileEx
FileReadError : FileEx
FileWriteError : FileEx
FileNotFound : FileEx
PermissionDenied : FileEx
FileExists : FileEx

Has : List (a -> Type) -> a -> Type

data HasErr : Error -> List Error -> Type

Totality: total
Constructors:

Here : HasErr e (e :: es)
There : HasErr e es -> HasErr e (e' :: es)

data IOError : Type

Totality: total
Constructors:

GenericErr : String -> IOError
FileErr : FileEx -> IOError

Init : List Error

data Path : Type

  States whether the program's execution path is linear or might throw exceptions so that we can know
  whether it is safe to reference linear resources.

Totality: total
Constructors:

MayThrow : Path
NoThrow : Path

interface PrimIO : List Error -> Type

Parameters: e
Methods:

primIO : IO a -> App e a
primIO1 : (1 _ : IO a) -> App1 e a
fork : (PrimIO e' => App e' ()) -> App e ()

Implementation:

HasErr AppHasIO e => PrimIO e

data SafeBind : Path -> Path -> Type

Totality: total
Constructors:

SafeSame : SafeBind l l
SafeToThrow : SafeBind NoThrow MayThrow

data State : a -> Type -> List Error -> Type

Totality: total
Constructor:

MkState : IORef t -> State tag t e

data Usage : Type

Totality: total
Constructors:

One : Usage
Any : Usage

app : (1 _ : App e a) -> App1 e a

app1 : (1 _ : App1 e a) -> App e a

bindApp1 : (1 _ : App1 e a) -> (1 _ : Cont1Type u a u' e b) -> App1 e b

bindL : App e a -> (1 _ : (a -> App e b)) -> App e b

catch : HasErr err es => App es a -> (err -> App es a) -> App es a

fork : PrimIO e => (PrimIO e' => App e' ()) -> App e ()

get : (0 tag : _) -> State tag t e => App e t

handle : App (err :: e) a -> (a -> App e b) -> (err -> App e b) -> App e b

lift : App e a -> App (err :: e) a

mapState : State tag t e -> State tag t (eff :: e)

modify : (0 tag : _) -> State tag t e => (t -> t) -> App e ()

new : t -> (State tag t e => App e a) -> App e a

new1 : t -> (1 _ : (State tag t e => App1 e a)) -> App1 e a

noThrow : App Init a -> App Init a

primIO : PrimIO e => IO a -> App e a

primIO1 : PrimIO e => (1 _ : IO a) -> App1 e a

put : (0 tag : _) -> State tag t e => t -> App e ()

run : App Init a -> IO a

  The only way provided by `Control.App` to run an App.
  @ Init A concrete list of errors.

throw : HasErr err es => err -> App es a