git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/docs/effects/summary.rst
152 lines 3.2 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 -> Eff b [EXCEPTION a]
25 Handler (Exception a) Maybe where { ... }
26 Handler (Exception a) List where { ... }
27 Handler (Exception a) (Either a) where { ... }
28 Handler (Exception a) (IOExcept a) where { ... }
29 Show a => Handler (Exception a) IO where { ... }
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 : (fname : String)
46 -> (m : Mode)
47 -> Eff Bool [FILE_IO ()]
48 (\res => [FILE_IO (case res of
49 True => OpenFile m
50 False => ())])
51 close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
53 readLine : Eff String [FILE_IO (OpenFile Read)]
54 writeLine : String -> Eff () [FILE_IO (OpenFile Write)]
55 eof : Eff Bool [FILE_IO (OpenFile Read)]
57 Handler FileIO IO where { ... }
59RND
60===
62.. code-block:: idris
64 module Effect.Random
66 import Effects
67 import Data.Vect
68 import Data.Fin
70 RND : EFFECT
72 srand : Integer -> Eff m () [RND]
73 rndInt : Integer -> Integer -> Eff m Integer [RND]
74 rndFin : (k : Nat) -> Eff m (Fin (S k)) [RND]
76 Handler Random m where { ... }
78SELECT
79======
81.. code-block:: idris
83 module Effect.Select
85 import Effects
87 SELECT : EFFECT
89 select : List a -> Eff m a [SELECT]
91 Handler Selection Maybe where { ... }
92 Handler Selection List where { ... }
94STATE
95=====
97.. code-block:: idris
99 module Effect.State
101 import Effects
103 STATE : Type -> EFFECT
105 get : Eff m x [STATE x]
106 put : x -> Eff m () [STATE x]
107 putM : y -> Eff m () [STATE x] [STATE y]
108 update : (x -> x) -> Eff m () [STATE x]
110 Handler State m where { ... }
112STDIO
113=====
115.. code-block:: idris
117 module Effect.StdIO
119 import Effects
120 import Control.IOExcept
122 STDIO : EFFECT
124 putChar : Handler StdIO m => Char -> Eff m () [STDIO]
125 putStr : Handler StdIO m => String -> Eff m () [STDIO]
126 putStrLn : Handler StdIO m => String -> Eff m () [STDIO]
128 getStr : Handler StdIO m => Eff m String [STDIO]
129 getChar : Handler StdIO m => Eff m Char [STDIO]
131 Handler StdIO IO where { ... }
132 Handler StdIO (IOExcept a) where { ... }
134SYSTEM
135======
137.. code-block:: idris
139 module Effect.System
141 import Effects
142 import System
143 import Control.IOExcept
145 SYSTEM : EFFECT
147 getArgs : Handler System e => Eff e (List String) [SYSTEM]
148 time : Handler System e => Eff e Int [SYSTEM]
149 getEnv : Handler System e => String -> Eff e (Maybe String) [SYSTEM]
151 Handler System IO where { ... }
152 Handler System (IOExcept a) where { ... }