mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-24 12:54:28 +03:00
51 lines
2.1 KiB
ReStructuredText
51 lines
2.1 KiB
ReStructuredText
|
.. _proofs-index:
|
||
|
|
|
||
|
|
################################
|
||
|
|
Structuring Idris 2 Applications
|
||
|
|
################################
|
||
|
|
|
||
|
|
A tutorial on structuring Idris 2 applications using ``Control.App``.
|
||
|
|
|
||
|
|
.. note::
|
||
|
|
|
||
|
|
The documentation for Idris has been published under the Creative
|
||
|
|
Commons CC0 License. As such to the extent possible under law, *The
|
||
|
|
Idris Community* has waived all copyright and related or neighboring
|
||
|
|
rights to Documentation for Idris.
|
||
|
|
|
||
|
|
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||
|
|
|
||
|
|
.. toctree::
|
||
|
|
:maxdepth: 1
|
||
|
|
|
||
|
|
Idris applications have ``main : IO ()`` as an entry point. A type ``IO a`` is
|
||
|
|
a description of interactive actions which produce a value of type ``a``. This
|
||
|
|
is fine for primitives, but ``IO`` does not support exceptions so we have to be
|
||
|
|
explicit about how an operation handles failure. Also, if we do
|
||
|
|
want to support exceptions, we also want to explain how exceptions and linearity
|
||
|
|
(see Section :ref:`sect-multiplicites`) interact.
|
||
|
|
|
||
|
|
In this tutorial, we describe a parameterised type ``App`` and a related
|
||
|
|
parameterised type ``App1``, which together allow us to structure larger
|
||
|
|
applications, taking into account both exceptions and linearity. The aims of
|
||
|
|
``App`` and ``App1`` are that they should:
|
||
|
|
|
||
|
|
* make it possible to express what interactions a function does, in its type,
|
||
|
|
without too much notational overhead.
|
||
|
|
* have little or no performance overhead compared to writing in \texttt{IO}.
|
||
|
|
* be compatible with other libraries and techniques for describing effects,
|
||
|
|
such as algebraic effects or monad transformers.
|
||
|
|
* be sufficiently easy to use and performant that it can be the basis of
|
||
|
|
*all* libraries that make foreign function calls, much as *IO*
|
||
|
|
is in Idris 1 and Haskell
|
||
|
|
* be compatible with linear types, meaning that they should express whether a
|
||
|
|
section of code is linear (guaranteed to execute exactly once without
|
||
|
|
throwing an exception) or whether it might throw an exception.
|
||
|
|
|
||
|
|
We begin by introducing ``App``, with some small example
|
||
|
|
programs, then show how to extend it with exceptions, state, and other
|
||
|
|
interfaces.
|
||
|
|
|
||
|
|
[To be continued...]
|
||
|
|
|