git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/docs/effects/summary.rst
153 lines 3.3 kB history raw
1.. _sect-appendix:
3***************
4Effects Summary
5***************
7This appendix gives interfaces for the core effects provided by the
8library.
10EXCEPTION
11=========
13.. code-block:: idris
15 module Effect.Exception
17 import Effects
18 import System
19 import Control.IOExcept
21 EXCEPTION : Type -> EFFECT
23 raise : a -> { [EXCEPTION a ] } Eff m b
25 instance Handler (Exception a) Maybe
26 instance Handler (Exception a) List
27 instance Handler (Exception a) (Either a)
28 instance Handler (Exception a) (IOExcept a)
29 instance Show a => Handler (Exception a) IO
31FILE\_IO
32========
34.. code-block:: idris
36 module Effect.File
38 import Effects
39 import Control.IOExcept
41 FILE_IO : Type -> EFFECT
43 data OpenFile : Mode -> Type
45 open : Handler FileIO e => String -> (m : Mode) ->
46 { [FILE_IO ()] ==>
47 {ok} [FILE_IO (if ok then OpenFile m else ())] } Eff e Bool
48 close : Handler FileIO e =>
49 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
51 readLine : Handler FileIO e =>
52 { [FILE_IO (OpenFile Read)] } Eff e String
53 writeLine : Handler FileIO e => String ->
54 { [FILE_IO (OpenFile Write)] } Eff e ()
55 eof : Handler FileIO e =>
56 { [FILE_IO (OpenFile Read)] } Eff e Bool
58 instance Handler FileIO IO
60RND
61===
63.. code-block:: idris
65 module Effect.Random
67 import Effects
68 import Data.Vect
69 import Data.Fin
71 RND : EFFECT
73 srand : Integer -> { [RND] } Eff m ()
74 rndInt : Integer -> Integer -> { [RND] } Eff m Integer
75 rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
77 instance Handler Random m
79SELECT
80======
82.. code-block:: idris
84 module Effect.Select
86 import Effects
88 SELECT : EFFECT
90 select : List a -> { [SELECT] } Eff m a
92 instance Handler Selection Maybe
93 instance Handler Selection List
95STATE
96=====
98.. code-block:: idris
100 module Effect.State
102 import Effects
104 STATE : Type -> EFFECT
106 get : { [STATE x] } Eff m x
107 put : x -> { [STATE x] } Eff m ()
108 putM : y -> { [STATE x] ==> [STATE y] } Eff m ()
109 update : (x -> x) -> { [STATE x] } Eff m ()
111 instance Handler State m
113STDIO
114=====
116.. code-block:: idris
118 module Effect.StdIO
120 import Effects
121 import Control.IOExcept
123 STDIO : EFFECT
125 putChar : Handler StdIO m => Char -> { [STDIO] } Eff m ()
126 putStr : Handler StdIO m => String -> { [STDIO] } Eff m ()
127 putStrLn : Handler StdIO m => String -> { [STDIO] } Eff m ()
129 getStr : Handler StdIO m => { [STDIO] } Eff m String
130 getChar : Handler StdIO m => { [STDIO] } Eff m Char
132 instance Handler StdIO IO
133 instance Handler StdIO (IOExcept a)
135SYSTEM
136======
138.. code-block:: idris
140 module Effect.System
142 import Effects
143 import System
144 import Control.IOExcept
146 SYSTEM : EFFECT
148 getArgs : Handler System e => { [SYSTEM] } Eff e (List String)
149 time : Handler System e => { [SYSTEM] } Eff e Int
150 getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)
152 instance Handler System IO
153 instance Handler System (IOExcept a)