Some documentation updates

Remove things from CONTRIBUTING that are done, and initial App
documentation (though it could use more examples).
This commit is contained in:
Edwin Brady 2020-05-25 09:03:08 +01:00
parent f841f4a48a
commit 2206692533
7 changed files with 605 additions and 11 deletions

View File

@ -4,7 +4,6 @@ Contributing to Idris 2
Contributions are welcome! The most important things needed at this stage, Contributions are welcome! The most important things needed at this stage,
beyond work on the language core, are (in no particular order): beyond work on the language core, are (in no particular order):
* CI integration.
* Documentation string support (at the REPL and IDE mode). * Documentation string support (at the REPL and IDE mode).
* Generating HTML documentation from documentation strings (and possibly other * Generating HTML documentation from documentation strings (and possibly other
formations) formations)
@ -22,8 +21,6 @@ beyond work on the language core, are (in no particular order):
- (Not really part of Idris 2, but an editing mode for vim would be lovely!) - (Not really part of Idris 2, but an editing mode for vim would be lovely!)
* Some parts of the Idris 1 Prelude are not yet implemented and should be * Some parts of the Idris 1 Prelude are not yet implemented and should be
added to base/ added to base/
* Partial evaluation, especially for specialisation of interface
implementations.
* The lexer and parser are quite slow, new and faster versions with better * The lexer and parser are quite slow, new and faster versions with better
errors would be good. errors would be good.
- In particular, large sections commented out with {- -} can take a while - In particular, large sections commented out with {- -} can take a while
@ -47,8 +44,6 @@ notably:
- This will necessarily be slightly different from Idris 1 since the - This will necessarily be slightly different from Idris 1 since the
elaborator works differently. It would also be nice to extend it with elaborator works differently. It would also be nice to extend it with
libraries and perhaps syntax for deriving implementations of interfaces. libraries and perhaps syntax for deriving implementations of interfaces.
* `%default` directives, since coverage and totality checking have not been well
tested yet.
Other contributions are also welcome, but I (@edwinb) will need to be Other contributions are also welcome, but I (@edwinb) will need to be
confident that I'll be able to maintain them! confident that I'll be able to maintain them!
@ -74,11 +69,6 @@ behaviour might be useful in a proof (so very small definitions) are
Syntax Syntax
------ ------
Some syntax that hasn't yet been implemented but will be:
* Idiom brackets
* !-notation [needs some thought about the exact rules]
Some things from Idris 1 definitely won't be implemented: Some things from Idris 1 definitely won't be implemented:
* `%access` directives, because it's too easy to export things by accident * `%access` directives, because it's too easy to export things by accident

View File

@ -0,0 +1,88 @@
Exceptions and State
====================
``Control.App`` is primarily intended to make it easier to manage the common
cases of applications with exceptions and state. We can throw and catch
exceptions listed in the environment (the ``e`` parameter to ``App``) and
introduce new global state.
Exceptions
----------
The ``Environment`` is a list of error types, usable via the
``Exception`` interface defined in ``Control.App``:
.. code-block:: idris
interface Exception err e where
throw : err -> App e a
catch : App e a -> (err -> App e a) -> App e a
We can use ``throw`` and ``catch`` for some exception type
``err`` as long as the exception type exists in the environment. This is
checked with the ``HasErr`` predicate, also defined in ``Control.App``:
.. code-block:: idris
data HasErr : Type -> Environment -> Type where
Here : HasErr e (e :: es)
There : HasErr e es -> HasErr e (e' :: es)
HasErr err e => Exception err e where ...
Note the ``HasErr`` constraint on ``Exception``: this is one place
where it is notationally convenient that the ``auto`` implicit mechanism
and the interface resolution mechanism are identical in Idris 2.
Finally, we can introduce new exception types via ``handle``, which runs a
block of code which might throw, handling any exceptions:
.. code-block:: idris
handle : App (err :: e) a -> (onok : a -> App e b) ->
(onerr : err -> App e b) -> App e b
Adding State
------------
Applications will typically need to keep track of state, and we support
this primitively in ``App`` using a ``State`` type, defined in
``Control.App``:
.. code-block:: idris
data State : (tag : a) -> Type -> Environment -> Type
The ``tag`` is used purely to distinguish between different states,
and is not required at run-time, as explicitly stated in the types of
``get`` and ``put``, which are used to access and update a state:
.. code-block:: idris
get : (0 tag : a) -> State tag t e => App {l} e t
put : (0 tag : a) -> State tag t e => t -> App {l} e ()
These use an ``auto``-implicit to pass around
a ``State`` with the relevant ``tag`` implicitly, so we refer
to states by tag alone. In ``helloCount`` earlier, we used an empty type
\texttt{Counter} as the tag:
.. code-block:: idris
data Counter : Type where -- complete definition
The environment ``e`` is used to ensure that
states are only usable in the environment in which they are introduced.
States are introduced using ``new``:
.. code-block:: idris
new : t -> (1 p : State tag t e => App {l} e a) -> App {l} e a
Note that the type tells us ``new`` runs the program with the state
exactly once.
Rather than using ``State`` and ``Exception`` directly, however,
we typically use interfaces to constrain the operations which are allowed
in an environment. Internally, ``State`` is implemented via an
``IORef``, primarily for performance reasons.

View File

@ -46,4 +46,11 @@ We begin by introducing ``App``, with some small example
programs, then show how to extend it with exceptions, state, and other programs, then show how to extend it with exceptions, state, and other
interfaces. interfaces.
[To be continued...] .. toctree::
:maxdepth: 1
introapp
exceptionsstate
interfaces
linear

View File

@ -0,0 +1,148 @@
Defining Interfaces
===================
The only way provided by ``Control.App`` to run an ``App`` is
via the ``run`` function, which takes a concrete environment
``Init``.
All concrete extensions to this environment 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 environment.
Example: Console I/O
--------------------
We have seen an initial example using the ``Console`` interface,
which is declared as follows, in ``Control.App.Console``:
.. code-block:: idris
interface Console e where
putStr : String -> App {l} e ()
getStr : 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:
.. code-block:: idris
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 environment supporting
``PrimIO``. Note that ``fork`` starts a new environment ``e'`` so that states
are only available in a single thread.
There is an implementation of ``PrimIO`` for an environment 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 environment ``Init``.
.. code-block:: idris
HasErr Void e => PrimIO e where ...
Given this, we can implement \texttt{Console} and run our \texttt{hello}
program in ``IO``. It is implemented as follows in ``Control.App.Console``:
.. code-block:: idris
PrimIO e => Console e where
putStr str = primIO $ putStr str
getStr = 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:
.. code-block:: idris
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``:
.. code-block:: idris
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
fPutStr : File -> String -> 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 environment 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``:
.. code-block:: idris
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:
.. code-block:: idris
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
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``:
.. code-block:: idris
readMain : String -> App Init ()
readMain fname = handle (readFile fname)
(\str => putStrLn $ "Success:\n" ++ show str)
(\err : IOError => putStrLn $ "Error: " ++ show err)

View File

@ -0,0 +1,108 @@
Introducing App
===============
``App`` is declared as below, in a module ``Control.App``, which is part of
the ``base`` libraries.
It is parameterised by an implicit
``Path`` (which states whether the program's execution path
is linear or might throw
exceptions), which has a ``default`` value that the program
might throw, and an ``Environment``
(which gives a list of exception types which can be thrown, and is
a synonym for ``List Type``):
.. code-block:: idris
data App : {default MayThrow l : Path} ->
(e : Environment) -> Type -> Type
It serves the same purpose as ``IO``, but supports throwing and catching
exceptions, and allows us to define more constrained interfaces parameterised
by the environment ``e``.
e.g. a program which supports console IO:
.. code-block:: idris
hello : Console e => App e ()
hello = putStrLn "Hello, App world!"
We can use this in a complete program as follows:
.. code-block:: idris
module Main
import Control.App
import Control.App.Console
hello : Console e => App e ()
hello = putStrLn "Hello, App world!"
main : IO ()
main = run hello
Or, a program which supports console IO and carries an ``Int`` state,
labelled ``Counter``:
.. code-block:: idris
data Counter : Type where
helloCount : (Console e, State Counter Int e) => App e ()
helloCount = do c <- get Counter
put Counter (c + 1)
putStrLn "Hello, counting world"
c <- get Counter
putStrLn ("Counter " ++ show c)
To run this as part of a complete program, we need to initialise the state.
.. code-block:: idris
main : IO ()
main = run (new 93 helloCount)
For convenience, we can list multiple interfaces in one go, using a function
``Has``, defined in ``Control.App``, to compute the interface constraints:
.. code-block:: idris
helloCount : Has [Console, State Counter Int] e => App e ()
0 Has : List (a -> Type) -> a -> Type
Has [] es = ()
Has (e :: es') es = (e es, Has es' es)
The purpose of ``Path`` is to state whether a program can throw
exceptions, so that we can know where it is safe to reference linear
resources. It is declared as follows:
.. code-block:: idris
data Path = MayThrow | NoThrow
The type of ``App`` states that ``MayThrow`` is the default.
We expect this to be the most
common case. After all, realistically, most operations have possible failure
modes, especially those which interact with the outside world.
The ``0`` on the declaration of ``Has`` indicates that it can only
be run in an erased context, so it will never be run at run-time.
To run an ``App`` inside ``IO``, we use an initial
environment ``Init`` (recall that an ``Environment`` is a
``List Type``):
.. code-block:: idris
Init : Environment
Init = [Void]
run : App {l} Init a -> IO a
Generalising the ``Path`` parameter with ``l``
means that we can invoke ``run`` for any application, whether the ``Path``
is ``NoThrow`` or ``MayThrow``. But, in practice, all applications
given to ``run`` will not throw at the top level, because the only
exception type available is the empty type ``Void``. Any exceptions
will have been introduced and handled inside the ``App``.

253
docs/source/app/linear.rst Normal file
View File

@ -0,0 +1,253 @@
Linear Resources
================
We have introduced ``App`` for writing
interactive programs, using interfaces to constrain which operations are
permitted, but have not yet seen the ``Path`` parameter in action.
Its purpose is to constrain when programs can throw exceptions,
to know where linear resource usage is allowed. The bind operator
for ``App`` is defined as follows (not via ``Monad``):
.. code-block:: idris
data SafeBind : Path -> (l' : Path) -> Type where
SafeSame : SafeBind l l
SafeToThrow : SafeBind NoThrow MayThrow
(>>=) : SafeBind l l' =>
App {l} e a -> (a -> App {l=l'} e b) -> App {l=l'} e b
The intuition behind this type is that, when sequencing two ``App``
programs:
* if the first action might throw an exception, then the whole program might
throw.
* if the first action cannot throw an exception, the second action can still
throw, and the program as a whole can throw.
* if neither action can throw an exception, the program as a whole cannot
throw.
The reason for the detail in the type is that it is useful to be able to
sequence programs with a different ``Path``, but in doing so, we must
calculate the resulting ``Path`` accurately.
Then, if we want to sequence subprograms with linear variables,
we can use an alternative bind operator which guarantees to run the
continuation exactly once:
.. code-block:: idris
bindL : App {l=NoThrow} e a ->
(1 k : a -> App {l} e b) -> App {l} e b
To illustrate the need for ``bindL``, we can try writing a program which
tracks the state of a secure data store, which requires logging in before
reading the data.
Example: a data store requiring a login
---------------------------------------
Many software components rely on some form of state, and there may be
operations which are only valid in specific states. For example, consider
a secure data store in which a user must log in before getting access to
some secret data. This system can be in one of two states:
* ``LoggedIn``, in which the user is allowed to read the secret
* ``LoggedOut``, in which the user has no access to the secret
We can provide commands to log in, log out, and read the data, as illustrated
in the following diagram:
|login|
The ``login`` command, if it succeeds, moves the overall system state from
``LoggedOut`` to ``LoggedIn``. The ``logout`` command moves the state from
``LoggedIn`` to ``LoggedOut``. Most importantly, the ``readSecret`` command
is only valid when the system is in the ``LoggedIn`` state.
We can represent the state transitions using functions with linear types.
To begin, we define an interface for connecting to and disconnecting from
a store:
.. code-block:: idris
interface StoreI e where
connect : (1 prog : (1 d : Store LoggedOut) ->
App {l} e ()) -> App {l} e ()
disconnect : (1 d : Store LoggedOut) -> App {l} e ()
Neither ``connect`` nor ``disconnect`` throw, as shown by
generalising over ``l``. Once we
have a connection, we can use the following functions to
access the resource directly:
.. code-block:: idris
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (val : a) -> (1 resource : r val) -> Res a r
login : (1 s : Store LoggedOut) -> (password : String) ->
Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
logout : (1 s : Store LoggedIn) -> Store LoggedOut
readSecret : (1 s : Store LoggedIn) ->
Res String (const (Store LoggedIn))
``Res`` is defined in ``Control.App`` since it is commonly useful. It is a
dependent pair type, which associates a value with a linear resource.
We'll leave the other definitions abstract, for the purposes of this
introductory example.
The following listing shows a complete program accessing the store, which
reads a password, accesses the store if the password is correct and prints the
secret data. It uses ``let (>>=) = bindL`` to redefine
``do``-notation locally.
.. code-block:: idris
storeProg : Has [Console, StoreI] e => App e ()
storeProg = let (>>=) = bindL in
do putStr "Password: "
password <- getStr
connect $ \s =>
do let True @@ s = login s password
| False @@ s => do putStrLn "Wrong password"
disconnect s
let str @@ s = readSecret s
putStrLn $ "Secret: " ++ show str
let s = logout s
disconnect s
If we omit the ``let (>>=) = bindL``, it will use the default
``(>>=)`` operator, which allows the continuation to be run multiple
times, which would mean that ``s`` is not guaranteed to be accessed
linearly, and ``storeProg`` would not type check.
We can safely use ``getStr`` and ``putStr`` because they
are guaranteed not to throw by the ``Path`` parameter in their types.
.. |login| image:: ../image/login.png
:width: 500px
App1: Linear Interfaces
-----------------------
Adding the ``bindL`` function to allow locally rebinding the
``(>>=)`` operator allows us to combine existing linear resource
programs with operations in ``App`` - at least, those that don't throw.
It would nevertheless be nice to interoperate more directly with ``App``.
One advantage of defining interfaces is that we can provide multiple
implementations for different contexts, but our implementation of the
data store uses primitive functions (which we left undefined in any case)
to access the store.
To allow control over linear resources, ``Control.App`` provides an alternative
parameterised type ``App1``:
.. code-block:: idris
data App1 : {default One u : Usage} ->
(e : Environment) -> Type -> Type
There is no need for a ``Path`` argument, since linear programs can
never throw. The ``Usage`` argument states whether the value
returned is to be used once, or has unrestricted usage, with
the default in ``App1`` being to use once:
.. code-block:: idris
data Usage = One | Any
The main difference from ``App`` is the ``(>>=)`` operator, which
has a different multiplicity for the variable bound by the continuation
depending on the usage of the first action:
.. code-block:: idris
Cont1Type : Usage -> Type -> Usage -> Environment ->
Type -> Type
Cont1Type One a u e b = (1 x : a) -> App1 {u} e b
Cont1Type Any a u e b = (x : a) -> App1 {u} e b
(>>=) : {u : _} -> (1 act : App1 {u} e a) ->
(1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b
``Cont1Type`` returns a continuation which uses the argument linearly,
if the first ``App1`` program has usage ``One``, otherwise it
returns a continuation where argument usage is unrestricted. Either way,
because there may be linear resources in scope, the continuation is
run exactly once and there can be no exceptions thrown.
Using ``App1``, we can define all of the data store operations in a
single interface, as shown in the following listing.
Each operation other than ``disconnect`` returns a `linear` resource.
.. code-block:: idris
interface StoreI e where
connect : App1 e (Store LoggedOut)
login : (1 d : Store LoggedOut) -> (password : String) ->
App1 e (Res Bool (\ok => Store (if ok then LoggedIn
else LoggedOut))
logout : (1 d : Store LoggedIn) -> App1 e (Store LoggedOut)
readSecret : (1 d : Store LoggedIn) ->
App1 e (Res String (const (Store LoggedIn)))
disconnect : (1 d : Store LoggedOut) -> App {l} e ()
We can explicitly move between ``App`` and ``App1``:
.. code-block:: idris
app : (1 p : App {l=NoThrow} e a) -> App1 {u=Any} e a
app1 : (1 p : App1 {u=Any} e a) -> App {l} e a
We can run an ``App`` program using ``app``, inside ``App1``,
provided that it is guaranteed not to throw. Similarly, we can run an
``App1`` program using ``app1``, inside ``App``, provided that
the value it returns has unrestricted usage. So, for example, we can
write:
.. code-block:: idris
storeProg : Has [Console, StoreI] e => App e ()
storeProg = app1 $ do
store <- connect
app $ putStr "Password: "
?what_next
This uses ``app1`` to state that the body of the program is linear,
then ``app`` to state that the ``putStr`` operation is in
``App``. We can see that ``connect`` returns a linear resource
by inspecting the hole ``what_next``, which also shows that we are
running inside ``App1``:
.. code-block:: idris
0 e : List Type
1 store : Store LoggedOut
-------------------------------------
what_next : App1 e ()
For completeness, one way to implement the interface is as follows, with
hard coded password and internal data:
.. code-block:: idris
Has [Console] e => StoreI e where
connect
= do app $ putStrLn "Connect"
pure1 (MkStore "xyzzy")
login (MkStore str) pwd
= if pwd == "Mornington Crescent"
then pure1 (True @@ MkStore str)
else pure1 (False @@ MkStore str)
logout (MkStore str) = pure1 (MkStore str)
readSecret (MkStore str) = pure1 (str @@ MkStore str)
disconnect (MkStore _)
= putStrLn "Door destroyed"
Then we can run it in ``main``:
.. code-block:: idris
main : IO ()
main = run storeProg

BIN
docs/source/image/login.png Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 9.9 KiB