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.
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:
27 readInt : { [STATE (List Int), STDIO] } Eff ()
28 readInt = do let x = trim !getStr
31But what if, instead of a list of integers, we would like to store a
32``Vect``, maintaining the length in the type?
36 readInt : { [STATE (Vect n Int), STDIO] } Eff ()
37 readInt = do let x = trim !getStr
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:
46 readInt : { [STATE (Vect n Int), STDIO] ==>
47 [STATE (Vect (S n) Int), STDIO] } Eff ()
48 readInt = do let x = trim !getStr
51The notation ``{ xs ==> xs’ } Eff a`` in a type 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:
59 putM : y -> { [STATE x] ==> [STATE y] } Eff ()
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:
72 readInt : { [STATE (Vect n Int), STDIO] ==>
73 [STATE (Vect (S n) Int), STDIO] } Eff Bool
74 readInt = do let x = trim !getStr
75 case all isDigit (unpack x) of
77 True => do putM (cast x :: !get)
80Unfortunately, this will not type check because the vector does not get
81extended in both branches of the ``case``!
85 MutState.idr:18:19:When elaborating right hand side of Main.case
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:
94 readInt : { [STATE (Vect n Int), STDIO] ==>
95 {ok} if ok then [STATE (Vect (S n) Int), STDIO]
96 else [STATE (Vect n Int), STDIO] } Eff Bool
97 readInt = do let x = trim !getStr
98 case all isDigit (unpack x) of
100 True => do putM (cast x :: !get)
103The notation ``{ xs ==> res xs’ } Eff a`` in a type means that the
104effects available are updated from ``xs`` to ``xs’``, *and* the
105resulting effects ``xs’`` may depend on the result of the operation
106``res``, of type ``a``. Here, the resulting effects are computed from
107the result ``ok``—if ``True``, the vector is extended, otherwise it
110When using the function, we will naturally 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:
117 { [STATE (Vect m Int), STDIO] ==>
118 [STATE (Vect (n + m) Int), STDIO] } Eff ()
120 readN {m} (S k) = case !readInt of
121 True => rewrite plusSuccRightSucc k m in readN 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.
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.
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
149- A file which is open for reading must not be written to, and vice
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 in Listing :ref:`eff-fileio`. 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.
165 :caption: File I/O Effect
170 import Control.IOExcept
172 FILE_IO : Type -> EFFECT
174 data OpenFile : Mode -> Type
176 open : String -> (m : Mode) ->
178 {ok} [FILE_IO (if ok then OpenFile m else ())] } Eff Bool
179 close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff ()
181 readLine : { [FILE_IO (OpenFile Read)] } Eff String
182 writeLine : { [FILE_IO (OpenFile Write)] } Eff ()
183 eof : { [FILE_IO (OpenFile Read)] } Eff Bool
185 instance Handler FileIO IO
187In particular, consider the type of ``open``:
191 open : String -> (m : Mode) ->
193 {ok} [FILE_IO (if ok then OpenFile m else ())] } Eff Bool
195This returns a ``Bool`` which indicates whether opening the file was
196successful. The resulting state depends on whether the operation was
197successful; if so, we have a file handle open for the stated purpose,
198and if not, we have no file handle. By ``case`` analysis on the result,
199we continue the protocol accordingly.
203 :caption: Reading a File
205 readFile : { [FILE_IO (OpenFile Read)] } Eff (List String)
206 readFile = readAcc [] where
207 readAcc : List String -> { [FILE_IO (OpenFile Read)] }
209 readAcc acc = if (not !eof)
210 then readAcc (!readLine :: acc)
211 else pure (reverse acc)
213Given a function ``readFile`` (Listing :ref:`eff-readfile`) which reads from
214an open file until reaching the end, we can write a program which opens
215a file, reads it, then displays the contents and closes it, as follows,
216correctly following the protocol:
220 dumpFile : String -> { [FILE_IO (), STDIO] } Eff ()
221 dumpFile name = case !(open name Read) of
222 True => do putStrLn (show !readFile)
224 False => putStrLn ("Error!")
226The type of ``dumpFile``, with ``FILE_IO ()`` in its effect list,
227indicates that any use of the file resource will follow the protocol
228correctly (i.e. it both begins and ends with an empty resource). If we
229fail to follow the protocol correctly (perhaps by forgetting to close
230the file, failing to check that ``open`` succeeded, or opening the file
231for writing) then we will get a compile-time error. For example,
232changing ``open name Read`` to ``open name Write`` yields a compile-time
233error of the following form:
237 FileTest.idr:16:18:When elaborating right hand side of Main.case
240 SubList [(FILE_IO (OpenFile Read))]
241 [(FILE_IO (OpenFile Write)), STDIO]
243In other words: when reading a file, we need a file which is open for
244reading, but the effect list contains a ``FILE_IO`` effect carrying a
245file open for writing.
250It might seem that having to test each potentially failing operation
251with a ``case`` clause could lead to ugly code, with lots of
252nested case blocks. Many languages support exceptions to improve this,
253but unfortunately exceptions may not allow completely clean resource
254management—for example, guaranteeing that any ``open`` which did succeed
255has a corresponding close.
257Idris supports *pattern-matching* bindings, such as the following:
261 dumpFile : String -> { [FILE_IO (), STDIO] } Eff ()
262 dumpFile name = do True <- open name Read
263 putStrLn (show !readFile)
266This also has a problem: we are no longer dealing with the case where
267opening a file failed! The solution is to extend the pattern-matching
268binding syntax to give brief clauses for failing matches. Here, for
269example, we could write:
273 dumpFile : String -> { [FILE_IO (), STDIO] } Eff ()
274 dumpFile name = do True <- open name Read | False => putStrLn "Error"
275 putStrLn (show !readFile)
278This is exactly equivalent to the definition with the explicit ``case``.
279In general, in a ``do``-block, the syntax:
283 do pat <- val | <alternatives>
295There can be several ``alternatives``, separated by a vertical bar
296``|``. For example, there is a ``SYSTEM`` effect which supports
297reading command line arguments, among other things (see Appendix
298:ref:`sect-appendix`). To read command line arguments, we can use
303 getArgs : { [SYSTEM] } Eff (List String)
305A main program can read command line arguments as follows, where in the
306list which is returned, the first element ``prog`` is the executable
307name and the second is an expected argument:
311 emain : { [SYSTEM, STDIO] } Eff ()
312 emain = do [prog, arg] <- getArgs
313 putStrLn $ "Argument is " ++ arg
314 {- ... rest of function ... -}
316Unfortunately, this will not fail gracefully if no argument is given, or
317if too many arguments are given. We can use pattern matching bind
318alternatives to give a better (more informative) error:
322 emain : { [SYSTEM, STDIO] } Eff ()
323 emain = do [prog, arg] <- getArgs | [] => putStrLn "Can't happen!"
324 | [prog] => putStrLn "No arguments!"
325 | _ => putStrLn "Too many arguments!"
326 putStrLn $ "Argument is " ++ arg
327 {- ... rest of function ... -}
329If ``getArgs`` does not return something of the form ``[prog, arg]`` the
330alternative which does match is executed instead, and that value
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list