git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/docs/effects/depeff.rst
333 lines 12 kB history raw
1.. _sect-depeff:
3*****************
4Dependent Effects
5*****************
7In the programs we have seen so far, the available effects have remained
8constant. Sometimes, however, an operation can *change* the available
9effects. The simplest example occurs when we have a state with a
10dependent type—adding an element to a vector also changes its type, for
11example, since its length is explicit in the type. In this section, we
12will see how the library supports this. Firstly, we will see how states
13with dependent types can be implemented. Secondly, we will see how the
14effects can depend on the *result* of an effectful operation. Finally,
15we will see how this can be used to implement a type-safe and
16resource-safe protocol for file management.
18Dependent States
19================
21Suppose we have a function which reads input from the console, converts
22it to an integer, and adds it to a list which is stored in a ``STATE``.
23It might look something like the following:
25.. code-block:: idris
27 readInt : Eff () [STATE (List Int), STDIO]
28 readInt = do let x = trim !getStr
29 put (cast x :: !get)
31But what if, instead of a list of integers, we would like to store a
32``Vect``, maintaining the length in the type?
34.. code-block:: idris
36 readInt : Eff () [STATE (Vect n Int), STDIO]
37 readInt = do let x = trim !getStr
38 put (cast x :: !get)
40This will not type check! Although the vector has length ``n`` on entry
41to ``readInt``, it has length ``S n`` on exit. The library allows us to
42express this as follows:
44.. code-block:: idris
46 readInt : Eff ()[STATE (Vect n Int), STDIO]
47 [STATE (Vect (S n) Int), STDIO]
48 readInt = do let x = trim !getStr
49 putM (cast x :: !get)
51The type ``Eff a xs xs'`` means that the operation
52begins with effects ``xs`` available, and ends with effects ``xs’``
53available. We have used ``putM`` to update the state, where the ``M``
54suffix indicates that the *type* is being updated as well as the value.
55It has the following type:
57.. code-block:: idris
59 putM : y -> Eff () [STATE x] [STATE y]
61Result-dependent Effects
62========================
64Often, whether a state is updated could depend on the success or
65otherwise of an operation. In our ``readInt`` example, we might wish to
66update the vector only if the input is a valid integer (i.e. all
67digits). As a first attempt, we could try the following, returning a
68``Bool`` which indicates success:
70.. code-block:: idris
72 readInt : Eff Bool [STATE (Vect n Int), STDIO]
73 [STATE (Vect (S n) Int), STDIO]
74 readInt = do let x = trim !getStr
75 case all isDigit (unpack x) of
76 False => pure False
77 True => do putM (cast x :: !get)
78 pure True
80Unfortunately, this will not type check because the vector does not get
81extended in both branches of the ``case``!
83::
85 MutState.idr:18:19:When elaborating right hand side of Main.case
86 block in readInt:
87 Unifying n and S n would lead to infinite value
89Clearly, the size of the resulting vector depends on whether or not the
90value read from the user was valid. We can express this in the type:
92.. code-block:: idris
94 readInt : Eff Bool [STATE (Vect n Int), STDIO]
95 (\ok => if ok then [STATE (Vect (S n) Int), STDIO]
96 else [STATE (Vect n Int), STDIO])
97 readInt = do let x = trim !getStr
98 case all isDigit (unpack x) of
99 False => pureM False
100 True => do putM (cast x :: !get)
101 pureM True
103Using ``pureM`` rather than ``pure`` allows the output effects to be
104calculated from the value given. Its type is:
106.. code-block:: idris
108 pureM : (val : a) -> EffM m a (xs val) xs
110When using ``readInt``, we will have to check its return
111value in order to know what the new set of effects is. For example, to
112read a set number of values into a vector, we could write the following:
114.. code-block:: idris
116 readN : (n : Nat) ->
117 Eff () [STATE (Vect m Int), STDIO]
118 [STATE (Vect (n + m) Int), STDIO]
119 readN Z = pure ()
120 readN {m} (S k) = case !readInt of
121 True => rewrite plusSuccRightSucc k m in readN k
122 False => readN (S k)
124The ``case`` analysis on the result of ``readInt`` means that we know in
125each branch whether reading the integer succeeded, and therefore how
126many values still need to be read into the vector. What this means in
127practice is that the type system has verified that a necessary dynamic
128check (i.e. whether reading a value succeeded) has indeed been done.
130.. note::
131 Only ``case`` will work here. We cannot use ``if/then/else``
132 because the ``then`` and ``else`` branches must have the same
133 type. The ``case`` construct, however, abstracts over the value
134 being inspected in the type of each branch.
136File Management
137===============
139A practical use for dependent effects is in specifying resource usage
140protocols and verifying that they are executed correctly. For example,
141file management follows a resource usage protocol with the following
142(informally specified) requirements:
144- It is necessary to open a file for reading before reading it
146- Opening may fail, so the programmer should check whether opening was
147 successful
149- A file which is open for reading must not be written to, and vice
150 versa
152- When finished, an open file handle should be closed
154- When a file is closed, its handle should no longer be used
156These requirements can be expressed formally in , by creating a
157``FILE_IO`` effect parameterised over a file handle state, which is
158either empty, open for reading, or open for writing. The ``FILE_IO``
159effect’s definition is given below. Note that this
160effect is mainly for illustrative purposes—typically we would also like
161to support random access files and better reporting of error conditions.
163.. code-block:: idris
165 module Effect.File
167 import Effects
168 import Control.IOExcept
170 FILE_IO : Type -> EFFECT
172 data OpenFile : Mode -> Type
174 open : (fname : String)
175 -> (m : Mode)
176 -> Eff Bool [FILE_IO ()]
177 (\res => [FILE_IO (case res of
178 True => OpenFile m
179 False => ())])
180 close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
182 readLine : Eff String [FILE_IO (OpenFile Read)]
183 writeLine : String -> Eff () [FILE_IO (OpenFile Write)]
184 eof : Eff Bool [FILE_IO (OpenFile Read)]
186 Handler FileIO IO where { ... }
188In particular, consider the type of ``open``:
190.. code-block:: idris
192 open : (fname : String)
193 -> (m : Mode)
194 -> Eff Bool [FILE_IO ()]
195 (\res => [FILE_IO (case res of
196 True => OpenFile m
197 False => ())])
199This returns a ``Bool`` which indicates whether opening the file was
200successful. The resulting state depends on whether the operation was
201successful; if so, we have a file handle open for the stated purpose,
202and if not, we have no file handle. By ``case`` analysis on the result,
203we continue the protocol accordingly.
205.. _eff-readfile:
206.. code-block:: idris
208 readFile : Eff (List String) [FILE_IO (OpenFile Read)]
209 readFile = readAcc [] where
210 readAcc : List String -> Eff (List String) [FILE_IO (OpenFile Read)]
211 readAcc acc = if (not !eof)
212 then readAcc (!readLine :: acc)
213 else pure (reverse acc)
215Given a function ``readFile``, above, which reads from
216an open file until reaching the end, we can write a program which opens
217a file, reads it, then displays the contents and closes it, as follows,
218correctly following the protocol:
220.. code-block:: idris
222 dumpFile : String -> Eff () [FILE_IO (), STDIO]
223 dumpFile name = case !(open name Read) of
224 True => do putStrLn (show !readFile)
225 close
226 False => putStrLn ("Error!")
228The type of ``dumpFile``, with ``FILE_IO ()`` in its effect list,
229indicates that any use of the file resource will follow the protocol
230correctly (i.e. it both begins and ends with an empty resource). If we
231fail to follow the protocol correctly (perhaps by forgetting to close
232the file, failing to check that ``open`` succeeded, or opening the file
233for writing) then we will get a compile-time error. For example,
234changing ``open name Read`` to ``open name Write`` yields a compile-time
235error of the following form:
237::
239 FileTest.idr:16:18:When elaborating right hand side of Main.case
240 block in testFile:
241 Can't solve goal
242 SubList [(FILE_IO (OpenFile Read))]
243 [(FILE_IO (OpenFile Write)), STDIO]
245In other words: when reading a file, we need a file which is open for
246reading, but the effect list contains a ``FILE_IO`` effect carrying a
247file open for writing.
249Pattern-matching bind
250=====================
252It might seem that having to test each potentially failing operation
253with a ``case`` clause could lead to ugly code, with lots of
254nested case blocks. Many languages support exceptions to improve this,
255but unfortunately exceptions may not allow completely clean resource
256management—for example, guaranteeing that any ``open`` which did succeed
257has a corresponding close.
259Idris supports *pattern-matching* bindings, such as the following:
261.. code-block:: idris
263 dumpFile : String -> Eff () [FILE_IO (), STDIO]
264 dumpFile name = do True <- open name Read
265 putStrLn (show !readFile)
266 close
268This also has a problem: we are no longer dealing with the case where
269opening a file failed! The solution is to extend the pattern-matching
270binding syntax to give brief clauses for failing matches. Here, for
271example, we could write:
273.. code-block:: idris
275 dumpFile : String -> Eff () [FILE_IO (), STDIO]
276 dumpFile name = do True <- open name Read | False => putStrLn "Error"
277 putStrLn (show !readFile)
278 close
280This is exactly equivalent to the definition with the explicit ``case``.
281In general, in a ``do``-block, the syntax:
283.. code-block:: idris
285 do pat <- val | <alternatives>
286 p
288is desugared to
290.. code-block:: idris
292 do x <- val
293 case x of
294 pat => p
295 <alternatives>
297There can be several ``alternatives``, separated by a vertical bar
298``|``. For example, there is a ``SYSTEM`` effect which supports
299reading command line arguments, among other things (see Appendix
300:ref:`sect-appendix`). To read command line arguments, we can use
301``getArgs``:
303.. code-block:: idris
305 getArgs : Eff (List String) [SYSTEM]
307A main program can read command line arguments as follows, where in the
308list which is returned, the first element ``prog`` is the executable
309name and the second is an expected argument:
311.. code-block:: idris
313 emain : Eff () [SYSTEM, STDIO]
314 emain = do [prog, arg] <- getArgs
315 putStrLn $ "Argument is " ++ arg
316 {- ... rest of function ... -}
318Unfortunately, this will not fail gracefully if no argument is given, or
319if too many arguments are given. We can use pattern matching bind
320alternatives to give a better (more informative) error:
322.. code-block:: idris
324 emain : Eff () [SYSTEM, STDIO]
325 emain = do [prog, arg] <- getArgs | [] => putStrLn "Can't happen!"
326 | [prog] => putStrLn "No arguments!"
327 | _ => putStrLn "Too many arguments!"
328 putStrLn $ "Argument is " ++ arg
329 {- ... rest of function ... -}
331If ``getArgs`` does not return something of the form ``[prog, arg]`` the
332alternative which does match is executed instead, and that value
333returned.