Defining Interfaces
The only way provided by Control.App
to run an App
is
via the run
function, which takes a concrete list of errors
Init
.
All concrete extensions to this list of errors are via either handle
,
to introduce a new exception, or new
, to introduce a new state.
In order to compose App
programs effectively, rather than
introducing concrete exceptions and state in general, we define interfaces for
collections of operations which work in a specific list of errors.
Example: Console I/O
We have seen an initial example using the Console
interface,
which is declared as follows, in Control.App.Console
:
interface Console e where
putChar : Char -> App {l} e ()
putStr : String -> App {l} e ()
getChar : App {l} e Char
getLine : App {l} e String
It provides primitives for writing to and reading from the console, and
generalising the path parameter to l
means that neither can
throw an exception, because they have to work in both the NoThrow
and MayThrow
contexts.
To implement this for use in a top level IO
program, we need access to primitive IO
operations.
The Control.App
library defines a primitive interface for this:
interface PrimIO e where
primIO : IO a -> App {l} e a
fork : (forall e' . PrimIO e' => App {l} e' ()) -> App e ()
We use primIO
to invoke an IO
function. We also have a fork
primitive, which starts a new thread in a new list of errors supporting
PrimIO
. Note that fork
starts a new list of errors e'
so that states
are only available in a single thread.
There is an implementation of PrimIO
for a list of errors which can
throw the empty type as an exception. This means that if PrimIO
is the only interface available, we cannot throw an exception, which is
consistent with the definition of IO
. This also allows us to
use PrimIO
in the initial list of errors Init
.
HasErr AppHasIO e => PrimIO e where ...
Given this, we can implement Console
and run our hello
program in IO
. It is implemented as follows in Control.App.Console
:
PrimIO e => Console e where
putChar c = primIO $ putChar c
putStr str = primIO $ putStr str
getChar = primIO getChar
getLine = primIO getLine
Example: File I/O
Console I/O can be implemented directly, but most I/O operations can fail.
For example, opening a file can fail for several reasons: the file does not
exist; the user has the wrong permissions, etc. In Idris, the IO
primitive reflects this in its type:
openFile : String -> Mode -> IO (Either FileError File)
While precise, this becomes unwieldy when there are long sequences of
IO
operations. Using App
, we can provide an interface
which throws an exception when an operation fails, and guarantee that any
exceptions are handled at the top level using handle
.
We begin by defining the FileIO
interface, in Control.App.FileIO
:
interface Has [Exception IOError] e => FileIO e where
withFile : String -> Mode ->
(onError : IOError -> App e a) ->
(onOpen : File -> App e a) ->
App e a
fGetStr : File -> App e String
fGetChars : File -> Int -> App e String
fGetChar : File -> App e Char
fPutStr : File -> String -> App e ()
fPutStrLn : File -> String -> App e ()
fflush : File -> App e ()
fEOF : File -> App e Bool
We use resource bracketing - passing a function to withFile
for working
with the opened file - rather than an explicit open
operation,
to open a file, to ensure that the file handle is cleaned up on
completion.
One could also imagine an interface using a linear resource for the file, which
might be appropriate in some safety critical contexts, but for most programming
tasks, exceptions should suffice.
All of the operations can fail, and the interface makes this explicit by
saying we can only implement FileIO
if the list of errors supports
throwing and catching the IOError
exception. IOError
is defined
in Control.App
.
For example, we can use this interface to implement readFile
, throwing
an exception if opening the file fails in withFile
:
readFile : FileIO e => String -> App e String
readFile f = withFile f Read throw $ \h =>
do content <- read [] h
pure (concat content)
where
read : List String -> File -> App e (List String)
read acc h = do eof <- fEOF h
if eof then pure (reverse acc)
else do str <- fGetStr h
read (str :: acc) h
Again, this is defined in Control.App.FileIO
.
To implement FileIO
, we need access to the primitive operations
via PrimIO
, and the ability to throw exceptions if any of the
operations fail. With this, we can implement withFile
as follows,
for example:
Has [PrimIO, Exception IOError] e => FileIO e where
withFile fname m onError proc
= do Right h <- primIO $ openFile fname m
| Left err => onError (FileErr (toFileEx err))
res <- catch (proc h) onError
primIO $ closeFile h
pure res
...
Given this implementation of FileIO
, we can run readFile
,
provided that we wrap it in a top level handle
function to deal
with any errors thrown by readFile
:
readMain : String -> App Init ()
readMain fname = handle (readFile fname)
(\str => putStrLn $ "Success:\n" ++ show str)
(\err : IOError => putStrLn $ "Error: " ++ show err)