Effects Summary¶
This appendix gives interfaces for the core effects provided by the library.
EXCEPTION¶
module Effect.Exception
import Effects
import System
import Control.IOExcept
EXCEPTION : Type -> EFFECT
raise : a -> { [EXCEPTION a ] } Eff m b
instance Handler (Exception a) Maybe
instance Handler (Exception a) List
instance Handler (Exception a) (Either a)
instance Handler (Exception a) (IOExcept a)
instance Show a => Handler (Exception a) IO
FILE_IO¶
module Effect.File
import Effects
import Control.IOExcept
FILE_IO : Type -> EFFECT
data OpenFile : Mode -> Type
open : Handler FileIO e => String -> (m : Mode) ->
{ [FILE_IO ()] ==>
{ok} [FILE_IO (if ok then OpenFile m else ())] } Eff e Bool
close : Handler FileIO e =>
{ [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
readLine : Handler FileIO e =>
{ [FILE_IO (OpenFile Read)] } Eff e String
writeLine : Handler FileIO e => String ->
{ [FILE_IO (OpenFile Write)] } Eff e ()
eof : Handler FileIO e =>
{ [FILE_IO (OpenFile Read)] } Eff e Bool
instance Handler FileIO IO
RND¶
module Effect.Random
import Effects
import Data.Vect
import Data.Fin
RND : EFFECT
srand : Integer -> { [RND] } Eff m ()
rndInt : Integer -> Integer -> { [RND] } Eff m Integer
rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
instance Handler Random m
SELECT¶
module Effect.Select
import Effects
SELECT : EFFECT
select : List a -> { [SELECT] } Eff m a
instance Handler Selection Maybe
instance Handler Selection List
STATE¶
module Effect.State
import Effects
STATE : Type -> EFFECT
get : { [STATE x] } Eff m x
put : x -> { [STATE x] } Eff m ()
putM : y -> { [STATE x] ==> [STATE y] } Eff m ()
update : (x -> x) -> { [STATE x] } Eff m ()
instance Handler State m
STDIO¶
module Effect.StdIO
import Effects
import Control.IOExcept
STDIO : EFFECT
putChar : Handler StdIO m => Char -> { [STDIO] } Eff m ()
putStr : Handler StdIO m => String -> { [STDIO] } Eff m ()
putStrLn : Handler StdIO m => String -> { [STDIO] } Eff m ()
getStr : Handler StdIO m => { [STDIO] } Eff m String
getChar : Handler StdIO m => { [STDIO] } Eff m Char
instance Handler StdIO IO
instance Handler StdIO (IOExcept a)
SYSTEM¶
module Effect.System
import Effects
import System
import Control.IOExcept
SYSTEM : EFFECT
getArgs : Handler System e => { [SYSTEM] } Eff e (List String)
time : Handler System e => { [SYSTEM] } Eff e Int
getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)
instance Handler System IO
instance Handler System (IOExcept a)