Idris2Doc : Control.App

Control.App

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

  Visibility: public export
data HasErr : Error -> List Error -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Here : HasErr e (e :: es)
  
There : HasErr e es -> HasErr e (e' :: es)

  Hint: 
HasErr AppHasIO e => PrimIO e
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
  Visibility: public export
  Constructors:
  
MayThrow : Path
  
NoThrow : Path

  Hints:
  
Applicative (App es)
  
Functor (App es)
  
Uninhabited (OneOf [] p)
data Usage : Type
  Totality: total
  Visibility: public export
  Constructors:
  
One : Usage
  
Any : Usage
0 Has : List (a -> Type) -> a -> Type
  Visibility: public export
data SafeBind : Path -> Path -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
SafeSame : SafeBind l l
  
SafeToThrow : SafeBind NoThrow MayThrow
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
  Visibility: export
  Constructor: 
MkApp : (1 _ : ((1 _ : %World) -> AppRes (execTy l e t))) -> App e t

  Hints:
  
Applicative (App es)
  
Functor (App es)
  
Monad (App es)
data App1 : {default One _ : Usage} -> List Error -> Type -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkApp1 : (1 _ : ((1 _ : %World) -> App1Res u t)) -> App1 e t
Cont1Type : Usage -> Type -> Usage -> List Error -> Type -> Type
  Visibility: public export
bindApp1 : (1 _ : App1 e a) -> (1 _ : Cont1Type u a u' e b) -> App1 e b
  Visibility: export
data AppHasIO : Type
  When type is present in app "errors" list, app is allowed to perform I/O.

  Totality: total
  Visibility: public export
  Hints:
  
HasErr AppHasIO e => PrimIO e
  
Uninhabited AppHasIO
bindL : App e a -> (1 _ : (a -> App e b)) -> App e b
  Visibility: export
seqL : App e () -> (1 _ : App e b) -> App e b
  Visibility: export
app : (1 _ : App e a) -> App1 e a
  Visibility: export
app1 : (1 _ : App1 e a) -> App e a
  Visibility: export
(>>=) : SafeBind l l' => App e a -> (a -> App e b) -> App e b
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(>>=) : (1 _ : App1 e a) -> (1 _ : Cont1Type u a u' e b) -> App1 e b
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(>>) : (1 _ : App1 e ()) -> (1 _ : App1 e b) -> App1 e b
  Visibility: export
  Fixity Declaration: infixl operator, level 1
pure : a -> App1 e a
  Visibility: export
pure1 : (1 _ : a) -> App1 e a
  Visibility: export
data State : a -> Type -> List Error -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkState : IORef t -> State tag t e

  Hint: 
State tag t e -> State tag t (eff :: e)
mapState : State tag t e -> State tag t (eff :: e)
  Visibility: export
get : (0 tag : {_:2831}) -> State tag t e => App e t
  Visibility: export
put : (0 tag : {_:2883}) -> State tag t e => t -> App e ()
  Visibility: export
modify : (0 tag : {_:2941}) -> State tag t e => (t -> t) -> App e ()
  Visibility: export
new : t -> (State tag t e => App e a) -> App e a
  Visibility: export
Exception : Error -> List Error -> Type
  An alias for `HasErr`.

  Visibility: public export
throw : HasErr err es => err -> App es a
  Visibility: export
catch : HasErr err es => App es a -> (err -> App es a) -> App es a
  Visibility: export
handle : App (err :: e) a -> (a -> App e b) -> (err -> App e b) -> App e b
  Visibility: export
lift : App e a -> App (err :: e) a
  Visibility: export
Init : List Error
  Visibility: public export
run : App Init a -> IO a
  The only way provided by `Control.App` to run an App.
  @ Init A concrete list of errors.

  Visibility: export
noThrow : App Init a -> App Init a
  Visibility: export
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
primIO : PrimIO e => IO a -> App e a
  Visibility: public export
primIO1 : PrimIO e => (1 _ : IO a) -> App1 e a
  Visibility: public export
fork : PrimIO e => (PrimIO e' => App e' ()) -> App e ()
  Visibility: public export
new1 : t -> (1 _ : (State tag t e => App1 e a)) -> App1 e a
  Visibility: export
data FileEx : Type
  Totality: total
  Visibility: public export
  Constructors:
  
GenericFileEx : Int -> FileEx
  
FileReadError : FileEx
  
FileWriteError : FileEx
  
FileNotFound : FileEx
  
PermissionDenied : FileEx
  
FileExists : FileEx

  Hint: 
Show FileEx
data IOError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
GenericErr : String -> IOError
  
FileErr : FileEx -> IOError

  Hint: 
Show IOError