mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-22 14:38:20 +03:00
Heading normalisation, and reST usage fixes.
+ Fixed minor reST inconsistencies. + Normalised syntax used for headers to become inline with the [convention used for Python](http://sphinx.readthedocs.org/en/latest/rest.html#sections)
This commit is contained in:
Jan de Muijnck-Hughes
parent
5c8c1d316c
commit
87039fb0a7
@ -1,8 +1,8 @@
|
||||
.. _sect-further:
|
||||
|
||||
===============
|
||||
***************
|
||||
Further Reading
|
||||
===============
|
||||
***************
|
||||
|
||||
This tutorial has given an introduction to writing and reasoning about
|
||||
side-effecting programs in Idris, using the ``Effects`` library.
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-depeff:
|
||||
|
||||
=================
|
||||
*****************
|
||||
Dependent Effects
|
||||
=================
|
||||
*****************
|
||||
|
||||
In the programs we have seen so far, the available effects have remained
|
||||
constant. Sometimes, however, an operation can *change* the available
|
||||
@ -16,7 +16,7 @@ we will see how this can be used to implement a type-safe and
|
||||
resource-safe protocol for file management.
|
||||
|
||||
Dependent States
|
||||
----------------
|
||||
================
|
||||
|
||||
Suppose we have a function which reads input from the console, converts
|
||||
it to an integer, and adds it to a list which is stored in a ``STATE``.
|
||||
@ -59,7 +59,7 @@ It has the following type:
|
||||
putM : y -> { [STATE x] ==> [STATE y] } Eff ()
|
||||
|
||||
Result-dependent Effects
|
||||
------------------------
|
||||
========================
|
||||
|
||||
Often, whether a state is updated could depend on the success or
|
||||
otherwise of an operation. In our ``readInt`` example, we might wish to
|
||||
@ -134,7 +134,7 @@ check (i.e. whether reading a value succeeded) has indeed been done.
|
||||
being inspected in the type of each branch.
|
||||
|
||||
File Management
|
||||
---------------
|
||||
===============
|
||||
|
||||
A practical use for dependent effects is in specifying resource usage
|
||||
protocols and verifying that they are executed correctly. For example,
|
||||
@ -242,7 +242,7 @@ reading, but the effect list contains a ``FILE_IO`` effect carrying a
|
||||
file open for writing.
|
||||
|
||||
Pattern-matching bind
|
||||
---------------------
|
||||
=====================
|
||||
|
||||
It might seem that having to test each potentially failing operation
|
||||
with a ``case`` clause could lead to ugly code, with lots of
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-hangman:
|
||||
|
||||
=======================================
|
||||
***************************************
|
||||
Example: A “Mystery Word” Guessing Game
|
||||
=======================================
|
||||
***************************************
|
||||
|
||||
In this section, we will use the techniques and specific effects
|
||||
discussed in the tutorial so far to implement a larger example, a simple
|
||||
@ -29,7 +29,7 @@ using the newly defined effect (and any others required to implement the
|
||||
interface).
|
||||
|
||||
Step 1: Game State
|
||||
------------------
|
||||
==================
|
||||
|
||||
First, we categorise the game states as running games (where there are a
|
||||
number of guesses available, and a number of letters still to guess), or
|
||||
@ -53,7 +53,7 @@ this data:
|
||||
data Mystery : GState -> Type
|
||||
|
||||
Step 2: Game Rules
|
||||
------------------
|
||||
==================
|
||||
|
||||
We describe the game rules as a dependent effect, where each action has
|
||||
a *precondition* (i.e. what the game state must be before carrying out
|
||||
@ -131,7 +131,7 @@ then allow us to play the game.
|
||||
MYSTERY h = MkEff (Mystery h) MysteryRules
|
||||
|
||||
Step 3: Implement Rules
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
To *implement* the rules, we begin by giving a concrete definition of
|
||||
game state:
|
||||
@ -211,7 +211,7 @@ such a way that the number of missing letters or number of guesses does
|
||||
not follow the rules.
|
||||
|
||||
Step 4: Implement Interface
|
||||
---------------------------
|
||||
===========================
|
||||
|
||||
Having described the rules, and implemented state transitions which
|
||||
follow those rules as an effect handler, we can now write an interface
|
||||
@ -225,7 +225,7 @@ for the game which uses the ``MYSTERY`` effect:
|
||||
The type indicates that the game must start in a running state, with
|
||||
some guesses available, and eventually reach a not-running state (i.e.
|
||||
won or lost). The only way to achieve this is by correctly following the
|
||||
stated rules.
|
||||
stated rules.
|
||||
|
||||
Note that the type of ``game`` makes no assumption that there are
|
||||
letters to be guessed in the given word (i.e. it is ``w`` rather than
|
||||
@ -267,7 +267,7 @@ generator, then pick a random ``Fin`` to index into a list of
|
||||
limited form of type inference, but very useful in practice.
|
||||
|
||||
A possible complete implementation of ``game`` is
|
||||
presented below:
|
||||
presented below:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -298,7 +298,7 @@ presented below:
|
||||
(S k) => game
|
||||
|
||||
Discussion
|
||||
----------
|
||||
==========
|
||||
|
||||
Writing the rules separately as an effect, then an implementation
|
||||
which uses that effect, ensures that the implementation must follow
|
||||
@ -330,4 +330,4 @@ These are, of course, simple errors, but were caught by the type
|
||||
checker before any testing of the game.
|
||||
|
||||
.. [1]
|
||||
Readers may recognise this game by the name “Hangman.”
|
||||
Readers may recognise this game by the name “Hangman”.
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-impleff:
|
||||
|
||||
====================
|
||||
********************
|
||||
Creating New Effects
|
||||
====================
|
||||
********************
|
||||
|
||||
We have now seen several side-effecting operations provided by the
|
||||
``Effects`` library, and examples of their use in Section
|
||||
@ -14,7 +14,7 @@ selection of the available effects are implemented, and show how new
|
||||
effectful operations may be provided.
|
||||
|
||||
State
|
||||
-----
|
||||
=====
|
||||
|
||||
Effects are described by *algebraic data types*, where the
|
||||
constructors describe the operations provided when the effect is
|
||||
@ -154,7 +154,7 @@ Such details are not important for using the library, or even writing
|
||||
new effects, however.
|
||||
|
||||
Summary
|
||||
~~~~~~~
|
||||
-------
|
||||
|
||||
The following listing summarises what is required to define the
|
||||
``STATE`` effect:
|
||||
@ -183,7 +183,7 @@ The following listing summarises what is required to define the
|
||||
|
||||
|
||||
Console I/O
|
||||
-----------
|
||||
===========
|
||||
|
||||
Then listing below gives the definition of the ``STDIO``
|
||||
effect, including handlers for ``IO`` and ``IOExcept``. We omit the
|
||||
@ -219,7 +219,7 @@ directly.
|
||||
STDIO = MkEff () StdIO
|
||||
|
||||
Exceptions
|
||||
----------
|
||||
==========
|
||||
|
||||
The listing below gives the definition of the ``Exception``
|
||||
effect, including two of its handlers for ``Maybe`` and ``List``. The
|
||||
@ -244,7 +244,7 @@ error.
|
||||
|
||||
|
||||
Non-determinism
|
||||
---------------
|
||||
===============
|
||||
|
||||
The following listing gives the definition of the ``Select``
|
||||
effect for writing non-deterministic programs, including a handler for
|
||||
@ -277,10 +277,10 @@ accumulate all successful results, and in the ``Maybe`` handler we try
|
||||
the first value in the last, and try later values only if that fails.
|
||||
|
||||
File Management
|
||||
---------------
|
||||
===============
|
||||
|
||||
Result-dependent effects are no different from non-dependent effects
|
||||
in the way they are implemented. The listing below
|
||||
in the way they are implemented. The listing below
|
||||
illustrates this for the ``FILE_IO`` effect. The syntax for state
|
||||
transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is
|
||||
computed from the result of the operation ``res``, follows that for
|
||||
@ -320,4 +320,3 @@ continuation ``k`` are different depending on whether the result is
|
||||
``True`` (opening succeeded) or ``False`` (opening failed). This uses
|
||||
``validFile``, defined in the ``Prelude``, to test whether a file
|
||||
handler refers to an open file or not.
|
||||
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
============
|
||||
************
|
||||
Introduction
|
||||
============
|
||||
************
|
||||
|
||||
Pure functional languages with dependent types such as `Idris
|
||||
<http://idris-lang.org/>`_ support reasoning about programs directly
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-simpleff:
|
||||
|
||||
==============
|
||||
**************
|
||||
Simple Effects
|
||||
==============
|
||||
**************
|
||||
|
||||
So far we have seen how to write programs with locally mutable state
|
||||
using the ``STATE`` effect. To recap, we have the definitions below
|
||||
@ -41,7 +41,7 @@ All of the effects in the library, including those described in this
|
||||
section, are summarised in Appendix :ref:`sect-appendix`.
|
||||
|
||||
Console I/O
|
||||
-----------
|
||||
===========
|
||||
|
||||
Console I/O is supported with the ``STDIO``
|
||||
effect, which allows reading and writing characters and strings to and
|
||||
@ -67,7 +67,7 @@ can perform (or at the very least simulate) console I/O:
|
||||
instance Handler StdIO (IOExcept a)
|
||||
|
||||
Examples
|
||||
~~~~~~~~
|
||||
--------
|
||||
|
||||
A program which reads the user’s name, then says hello, can be written
|
||||
as follows:
|
||||
@ -117,7 +117,7 @@ read and write from the console. To run this, ``main`` does not need
|
||||
to be changed.
|
||||
|
||||
Aside: Resource Types
|
||||
~~~~~~~~~~~~~~~~~~~~~
|
||||
---------------------
|
||||
|
||||
To find out the resource type of an effect, if necessary (for example
|
||||
if we want to initialise a resource explicitiy with ``runInit`` rather
|
||||
@ -132,7 +132,7 @@ than using a default value with ``run``) we can run the
|
||||
Int : Type
|
||||
|
||||
Exceptions
|
||||
----------
|
||||
==========
|
||||
|
||||
The ``EXCEPTION``
|
||||
effect is declared in module ``Effect.Exception``. This allows programs
|
||||
@ -155,7 +155,7 @@ generally:
|
||||
instance Show a => Handler (Exception a) IO
|
||||
|
||||
Example
|
||||
~~~~~~~
|
||||
-------
|
||||
|
||||
Suppose we have a ``String`` which is expected to represent an integer
|
||||
in the range ``0`` to ``n``. We can write a function ``parseNumber``
|
||||
@ -232,7 +232,7 @@ the boundedness proof:
|
||||
else raise NotANumber
|
||||
|
||||
Random Numbers
|
||||
--------------
|
||||
==============
|
||||
|
||||
Random number generation is also implemented by the library, in module
|
||||
``Effect.Random``:
|
||||
@ -263,7 +263,7 @@ produce a random number:
|
||||
(essentially a number with an upper bound given in its type).
|
||||
|
||||
Example
|
||||
~~~~~~~
|
||||
-------
|
||||
|
||||
We can use the ``RND`` effect to implement a simple guessing game. The
|
||||
``guess`` function, given a target number, will repeatedly ask the
|
||||
@ -317,7 +317,7 @@ do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.
|
||||
|
||||
|
||||
Non-determinism
|
||||
---------------
|
||||
===============
|
||||
|
||||
The listing below gives the definition of the non-determinism
|
||||
effect, which allows a program to choose a value non-deterministically
|
||||
@ -337,7 +337,7 @@ succeeds:
|
||||
instance Handler Selection List
|
||||
|
||||
Example
|
||||
~~~~~~~
|
||||
-------
|
||||
|
||||
The ``SELECT`` effect can be used to solve constraint problems, such
|
||||
as finding Pythagorean triples. The idea is to use ``select`` to give
|
||||
@ -373,7 +373,7 @@ context). We can try this as follows:
|
||||
print $ the (List _) $ run (triple 100)
|
||||
|
||||
``vadd`` revisited
|
||||
------------------
|
||||
==================
|
||||
|
||||
We now return to the ``vadd`` program from the introduction. Recall the
|
||||
definition:
|
||||
@ -453,7 +453,7 @@ with gracefully.
|
||||
else raise "Not a number"
|
||||
|
||||
Example: An Expression Calculator
|
||||
---------------------------------
|
||||
=================================
|
||||
|
||||
To show how these effects can fit together, let us consider an
|
||||
evaluator for a simple expression language, with addition and integer
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-state:
|
||||
|
||||
=====
|
||||
*****
|
||||
State
|
||||
=====
|
||||
*****
|
||||
|
||||
Many programs, even pure programs, can benefit from locally mutable
|
||||
state. For example, consider a program which tags binary tree nodes
|
||||
@ -34,7 +34,7 @@ specific value ``i``, has the following type:
|
||||
treeTag : (i : Int) -> BTree a -> BTree (Int, a)
|
||||
|
||||
First attempt
|
||||
-------------
|
||||
=============
|
||||
|
||||
Naïvely, we can implement ``treeTag`` by implementing a helper
|
||||
function which propagates a counter, returning the result of the count
|
||||
@ -75,7 +75,7 @@ is local mutable state (the counter) which we have had to make
|
||||
explicit.
|
||||
|
||||
Introducing ``Effects``
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
Idris provides a library, ``Effects`` [3]_, which captures this
|
||||
pattern and many others involving effectful computation [1]_. An
|
||||
@ -217,7 +217,7 @@ shown in Listing [introprog].
|
||||
main = print (treeTag 1 testTree)
|
||||
|
||||
Effects and Resources
|
||||
---------------------
|
||||
=====================
|
||||
|
||||
Each effect is associated with a *resource*, which is initialised
|
||||
before an effectful program can be run. For example, in the case of
|
||||
@ -261,7 +261,7 @@ implemented ``treeTag`` by initialising the state as follows:
|
||||
treeTag i x = runPureInit [i] (treeTagAux x)
|
||||
|
||||
Labelled Effects
|
||||
----------------
|
||||
================
|
||||
|
||||
What if we have more than one state, especially more than one state of
|
||||
the same type? How would ``get`` and ``put`` know which state they
|
||||
@ -358,7 +358,7 @@ effect. Note that labels are polymorphic in the label type ``lbl``.
|
||||
Hence, a label can be anything—a string, an integer, a type, etc.
|
||||
|
||||
``!``-notation
|
||||
--------------
|
||||
==============
|
||||
|
||||
In many cases, using ``do``-notation can make programs unnecessarily
|
||||
verbose, particularly in cases where the value bound is used once,
|
||||
@ -412,7 +412,7 @@ is lifted to:
|
||||
f g'
|
||||
|
||||
Syntactic Sugar and ``Eff``
|
||||
---------------------------
|
||||
===========================
|
||||
|
||||
By now, you may be wondering about the syntax we are using for
|
||||
``Eff``, because it doesn’t look like a normal type! (If not, you may
|
||||
|
||||
@ -1,14 +1,14 @@
|
||||
.. _sect-appendix:
|
||||
|
||||
===============
|
||||
***************
|
||||
Effects Summary
|
||||
===============
|
||||
***************
|
||||
|
||||
This appendix gives interfaces for the core effects provided by the
|
||||
library.
|
||||
|
||||
EXCEPTION
|
||||
---------
|
||||
=========
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -29,7 +29,7 @@ EXCEPTION
|
||||
instance Show a => Handler (Exception a) IO
|
||||
|
||||
FILE\_IO
|
||||
--------
|
||||
========
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -58,7 +58,7 @@ FILE\_IO
|
||||
instance Handler FileIO IO
|
||||
|
||||
RND
|
||||
---
|
||||
===
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -77,7 +77,7 @@ RND
|
||||
instance Handler Random m
|
||||
|
||||
SELECT
|
||||
------
|
||||
======
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -93,7 +93,7 @@ SELECT
|
||||
instance Handler Selection List
|
||||
|
||||
STATE
|
||||
-----
|
||||
=====
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -111,7 +111,7 @@ STATE
|
||||
instance Handler State m
|
||||
|
||||
STDIO
|
||||
-----
|
||||
=====
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -133,7 +133,7 @@ STDIO
|
||||
instance Handler StdIO (IOExcept a)
|
||||
|
||||
SYSTEM
|
||||
------
|
||||
======
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
==========================
|
||||
**************************
|
||||
Frequently Asked Questions
|
||||
==========================
|
||||
**************************
|
||||
|
||||
What are the differences between Agda and Idris?
|
||||
------------------------------------------------
|
||||
================================================
|
||||
|
||||
The main difference is that Idris has been designed from the start to support
|
||||
verified systems programming through easy interoperability with C and high
|
||||
@ -14,7 +14,7 @@ do notation. Idris also supports tactic based theorem proving, and has a
|
||||
lightweight Hugs/GHCI style interface.
|
||||
|
||||
Is Idris production ready?
|
||||
--------------------------
|
||||
==========================
|
||||
|
||||
Idris is primarily a research tool for exploring the possibilities of software
|
||||
development with dependent types, meaning that the primary goal is not (yet) to
|
||||
@ -29,7 +29,7 @@ limited to) extra library support, polishing the run-time system (and ensuring
|
||||
it is robust), providing and maintaining a JVM back end, etc.
|
||||
|
||||
Why does Idris use eager evaluation rather than lazy?
|
||||
-----------------------------------------------------
|
||||
=====================================================
|
||||
|
||||
Idris uses eager evaluation for more predictable performance, in particular
|
||||
because one of the longer term goals is to be able to write efficient and
|
||||
@ -57,7 +57,7 @@ concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an
|
||||
``Int``.
|
||||
|
||||
How can I make lazy control structures?
|
||||
---------------------------------------
|
||||
=======================================
|
||||
|
||||
You can make control structures using the special Lazy type. For example,
|
||||
``if...then...else`` is defined as follows in the library:
|
||||
@ -74,7 +74,7 @@ The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will
|
||||
only be evaluated if they are used, that is, they are evaluated lazily.
|
||||
|
||||
Evaluation at the REPL doesn't behave as I expect. What's going on?
|
||||
-------------------------------------------------------------------
|
||||
===================================================================
|
||||
|
||||
Being a fully dependently typed language, Idris has two phases where it
|
||||
evaluates things, compile-time and run-time. At compile-time it will only
|
||||
@ -100,14 +100,14 @@ the difference between:
|
||||
\n => \m => plus n (S m) : Nat -> Nat -> Nat
|
||||
|
||||
When will Idris be self-hosting?
|
||||
--------------------------------
|
||||
================================
|
||||
|
||||
It’s not a priority, though not a bad idea in the long run. It would be a
|
||||
worthwhile effort in the short term to implement libraries to support
|
||||
self-hosting, such as a good parsing library.
|
||||
|
||||
Does Idris have Universe Polymorphism? What is the type of ``Type``?
|
||||
--------------------------------------------------------------------
|
||||
====================================================================
|
||||
|
||||
Rather than Universe polymorphism, Idris has a cumulative hierarchy of
|
||||
universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
|
||||
@ -115,7 +115,7 @@ Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
|
||||
provided that ``n <= m``.
|
||||
|
||||
Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
|
||||
------------------------------------------------------------------------------------
|
||||
===================================================================================
|
||||
|
||||
Historically the C language and many other languages have used the
|
||||
names ``Float`` and ``Double`` to represent floating point numbers of
|
||||
@ -132,14 +132,14 @@ That is, the names ``Float`` and ``Double`` are used to describe
|
||||
single and double precision numbers.
|
||||
|
||||
What does the name ‘Idris’ mean?
|
||||
--------------------------------
|
||||
================================
|
||||
|
||||
British people of a certain age may be familiar with this
|
||||
`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
|
||||
that doesn’t help, maybe you can invent a suitable acronym :-) .
|
||||
|
||||
Where can I find more answers?
|
||||
------------------------------
|
||||
==============================
|
||||
|
||||
There is an `Unofficial FAQ
|
||||
<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
***********************
|
||||
Type Providers in Idris
|
||||
=======================
|
||||
***********************
|
||||
|
||||
`Type providers in Idris
|
||||
<http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__
|
||||
@ -9,7 +10,7 @@ foreign functions, because these will often be used with type
|
||||
providers.
|
||||
|
||||
The use case
|
||||
------------
|
||||
============
|
||||
|
||||
First, let's talk about *why* we might want type providers. There are
|
||||
a number of reasons to use them and there are other examples available
|
||||
@ -23,7 +24,7 @@ relied upon. We don't just want to hard-code these types into our
|
||||
program... so we'll use a type provider to find them at compile time!
|
||||
|
||||
A simple example
|
||||
----------------
|
||||
================
|
||||
|
||||
First, let's go over a basic usage of type providers, because foreign
|
||||
functions can be confusing but it's important to remember that
|
||||
@ -94,7 +95,7 @@ themselves!
|
||||
Don't worry, there's a better way.
|
||||
|
||||
Foreign Functions
|
||||
-----------------
|
||||
=================
|
||||
|
||||
It's actually pretty easy to write a C function that figures out the
|
||||
size of ``size_t``:
|
||||
@ -114,8 +115,8 @@ So now we can get the size of ``size_t`` as long as we're in C code.
|
||||
We'd like to be able to use this from Idris. Can we do this? It turns
|
||||
out we can.
|
||||
|
||||
mkForeign
|
||||
~~~~~~~~~
|
||||
``mkForeign``
|
||||
-------------
|
||||
|
||||
With mkForeign, we can turn a C function into an IO action. It works
|
||||
like this:
|
||||
@ -138,7 +139,7 @@ compiler "Treat the return value of this C function like it's a C int,
|
||||
and when you pass it back into Idris, convert it to an Idris int."
|
||||
|
||||
Caveats of mkForeign
|
||||
^^^^^^^^^^^^^^^^^^^^
|
||||
--------------------
|
||||
|
||||
First and foremost: ``mkForeign`` is not actually a function. It is
|
||||
treated specially by the compiler, and there are certain rules you
|
||||
@ -185,7 +186,7 @@ applied. This is okay:
|
||||
lengths = mapM strlen listOfStrings
|
||||
|
||||
Running foreign functions
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
-------------------------
|
||||
|
||||
This is all well and good for writing code that will typecheck. To
|
||||
actually run the code, we'll need to do just a bit more work. Exactly
|
||||
@ -193,7 +194,7 @@ what we need to do depends on whether we want to interpret or compile
|
||||
our code.
|
||||
|
||||
In the interpreter
|
||||
^^^^^^^^^^^^^^^^^^
|
||||
------------------
|
||||
|
||||
If we want to call our foreign functions from interpreted code (such
|
||||
as the REPL or a type provider), we need to dynamically link a library
|
||||
@ -213,7 +214,7 @@ functions from an installed library rather than something you wrote
|
||||
yourself, the "./" is not necessary.
|
||||
|
||||
In an executable
|
||||
^^^^^^^^^^^^^^^^
|
||||
----------------
|
||||
|
||||
If we want to run our code from an executable, we can statically link
|
||||
instead. We'll use the ``%include`` and ``%link`` directives:
|
||||
@ -229,7 +230,7 @@ directives search in the current directory by default. (That is, the
|
||||
directory from which we run idris.)
|
||||
|
||||
Putting it all together
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
So, at the beginning of this article I said we'd use type providers to
|
||||
port ``struct stat`` to Idris. The relevant part is just translating
|
||||
|
||||
@ -15,6 +15,7 @@ Documentation for the Idris Language
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
|
||||
* :ref:`tutorial-index`
|
||||
* :ref:`eff-tutorial-index`
|
||||
* :ref:`faq-index`
|
||||
@ -47,7 +48,7 @@ The Idris Tutorial
|
||||
tutorial/miscellany
|
||||
tutorial/conclusions
|
||||
|
||||
.. _effects:
|
||||
.. _faq:
|
||||
|
||||
##########################
|
||||
Frequently Asked Questions
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
****************
|
||||
Inductive Proofs
|
||||
================
|
||||
****************
|
||||
|
||||
Before embarking on proving ``plus_commutes`` in Idris itself, let us
|
||||
consider the overall structure of a proof of some property of natural
|
||||
@ -25,7 +26,7 @@ case). Recalling ``plus``:
|
||||
|
||||
This is total because it covers all possible inputs (the first argument
|
||||
can only be ``Z`` or ``S k`` for some ``k``, and the second argument
|
||||
``m`` covers all possible ``Nat``\ s) and in the recursive call, ``k``
|
||||
``m`` covers all possible ``Nat``) and in the recursive call, ``k``
|
||||
is structurally smaller than ``S k`` so the first argument will always
|
||||
reach the base case ``Z`` in any sequence of recursive calls.
|
||||
|
||||
@ -50,7 +51,7 @@ function capturing all such inductive definitions:
|
||||
.. code-block:: idris
|
||||
|
||||
nat_induction : (P : Nat -> Type) -> -- Property to show
|
||||
(P Z) -> -- Base case
|
||||
(P Z) -> -- Base case
|
||||
((k : Nat) -> P k -> P (S k)) -> -- Inductive step
|
||||
(x : Nat) -> -- Show for all x
|
||||
P x
|
||||
@ -63,12 +64,12 @@ version of ``plus``:
|
||||
.. code-block:: idris
|
||||
|
||||
plus_ind : Nat -> Nat -> Nat
|
||||
plus_ind n m
|
||||
plus_ind n m
|
||||
= nat_induction (\x => Nat)
|
||||
m -- Base case, plus_ind Z m
|
||||
(\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
|
||||
-- where k_rec = plus_ind k m
|
||||
n
|
||||
n
|
||||
|
||||
To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and
|
||||
``m``, we can also use induction. Either we can fix ``m`` and perform
|
||||
|
||||
@ -1,13 +1,14 @@
|
||||
***************************
|
||||
Interactive Theorem Proving
|
||||
===========================
|
||||
***************************
|
||||
|
||||
Idris also supports interactive theorem proving via tactics. This
|
||||
is generally not recommended to be used directly, but rather used as a
|
||||
is generally not recommended to be used directly, but rather used as a
|
||||
mechanism for building proof automation which is beyond the scope of this
|
||||
tutorial. In this section, we briefly discus tactics.
|
||||
|
||||
One way to write proofs interactively is to write the general *structure* of
|
||||
the proof, and use the interactive mode to complete the details.
|
||||
the proof, and use the interactive mode to complete the details.
|
||||
Consider the following definition, proved in :ref:`sect-theorems`:
|
||||
|
||||
.. code-block:: idris
|
||||
@ -162,5 +163,3 @@ which is trivially provable:
|
||||
|
||||
Again, we can add this proof to the end of our source file using the
|
||||
``:addproof`` command at the interactive prompt.
|
||||
|
||||
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
***********************
|
||||
Pattern Matching Proofs
|
||||
=======================
|
||||
***********************
|
||||
|
||||
In this section, we will provide a proof of ``plus_commutes`` directly,
|
||||
by writing a pattern matching definition. We will use interactive
|
||||
@ -26,7 +27,7 @@ mapping to Emacs commands.
|
||||
|
||||
|
||||
Creating a Definition
|
||||
---------------------
|
||||
=====================
|
||||
|
||||
To begin, create a file ``pluscomm.idr`` containing the following type
|
||||
declaration:
|
||||
@ -87,7 +88,7 @@ It is a good idea to give these slightly more meaningful names:
|
||||
plus_commutes (S k) m = ?plus_commutes_S
|
||||
|
||||
Base Case
|
||||
---------
|
||||
=========
|
||||
|
||||
We can create a separate lemma for the base case interactively, by
|
||||
pressing ``\l`` with the cursor over ``plus_commutes_Z``. This
|
||||
@ -263,7 +264,7 @@ proof, giving:
|
||||
The base case is now complete.
|
||||
|
||||
Inductive Step
|
||||
--------------
|
||||
==============
|
||||
|
||||
Our main theorem, ``plus_commutes`` should currently be in the following
|
||||
state:
|
||||
@ -333,9 +334,9 @@ defined by matching on its first argument. The complete definition is:
|
||||
plus_commutes_S k Z = Refl
|
||||
plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
|
||||
|
||||
All metavariables have now been solved,
|
||||
All metavariables have now been solved,
|
||||
|
||||
The ``total`` annotation means that we require the final function to
|
||||
The ``total`` annotation means that we require the final function to
|
||||
pass the totality checker; i.e. it will terminate on all possible
|
||||
well-typed inputs. This is important for proofs, since it provides a
|
||||
guarantee that the proof is valid in *all* cases, not just those for
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
********************************************
|
||||
Running example: Addition of Natural Numbers
|
||||
============================================
|
||||
********************************************
|
||||
|
||||
Throughout this tutorial, we will be working with the following
|
||||
function, defined in the Idris prelude, which defines addition on
|
||||
@ -44,7 +45,7 @@ We can use these properties in an Idris program, but in order to do so
|
||||
we must *prove* them.
|
||||
|
||||
Equality Proofs
|
||||
---------------
|
||||
===============
|
||||
|
||||
Idris has a built-in propositional equality type, conceptually defined
|
||||
as follows:
|
||||
@ -93,7 +94,7 @@ error:
|
||||
4 = 5 (Expected type)
|
||||
|
||||
Type checking equality proofs
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
-----------------------------
|
||||
|
||||
An important step in type checking Idris programs is *unification*,
|
||||
which attempts to resolve implicit arguments such as the implicit
|
||||
@ -123,7 +124,7 @@ following equalities directly:
|
||||
plus_reduces_Sk k m = Refl
|
||||
|
||||
Heterogeneous Equality
|
||||
----------------------
|
||||
======================
|
||||
|
||||
Equality in Idris is *heterogeneous*, meaning that we can even propose
|
||||
equalities between values in different types:
|
||||
@ -164,7 +165,7 @@ there is only one value which will type check:
|
||||
vect_eq_length xs _ Refl = Refl
|
||||
|
||||
Properties of ``plus``
|
||||
----------------------
|
||||
======================
|
||||
|
||||
Using the ``(=)`` type, we can now state the properties of ``plus``
|
||||
given above as Idris type declarations:
|
||||
@ -185,4 +186,4 @@ the function.) We will also discuss how to use such equality proofs, and
|
||||
see where the need for them arises in practice.
|
||||
|
||||
.. [1]
|
||||
This is known as the Curry-Howard correspondence
|
||||
This is known as the Curry-Howard correspondence.
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-documenting:
|
||||
|
||||
======================
|
||||
**********************
|
||||
Documenting Idris Code
|
||||
======================
|
||||
**********************
|
||||
|
||||
Idris documentation comes in two major forms: comments, which exist
|
||||
for a reader’s edification and are ignored by the compiler, and inline
|
||||
@ -12,7 +12,7 @@ reference. To consult the documentation for a declaration ``f``, write
|
||||
(``C-c C-d`` in Emacs, in Vim).
|
||||
|
||||
Comments
|
||||
--------
|
||||
========
|
||||
|
||||
Use comments to explain why code is written the way that it
|
||||
is. Idris’s comment syntax is the same as that of Haskell: lines
|
||||
@ -22,7 +22,7 @@ lines. These can be used to comment out lines of code or provide
|
||||
simple documentation for the readers of Idris code.
|
||||
|
||||
Inline Documentation
|
||||
--------------------
|
||||
====================
|
||||
|
||||
Idris also supports a comprehensive and rich inline syntax for Idris
|
||||
code to be generated. This syntax also allows for named parameters and
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
*************************
|
||||
Erasure By Usage Analysis
|
||||
=========================
|
||||
*************************
|
||||
|
||||
This work stems from this `feature proposal
|
||||
<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__
|
||||
@ -8,7 +9,7 @@ is out of date — and sometimes even in direct contradiction with the
|
||||
eventual implementation.
|
||||
|
||||
Motivation
|
||||
----------
|
||||
==========
|
||||
|
||||
Traditional dependently typed languages (Agda, Coq) are good at
|
||||
erasing *proofs* (either via irrelevance or an extra universe).
|
||||
@ -52,7 +53,7 @@ The following two sections describe two cases where doing so improves
|
||||
the runtime performance asymptotically.
|
||||
|
||||
Binary numbers
|
||||
~~~~~~~~~~~~~~
|
||||
--------------
|
||||
|
||||
- O(n) instead of O(log n)
|
||||
|
||||
@ -106,7 +107,7 @@ should get rid of them and get runtime code similar to what a idris
|
||||
programmer would write.
|
||||
|
||||
U-views of lists
|
||||
~~~~~~~~~~~~~~~~
|
||||
----------------
|
||||
|
||||
- O(n^2) instead of O(n)
|
||||
|
||||
@ -141,7 +142,7 @@ linear time — so we need to erase the index ``xs`` if we want to
|
||||
achieve this goal.
|
||||
|
||||
Changes to Idris
|
||||
----------------
|
||||
================
|
||||
|
||||
Usage analysis is run at every compilation and its outputs are used
|
||||
for various purposes. This is actually invisible to the user but it's
|
||||
@ -185,7 +186,7 @@ Postulates are no longer required to be collapsible. They are now
|
||||
required to be *unused* instead.
|
||||
|
||||
Changes to the language
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
You can use dots to mark fields that are not intended to be used at
|
||||
runtime.
|
||||
@ -221,7 +222,7 @@ You can also put dots in types of functions to get more guarantees.
|
||||
and free implicits are automatically dotted here, too.
|
||||
|
||||
What it means
|
||||
-------------
|
||||
=============
|
||||
|
||||
Dot annotations serve two purposes:
|
||||
|
||||
@ -235,7 +236,7 @@ are there mainly to help the programmer (and the compiler) refrain
|
||||
from using the values they want to erase.
|
||||
|
||||
How to use it
|
||||
-------------
|
||||
=============
|
||||
|
||||
Ideally, few or no extra annotations are needed -- in practice, it
|
||||
turns out that having free implicits automatically dotted is enough to
|
||||
@ -250,7 +251,7 @@ compiles to a reasonable binary. Generally, it's sufficient to follow
|
||||
erasure warnings (which may be sometimes unhelpful at the moment).
|
||||
|
||||
Benchmarks
|
||||
----------
|
||||
==========
|
||||
|
||||
- source: https://github.com/ziman/idris-benchmarks
|
||||
- results: http://ziman.functor.sk/erasure-bm/
|
||||
@ -258,7 +259,7 @@ Benchmarks
|
||||
It can be clearly seen that asymptotics are improved by erasure.
|
||||
|
||||
Shortcomings
|
||||
------------
|
||||
============
|
||||
|
||||
You can't get warnings in libraries because usage analysis starts from
|
||||
``Main.main``. This will be solved by the planned ``%default_usage``
|
||||
@ -300,7 +301,7 @@ only if it is unused in every implementation of the method that occurs
|
||||
in the program.
|
||||
|
||||
Planned features
|
||||
----------------
|
||||
================
|
||||
|
||||
- Fixes to the above shortcomings in general.
|
||||
|
||||
@ -316,10 +317,10 @@ Planned features
|
||||
in compiled programs.
|
||||
|
||||
Troubleshooting
|
||||
---------------
|
||||
===============
|
||||
|
||||
My program is slower
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
--------------------
|
||||
|
||||
The patch introducing erasure by usage analysis also disabled some
|
||||
optimisations that were in place before; these are subsumed by the new
|
||||
@ -336,14 +337,14 @@ getting compiled into the binary.
|
||||
The solution is to change the code so that there are no warnings.
|
||||
|
||||
Usage warnings are unhelpful
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
----------------------------
|
||||
|
||||
This is a known issue and we are working on it. For now, see the section
|
||||
`How to read and resolve erasure
|
||||
warnings <#how-to-read-and-resolve-erasure-warnings>`__.
|
||||
|
||||
There should be no warnings in this function
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
--------------------------------------------
|
||||
|
||||
A possible cause is non-totality of the function (more precisely,
|
||||
non-coverage). If a function is non-covering, the program needs to
|
||||
@ -361,7 +362,7 @@ https://gist.github.com/ziman/10458331). You can either rephrase the
|
||||
function or wait until this is fixed, hopefully soon. Fixed.
|
||||
|
||||
The compiler refuses to recognise this thing as erased
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
------------------------------------------------------
|
||||
|
||||
You can force anything to be erased by wrapping it in the ``Erased``
|
||||
monad. While this program triggers usage warnings,
|
||||
@ -379,10 +380,10 @@ the following program does not:
|
||||
f g x = g (Erase x) -- OK
|
||||
|
||||
How to read and resolve erasure warnings
|
||||
----------------------------------------
|
||||
========================================
|
||||
|
||||
Example 1
|
||||
~~~~~~~~~
|
||||
---------
|
||||
|
||||
Consider the following program:
|
||||
|
||||
@ -439,7 +440,7 @@ or fixing ``vlen`` to not use the index:
|
||||
Which solution is appropriate depends on the usecase.
|
||||
|
||||
Example 2
|
||||
~~~~~~~~~
|
||||
---------
|
||||
|
||||
Consider the following program manipulating value-indexed binary
|
||||
numbers.
|
||||
@ -494,7 +495,7 @@ with every constructor of ``Bin`` and make it a bound implicit:
|
||||
I : {n : Nat} -> bin n -> Bin (1 + n + n)
|
||||
|
||||
References
|
||||
----------
|
||||
==========
|
||||
|
||||
.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive
|
||||
families need not store their indices
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
******************************
|
||||
New Foreign Function Interface
|
||||
==============================
|
||||
******************************
|
||||
|
||||
.. sectionauthor:: Edwin Brady
|
||||
|
||||
@ -19,7 +20,7 @@ are some things you will need to be aware of, which this page
|
||||
describes.
|
||||
|
||||
The ``IO'`` monad, and ``main``
|
||||
-------------------------------
|
||||
===============================
|
||||
|
||||
The ``IO`` monad exists as before, but is now specific to the C
|
||||
backend (or, more precisely, any backend whose foreign function calls
|
||||
@ -61,7 +62,7 @@ function's name, but potentially something more complicated such as an
|
||||
external library file or even a URL).
|
||||
|
||||
FFI descriptors
|
||||
---------------
|
||||
===============
|
||||
|
||||
An FFI descriptor is a record containing a predicate which holds when
|
||||
a type can be marshalled, and the type of the target of a foreign
|
||||
@ -98,7 +99,7 @@ For C, this is:
|
||||
String -- the name of the C function
|
||||
|
||||
Foreign calls
|
||||
-------------
|
||||
=============
|
||||
|
||||
To call a foreign function, the ``foreign`` function is used. For
|
||||
example:
|
||||
@ -134,7 +135,7 @@ example a shorthand for calling external JavaScript functions:
|
||||
jscall fname ty = foreign FFI_JS fname ty
|
||||
|
||||
FFI implementation
|
||||
~~~~~~~~~~~~~~~~~~
|
||||
------------------
|
||||
|
||||
In order to write bindings to external libraries, the details of how
|
||||
``foreign`` works are unnecessary --- you simply need to know that
|
||||
@ -172,7 +173,7 @@ builds the following implicit proof as the ``fty`` argument to
|
||||
FFun C_Str (FFun C_Str (FRet C_Ptr))
|
||||
|
||||
Compiling foreign calls
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
(This section assumes some knowledge of the Idris internals.)
|
||||
|
||||
@ -232,7 +233,7 @@ to marshal the arguments and return value appropriately.
|
||||
the function ``toFType``, to see how this works in practice.
|
||||
|
||||
JavaScript FFI descriptor
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
=========================
|
||||
|
||||
The JavaScript FFI descriptor is a little more complex, because the
|
||||
JavaScript FFI supports marshalling functions. It is defined as
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
****************
|
||||
Uniqueness Types
|
||||
================
|
||||
****************
|
||||
|
||||
Uniqueness Types are an experimental feature available from Idris
|
||||
0.9.15. A value with a unique type is guaranteed to have *at most one*
|
||||
@ -25,7 +26,7 @@ include:
|
||||
allocate
|
||||
|
||||
Using Uniqueness
|
||||
~~~~~~~~~~~~~~~~
|
||||
================
|
||||
|
||||
If ``x : T`` and ``T : UniqueType``, then there is at most one reference
|
||||
to ``x`` at any time during run-time execution. For example, we can
|
||||
@ -129,7 +130,7 @@ such a function may be passed a ``UniqueType``, any value of type
|
||||
once on the right hand side.
|
||||
|
||||
Borrowed Types
|
||||
~~~~~~~~~~~~~~
|
||||
--------------
|
||||
|
||||
It quickly becomes obvious when working with uniqueness types that
|
||||
having only one reference at a time can be painful. For example, what
|
||||
@ -227,7 +228,7 @@ therefore write ``showU`` as follows:
|
||||
showU' (x :: xs) = show x ++ ", " ++ showU' xs
|
||||
|
||||
Problems/Disadvantages/Still to do...
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
-------------------------------------
|
||||
|
||||
This is a work in progress, there is lots to do. The most obvious
|
||||
problem is the loss of abstraction. On the one hand, we have more
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-classes:
|
||||
|
||||
============
|
||||
************
|
||||
Type Classes
|
||||
============
|
||||
************
|
||||
|
||||
We often want to define functions which work across several different
|
||||
data types. For example, we would like arithmetic operators to work on
|
||||
@ -65,7 +65,7 @@ going to use it to convert each element to a ``String``:
|
||||
show' (x :: xs) = show x ++ ", " ++ show' xs
|
||||
|
||||
Default Definitions
|
||||
-------------------
|
||||
===================
|
||||
|
||||
The library defines an ``Eq`` class which provides an interface for
|
||||
comparing values for equality or inequality, with instances for all of
|
||||
@ -110,7 +110,7 @@ definition is missing, and there is a default definition for it, then
|
||||
the default is used instead.
|
||||
|
||||
Extending Classes
|
||||
-----------------
|
||||
=================
|
||||
|
||||
Classes can also be extended. A logical next step from an equality
|
||||
relation ``Eq`` is to define an ordering relation ``Ord``. We can
|
||||
@ -155,7 +155,7 @@ separated list, for example:
|
||||
sortAndShow xs = show (sort xs)
|
||||
|
||||
Functors and Applicatives
|
||||
-------------------------
|
||||
=========================
|
||||
|
||||
So far, we have seen single parameter type classes, where the parameter
|
||||
is of type ``Type``. In general, there can be any number (greater than
|
||||
@ -195,7 +195,7 @@ abstracts the notion of function application:
|
||||
(<*>) : f (a -> b) -> f a -> f b
|
||||
|
||||
Monads and ``do``-notation
|
||||
--------------------------
|
||||
==========================
|
||||
|
||||
The ``Monad`` class allows us to encapsulate binding and computation,
|
||||
and is the basis of ``do``-notation introduced in Section
|
||||
@ -248,7 +248,7 @@ are available, or return ``Nothing`` if they are not. Managing the
|
||||
Nothing : Maybe Int
|
||||
|
||||
``!``-notation
|
||||
~~~~~~~~~~~~~~
|
||||
--------------
|
||||
|
||||
In many cases, using ``do``-notation can make programs unnecessarily
|
||||
verbose, particularly in cases such as ``m_add`` above where the value
|
||||
@ -292,7 +292,7 @@ is lifted to:
|
||||
f g'
|
||||
|
||||
Monad comprehensions
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
--------------------
|
||||
|
||||
The list comprehension notation we saw in Section
|
||||
:ref:`sect-more-expr` is more general, and applies to anything which
|
||||
@ -336,7 +336,7 @@ would be:
|
||||
m_add x y = [ x' + y' | x' <- x, y' <- y ]
|
||||
|
||||
Idiom brackets
|
||||
--------------
|
||||
==============
|
||||
|
||||
While ``do`` notation gives an alternative meaning to sequencing,
|
||||
idioms give an alternative meaning to *application*. The notation and
|
||||
@ -386,7 +386,7 @@ application ``[| f a1 …an |]`` is translated into ``pure f <> a1 <>
|
||||
m_add' x y = [| x + y |]
|
||||
|
||||
An error-handling interpreter
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
-----------------------------
|
||||
|
||||
Idiom notation is commonly useful when defining evaluators. McBride
|
||||
and Paterson describe such an evaluator [1]_, for a language similar
|
||||
@ -455,7 +455,7 @@ to handle errors:
|
||||
MkEval envFn => envFn env
|
||||
|
||||
Named Instances
|
||||
---------------
|
||||
===============
|
||||
|
||||
It can be desirable to have multiple instances of a type class, for
|
||||
example to provide alternative methods for sorting or printing values.
|
||||
@ -492,7 +492,7 @@ instance ``myord`` as follows, at the Idris prompt:
|
||||
|
||||
|
||||
Determining Parameters
|
||||
----------------------
|
||||
======================
|
||||
|
||||
When a class has more than one parameter, it can help resolution if
|
||||
the parameters used to resolve the type class are restricted. For
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-concs:
|
||||
|
||||
===============
|
||||
***************
|
||||
Further Reading
|
||||
===============
|
||||
***************
|
||||
|
||||
Further information about Idris programming, and programming with
|
||||
dependent types in general, can be obtained from various sources:
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _tutorial-index:
|
||||
|
||||
####################
|
||||
The Idris Tutorial
|
||||
####################
|
||||
##################
|
||||
The Idris Tutorial
|
||||
##################
|
||||
|
||||
The is the Idris Tutorial. It will teach you about programming in the Idris Language.
|
||||
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-interactive:
|
||||
|
||||
===================
|
||||
*******************
|
||||
Interactive Editing
|
||||
===================
|
||||
*******************
|
||||
|
||||
By now, we have seen several examples of how Idris’ dependent type
|
||||
system can give extra confidence in a function’s correctness by giving
|
||||
@ -25,7 +25,7 @@ available.
|
||||
|
||||
|
||||
Editing at the REPL
|
||||
-------------------
|
||||
===================
|
||||
|
||||
The REPL provides a number of commands, which we will describe
|
||||
shortly, which generate new program fragments based on the currently
|
||||
@ -59,10 +59,10 @@ A text editor can take advantage of this, along with the editing
|
||||
commands, in order to provide interactive editing support.
|
||||
|
||||
Editing Commands
|
||||
----------------
|
||||
================
|
||||
|
||||
:addclause
|
||||
~~~~~~~~~~
|
||||
----------
|
||||
|
||||
The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a
|
||||
template definition for the function named ``f`` declared on line
|
||||
@ -91,7 +91,7 @@ This declares that any names generated for types in the ``Vect`` family
|
||||
should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.
|
||||
|
||||
:casesplit
|
||||
~~~~~~~~~~
|
||||
----------
|
||||
|
||||
The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the
|
||||
pattern variable ``x`` on line ``n`` into the various pattern forms it
|
||||
@ -125,7 +125,7 @@ That is, the pattern variable ``ys`` has been split into one case
|
||||
ys`` would lead to a unification error.
|
||||
|
||||
:addmissing
|
||||
~~~~~~~~~~~
|
||||
-----------
|
||||
|
||||
The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the
|
||||
clauses which are required to make the function ``f`` on line ``n``
|
||||
@ -148,7 +148,7 @@ generates the required clauses, and eliminates the clauses which would
|
||||
lead to unification errors.
|
||||
|
||||
:proofsearch
|
||||
~~~~~~~~~~~~
|
||||
------------
|
||||
|
||||
The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to
|
||||
find a value for the metavariable ``f`` on line ``n`` by proof search,
|
||||
@ -186,7 +186,7 @@ must have type ``c`` and the only way to get this is to apply ``f`` to
|
||||
recursively.
|
||||
|
||||
:makewith
|
||||
~~~~~~~~~
|
||||
---------
|
||||
|
||||
The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a
|
||||
``with`` to a pattern clause. For example, recall ``parity``. If line
|
||||
@ -219,7 +219,7 @@ dependent pattern matching by showing a programmer exactly what the
|
||||
valid patterns are.
|
||||
|
||||
Interactive Editing in Vim
|
||||
--------------------------
|
||||
==========================
|
||||
|
||||
The editor mode for Vim provides syntax highlighting, indentation and
|
||||
interactive editing support using the commands described above.
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-interp:
|
||||
|
||||
===================================
|
||||
***********************************
|
||||
Example: The Well-Typed Interpreter
|
||||
===================================
|
||||
***********************************
|
||||
|
||||
In this section, we’ll use the features we’ve seen so far to write a
|
||||
larger example, an interpreter for a simple functional programming
|
||||
@ -12,7 +12,7 @@ system to ensure that any programs which can be represented are
|
||||
well-typed.
|
||||
|
||||
Representing Languages
|
||||
----------------------
|
||||
======================
|
||||
|
||||
First, let us define the types in the language. We have integers,
|
||||
booleans, and functions, represented by ``Ty``:
|
||||
@ -140,7 +140,7 @@ that only the branch which is taken need be evaluated:
|
||||
Expr G a
|
||||
|
||||
Writing the Interpreter
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
When we evaluate an ``Expr``, we’ll need to know the values in scope,
|
||||
as well as their types. ``Env`` is an environment, indexed over the
|
||||
@ -225,7 +225,7 @@ its operands directly, and for ``If``, we apply the Idris
|
||||
else interp env e
|
||||
|
||||
Testing
|
||||
-------
|
||||
=======
|
||||
|
||||
We can make some simple test functions. Firstly, adding two inputs
|
||||
``\x. \y. y + x`` is written as follows:
|
||||
@ -248,7 +248,7 @@ can be written as:
|
||||
(Var Stop)))
|
||||
|
||||
Running
|
||||
-------
|
||||
=======
|
||||
|
||||
To finish, we write a ``main`` program which interprets the factorial
|
||||
function on user input:
|
||||
@ -271,7 +271,7 @@ program at the Idris interactive environment is:
|
||||
|
||||
|
||||
Aside: ``cast``
|
||||
~~~~~~~~~~~~~~~
|
||||
---------------
|
||||
|
||||
The prelude defines a type class ``Cast`` which allows conversion
|
||||
between types:
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-intro:
|
||||
|
||||
============
|
||||
************
|
||||
Introduction
|
||||
============
|
||||
************
|
||||
|
||||
In conventional programming languages, there is a clear distinction
|
||||
between *types* and *values*. For example, in `Haskell
|
||||
@ -44,7 +44,7 @@ a lightweight foreign function interface which allows easy interaction
|
||||
with external ``C`` libraries.
|
||||
|
||||
Intended Audience
|
||||
-----------------
|
||||
=================
|
||||
|
||||
This tutorial is intended as a brief introduction to the language, and
|
||||
is aimed at readers already familiar with a functional language such
|
||||
@ -55,7 +55,7 @@ briefly. The reader is also assumed to have some interest in using
|
||||
dependent types for writing and verifying systems software.
|
||||
|
||||
Example Code
|
||||
------------
|
||||
============
|
||||
|
||||
This tutorial includes some example code, which has been tested with
|
||||
Idris version . The files are available in the Idris
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-misc:
|
||||
|
||||
==========
|
||||
**********
|
||||
Miscellany
|
||||
==========
|
||||
**********
|
||||
|
||||
In this section we discuss a variety of additional features:
|
||||
|
||||
@ -15,7 +15,7 @@ In this section we discuss a variety of additional features:
|
||||
+ the universe hierarchy.
|
||||
|
||||
Auto implicit arguments
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
We have already seen implicit arguments, which allows arguments to be
|
||||
omitted when they can be inferred by the type checker, e.g.
|
||||
@ -70,7 +70,7 @@ to:
|
||||
head (x :: xs) = x
|
||||
|
||||
Implicit conversions
|
||||
--------------------
|
||||
====================
|
||||
|
||||
Idris supports the creation of *implicit conversions*, which allow
|
||||
automatic conversion of values from one type to another when required to
|
||||
@ -99,7 +99,7 @@ specific language, or to hide details of a proof. Such examples are
|
||||
beyond the scope of this tutorial.
|
||||
|
||||
Literate programming
|
||||
--------------------
|
||||
====================
|
||||
|
||||
Like Haskell, Idris supports *literate* programming. If a file has
|
||||
an extension of ``.lidr`` then it is assumed to be a literate file. In
|
||||
@ -120,7 +120,7 @@ program line (beginning with ``>``) and a comment line (beginning with
|
||||
any other character).
|
||||
|
||||
Foreign function calls
|
||||
----------------------
|
||||
======================
|
||||
|
||||
For practical programming, it is often necessary to be able to use
|
||||
external libraries, particularly for interfacing with the operating
|
||||
@ -191,7 +191,7 @@ function is implemented as follows, as a call to an external function
|
||||
putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
|
||||
|
||||
Include and linker directives
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
-----------------------------
|
||||
|
||||
Foreign function calls are translated directly to calls to C functions,
|
||||
with appropriate conversion between the Idris representation of a
|
||||
@ -215,7 +215,7 @@ through the following directives:
|
||||
object ``x.so``.
|
||||
|
||||
Testing foreign function calls
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
------------------------------
|
||||
|
||||
Normally, the Idris interpreter (used for typechecking and at the REPL)
|
||||
will not perform IO actions. Additionally, as it neither generates C
|
||||
@ -232,7 +232,7 @@ command or the ``%dynamic`` directive. For example:
|
||||
0.9995736030415051 : Float
|
||||
|
||||
Type Providers
|
||||
--------------
|
||||
==============
|
||||
|
||||
Idris type providers, inspired by F#’s type providers, are a means of
|
||||
making our types be “about” something in the world outside of Idris. For
|
||||
@ -301,7 +301,7 @@ provider implementations, including a statically-checked SQLite binding,
|
||||
are available in an external collection [1]_.
|
||||
|
||||
C Target
|
||||
--------
|
||||
========
|
||||
|
||||
The default target of Idris is C. Compiling via :
|
||||
|
||||
@ -341,14 +341,14 @@ is shown below :
|
||||
putStrLn $ show $ factorial 3
|
||||
|
||||
JavaScript Target
|
||||
-----------------
|
||||
=================
|
||||
|
||||
Idris is capable of producing *JavaScript* code that can be run in a
|
||||
browser as well as in the *NodeJS* environment or alike. One can use the
|
||||
FFI to communicate with the *JavaScript* ecosystem.
|
||||
|
||||
Code Generation
|
||||
~~~~~~~~~~~~~~~
|
||||
---------------
|
||||
|
||||
Code generation is split into two separate targets. To generate code
|
||||
that is tailored for running in the browser issue the following command:
|
||||
@ -375,7 +375,7 @@ automatically add a newline to the end of each string. This behaviour
|
||||
does not show up in the *NodeJS* code generator.
|
||||
|
||||
Using the FFI
|
||||
~~~~~~~~~~~~~
|
||||
-------------
|
||||
|
||||
To write a useful application we need to communicate with the outside
|
||||
world. Maybe we want to manipulate the DOM or send an Ajax request. For
|
||||
@ -441,7 +441,7 @@ program:
|
||||
The program outputs ``3``, just like we expected.
|
||||
|
||||
Including external *JavaScript* files
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
-------------------------------------
|
||||
|
||||
Whenever one is working with *JavaScript* one might want to include
|
||||
external libraries or just some functions that she or he wants to call
|
||||
@ -470,7 +470,7 @@ And for use in the browser:
|
||||
The given files will be added to the top of the generated code.
|
||||
|
||||
Including *NodeJS* modules
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
--------------------------
|
||||
|
||||
The *NodeJS* code generator can also include modules with the ``%lib``
|
||||
directive.
|
||||
@ -486,7 +486,7 @@ This directive compiles into the following *JavaScript*
|
||||
var fs = require("fs");
|
||||
|
||||
Shrinking down generated *JavaScript*
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
-------------------------------------
|
||||
|
||||
Idris can produce very big chunks of *JavaScript* code. However, the
|
||||
generated code can be minified using the ``closure-compiler`` from
|
||||
@ -497,7 +497,7 @@ and it’s highly recommended to use it when shipping a *JavaScript*
|
||||
application written in Idris.
|
||||
|
||||
Cumulativity
|
||||
------------
|
||||
============
|
||||
|
||||
Since values can appear in types and *vice versa*, it is natural that
|
||||
types themselves have types. For example:
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-namespaces:
|
||||
|
||||
=======================
|
||||
**********************
|
||||
Modules and Namespaces
|
||||
=======================
|
||||
**********************
|
||||
|
||||
An Idris program consists of a collection of modules. Each module
|
||||
includes an optional ``module`` declaration giving the name of the
|
||||
@ -72,7 +72,7 @@ main module, with the ``main`` function, must be called
|
||||
``Main``—although its filename need not be ``Main.idr``.
|
||||
|
||||
Export Modifiers
|
||||
----------------
|
||||
================
|
||||
|
||||
By default, all names defined in a module are exported for use by other
|
||||
modules. However, it is good practice only to export a minimal interface
|
||||
@ -146,7 +146,7 @@ abstract names in module ``C``, but will not re-export anything from
|
||||
module ``B``.
|
||||
|
||||
Explicit Namespaces
|
||||
-------------------
|
||||
===================
|
||||
|
||||
Defining a module also defines a namespace implicitly. However,
|
||||
namespaces can also be given *explicitly*. This is most useful if you
|
||||
@ -176,7 +176,7 @@ disambiguated by their types:
|
||||
"foofoo" : String
|
||||
|
||||
Parameterised blocks
|
||||
--------------------
|
||||
====================
|
||||
|
||||
Groups of functions can be parameterised over a number of arguments
|
||||
using a ``parameters`` declaration, for example:
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-packages:
|
||||
|
||||
========
|
||||
********
|
||||
Packages
|
||||
========
|
||||
********
|
||||
|
||||
Idris includes a simple system for building packages from a
|
||||
package description file. These files can be used with the Idris
|
||||
@ -10,7 +10,7 @@ compiler to manage the development process of your Idris
|
||||
programmes and packages.
|
||||
|
||||
Package Descriptions
|
||||
--------------------
|
||||
====================
|
||||
|
||||
A package description includes the following:
|
||||
|
||||
@ -58,7 +58,7 @@ external ``C`` libraries, the following options are available:
|
||||
object files to be installed, perhaps generated by the ``Makefile``.
|
||||
|
||||
Using Package files
|
||||
-------------------
|
||||
===================
|
||||
|
||||
Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:
|
||||
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
.. _sect-provisional:
|
||||
|
||||
=======================
|
||||
***********************
|
||||
Provisional Definitions
|
||||
=======================
|
||||
***********************
|
||||
|
||||
Sometimes when programming with dependent types, the type required by
|
||||
the type checker and the type of the program we have written will be
|
||||
@ -54,7 +54,7 @@ reduction. These values are obviously equal — how can we rewrite the
|
||||
program to fix this problem?
|
||||
|
||||
Provisional definitions
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
*Provisional definitions* help with this problem by allowing us to defer
|
||||
the proof details until a later point. There are two main reasons why
|
||||
@ -159,7 +159,7 @@ reversed:
|
||||
"[False, True, False, True, False, True]" : String
|
||||
|
||||
Suspension of Disbelief
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
Idris requires that proofs be complete before compiling programs
|
||||
(although evaluation at the prompt is possible without proof details).
|
||||
@ -192,7 +192,7 @@ The ``exact`` tactic allows us to provide an exact value for the proof.
|
||||
In this case, we assert that the value we gave was correct.
|
||||
|
||||
Example: Binary numbers
|
||||
-----------------------
|
||||
=======================
|
||||
|
||||
Previously, we implemented conversion to binary numbers using the
|
||||
``Parity`` view. Here, we show how to use the same view to implement a
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
.. _sect-starting:
|
||||
|
||||
===============
|
||||
***************
|
||||
Getting Started
|
||||
===============
|
||||
***************
|
||||
|
||||
Prerequisites
|
||||
-------------
|
||||
=============
|
||||
|
||||
Before installing Idris, you will need to make sure you have all
|
||||
of the necessary libraries and tools. You will need:
|
||||
@ -18,7 +18,7 @@ of the necessary libraries and tools. You will need:
|
||||
from MacPorts/Homebrew and all major Linux distributions.
|
||||
|
||||
Downloading and Installing
|
||||
--------------------------
|
||||
==========================
|
||||
|
||||
The easiest way to install Idris, if you have all of the
|
||||
prerequisites, is to type:
|
||||
@ -69,7 +69,7 @@ instead. Some useful options to the Idris command are:
|
||||
- ``--help`` display usage summary and command line options
|
||||
|
||||
The Interactive Environment
|
||||
---------------------------
|
||||
===========================
|
||||
|
||||
Entering ``idris`` at the shell prompt starts up the interactive
|
||||
environment. You should see something like the following:
|
||||
|
||||
@ -1,14 +1,17 @@
|
||||
Syntax Extensions
|
||||
=================
|
||||
.. _sect-syntax:
|
||||
|
||||
supports the implementation of *Embedded Domain Specific Languages*
|
||||
(EDSLs) in several ways [1]_. One way, as we have already seen, is
|
||||
through extending ``do`` notation. Another important way is to allow
|
||||
extension of the core syntax. In this section we describe two ways of
|
||||
extending the syntax: ``syntax`` rules and ``dsl`` notation.
|
||||
*****************
|
||||
Syntax Extensions
|
||||
*****************
|
||||
|
||||
Idris supports the implementation of *Embedded Domain Specific
|
||||
Languages* (EDSLs) in several ways [1]_. One way, as we have already
|
||||
seen, is through extending ``do`` notation. Another important way is
|
||||
to allow extension of the core syntax. In this section we describe two
|
||||
ways of extending the syntax: ``syntax`` rules and ``dsl`` notation.
|
||||
|
||||
``syntax`` rules
|
||||
----------------
|
||||
================
|
||||
|
||||
We have seen ``if...then...else`` expressions, but these are not built
|
||||
in. Instead, we can define a function in the prelude as follows (we
|
||||
@ -101,7 +104,7 @@ a bound variable, substituted on the right hand side. We have also put
|
||||
``in`` in quotation marks since it is already a reserved word.
|
||||
|
||||
``dsl`` notation
|
||||
----------------
|
||||
================
|
||||
|
||||
The well-typed interpreter in Section :ref:`sect-interp` is a simple
|
||||
example of a common programming pattern with dependent types. Namely:
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
.. _sect-theorems:
|
||||
|
||||
===============
|
||||
***************
|
||||
Theorem Proving
|
||||
===============
|
||||
***************
|
||||
|
||||
Equality
|
||||
--------
|
||||
========
|
||||
|
||||
Idris allows propositional equalities to be declared, allowing theorems about
|
||||
programs to be stated and proved. Equality is built in, but conceptually
|
||||
@ -31,7 +31,7 @@ For example:
|
||||
.. _sect-empty:
|
||||
|
||||
The Empty Type
|
||||
--------------
|
||||
==============
|
||||
|
||||
There is an empty type, :math:`\bot`, which has no constructors. It is
|
||||
therefore impossible to construct an element of the empty type, at least
|
||||
@ -64,7 +64,7 @@ contradiction.
|
||||
void : Void -> a
|
||||
|
||||
Simple Theorems
|
||||
---------------
|
||||
===============
|
||||
|
||||
When type checking dependent types, the type itself gets *normalised*.
|
||||
So imagine we want to prove the following theorem about the reduction
|
||||
@ -116,16 +116,16 @@ We can do the same for the reduction behaviour of plus on successors:
|
||||
Even for trival theorems like these, the proofs are a little tricky to
|
||||
construct in one go. When things get even slightly more complicated, it
|
||||
becomes too much to think about to construct proofs in this ‘batch
|
||||
mode’.
|
||||
mode’.
|
||||
|
||||
Idris provides interactive editing capabilities, which can help with
|
||||
building proofs. For more details on building proofs interactively in
|
||||
an editor, see :ref:`proofs-index`.
|
||||
an editor, see :ref:`proofs-index`.
|
||||
|
||||
.. _sect-totality:
|
||||
|
||||
Totality Checking
|
||||
-----------------
|
||||
=================
|
||||
|
||||
If we really want to trust our proofs, it is important that they are
|
||||
defined by *total* functions — that is, a function which is defined for
|
||||
@ -195,7 +195,7 @@ total, a function ``f`` must:
|
||||
- Not call any non-total functions
|
||||
|
||||
Directives and Compiler Flags for Totality
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
------------------------------------------
|
||||
|
||||
By default, Idris allows all well-typed definitions, whether total or not.
|
||||
However, it is desirable for functions to be total as far as possible, as this
|
||||
@ -216,7 +216,7 @@ Finally, the compiler flag ``--warnpartial`` causes to print a warning
|
||||
for any undeclared partial function.
|
||||
|
||||
Totality checking issues
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
------------------------
|
||||
|
||||
Please note that the totality checker is not perfect! Firstly, it is
|
||||
necessarily conservative due to the undecidability of the halting
|
||||
@ -226,14 +226,14 @@ into it so far, so there may still be cases where it believes a function
|
||||
is total which is not. Do not rely on it for your proofs yet!
|
||||
|
||||
Hints for totality
|
||||
~~~~~~~~~~~~~~~~~~
|
||||
------------------
|
||||
|
||||
In cases where you believe a program is total, but Idris does not agree, it is
|
||||
possible to give hints to the checker to give more detail for a termination
|
||||
argument. The checker works by ensuring that all chains of recursive calls
|
||||
eventually lead to one of the arguments decreasing towards a base case, but
|
||||
sometimes this is hard to spot. For example, the following definition cannot be
|
||||
checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``
|
||||
checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``
|
||||
will always be smaller than ``(x :: xs)``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
.. _sect-typefuns:
|
||||
|
||||
===================
|
||||
*******************
|
||||
Types and Functions
|
||||
===================
|
||||
*******************
|
||||
|
||||
Primitive Types
|
||||
---------------
|
||||
===============
|
||||
|
||||
Idris defines several primitive types: ``Int``, ``Integer`` and
|
||||
``Float`` for numeric operations, ``Char`` and ``String`` for text
|
||||
@ -71,7 +71,7 @@ work on user defined types. Boolean expressions can be tested with the
|
||||
"The answer!" : String
|
||||
|
||||
Data Types
|
||||
----------
|
||||
==========
|
||||
|
||||
Data types are declared in a similar way to Haskell data types, with a
|
||||
similar syntax. Natural numbers and lists, for example, can be
|
||||
@ -105,7 +105,7 @@ symbols:
|
||||
:+-*/=_.?|&><!@$%^~.
|
||||
|
||||
Functions
|
||||
---------
|
||||
=========
|
||||
|
||||
Functions are implemented by pattern matching, again using a similar
|
||||
syntax to Haskell. The main difference is that Idris requires type
|
||||
@ -175,7 +175,7 @@ numbers. This means it can optimise the representation, and functions
|
||||
such as ``plus`` and ``mult``.
|
||||
|
||||
``where`` clauses
|
||||
~~~~~~~~~~~~~~~~~
|
||||
-----------------
|
||||
|
||||
Functions can also be defined *locally* using ``where`` clauses. For
|
||||
example, to define a function which reverses a list, we can use an
|
||||
@ -241,10 +241,10 @@ So, for example, the following definitions are legal:
|
||||
where z w = y + w
|
||||
|
||||
Dependent Types
|
||||
---------------
|
||||
===============
|
||||
|
||||
Vectors
|
||||
~~~~~~~
|
||||
-------
|
||||
|
||||
A standard example of a dependent type is the type of “lists with
|
||||
length”, conventionally called vectors in the dependent type
|
||||
@ -322,7 +322,7 @@ two vectors — we needed a vector of length ``k + m``, but provided a
|
||||
vector of length ``k + k``.
|
||||
|
||||
The Finite Sets
|
||||
~~~~~~~~~~~~~~~
|
||||
---------------
|
||||
|
||||
Finite sets, as the name suggests, are sets with a finite number of
|
||||
elements. They are available as part of the Idris library, by
|
||||
@ -337,12 +337,12 @@ importing ``Data.Fin``, or can be declared as follows:
|
||||
From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
|
||||
So this is not a set in the sense of a collection that is a container of objects,
|
||||
rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
|
||||
Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
|
||||
Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
|
||||
``n`` is the argument used to instantiate the ``Fin`` type.
|
||||
For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
|
||||
|
||||
Let us look at the constructors in greater detail.
|
||||
|
||||
|
||||
``FZ`` is the zeroth element of a finite set with ``S k`` elements;
|
||||
``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
|
||||
elements. ``Fin`` is indexed by a ``Nat``, which represents the number
|
||||
@ -377,7 +377,7 @@ attempting to look up an element in an empty vector would give a
|
||||
compile time type error, since it would force ``n`` to be ``Z``.
|
||||
|
||||
Implicit Arguments
|
||||
~~~~~~~~~~~~~~~~~~
|
||||
------------------
|
||||
|
||||
Let us take a closer look at the type of ``index``:
|
||||
|
||||
@ -420,7 +420,7 @@ help document a function by making the purpose of an argument more
|
||||
clear.
|
||||
|
||||
“``using``” notation
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
--------------------
|
||||
|
||||
Sometimes it is useful to provide types of implicit arguments,
|
||||
particularly where there is a dependency ordering, or where the
|
||||
@ -460,7 +460,7 @@ appear within the block:
|
||||
There : Elem x xs -> Elem x (y :: xs)
|
||||
|
||||
Note: Declaration Order and ``mutual`` blocks
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
---------------------------------------------
|
||||
|
||||
In general, functions and data types must be defined before use, since
|
||||
dependent types allow functions to appear as part of types, and their
|
||||
@ -485,7 +485,7 @@ depend on the reduction behaviour of any of the functions in the
|
||||
block.
|
||||
|
||||
I/O
|
||||
---
|
||||
===
|
||||
|
||||
Computer programs are of little use if they do not interact with the
|
||||
user or the system in some way. The difficulty in a pure language such
|
||||
@ -542,7 +542,7 @@ example for reading and writing files, including:
|
||||
.. _sect-do:
|
||||
|
||||
“``do``” notation
|
||||
-----------------
|
||||
=================
|
||||
|
||||
I/O programs will typically need to sequence actions, feeding the
|
||||
output of one computation into the input of the next. ``IO`` is an
|
||||
@ -573,7 +573,7 @@ can be overloaded.
|
||||
.. _sect-lazy:
|
||||
|
||||
Laziness
|
||||
--------
|
||||
========
|
||||
|
||||
Normally, arguments to functions are evaluated before the function
|
||||
itself (that is, Idris uses *eager* evaluation). However, this is
|
||||
@ -611,7 +611,7 @@ without any explicit use of ``Force`` or ``Delay``:
|
||||
boolCase False t e = e;
|
||||
|
||||
Useful Data Types
|
||||
-----------------
|
||||
=================
|
||||
|
||||
Idris includes a number of useful data types and library functions
|
||||
(see the ``libs/`` directory in the distribution). This chapter
|
||||
@ -619,7 +619,7 @@ describes a few of these. The functions described here are imported
|
||||
automatically by every Idris program, as part of ``Prelude.idr``.
|
||||
|
||||
``List`` and ``Vect``
|
||||
~~~~~~~~~~~~~~~~~~~~~
|
||||
---------------------
|
||||
|
||||
We have already seen the ``List`` and ``Vect`` data types:
|
||||
|
||||
@ -692,7 +692,7 @@ remember that Idris is still in development, so if you don’t see
|
||||
the function you need, please feel free to add it and submit a patch!
|
||||
|
||||
Aside: Anonymous functions and operator sections
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
------------------------------------------------
|
||||
|
||||
There are actually neater ways to write the above expression. One way
|
||||
would be to use an anonymous function:
|
||||
@ -719,7 +719,7 @@ by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand
|
||||
to ``\x => 2 * x``.
|
||||
|
||||
Maybe
|
||||
~~~~~
|
||||
-----
|
||||
|
||||
``Maybe`` describes an optional value. Either there is a value of the
|
||||
given type, or there isn’t:
|
||||
@ -753,7 +753,7 @@ simply ``b``. Since the default value might not be used, we mark it as
|
||||
discarding it would be wasteful.
|
||||
|
||||
Tuples and Dependent Pairs
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
--------------------------
|
||||
|
||||
Values can be paired with the following built-in data type:
|
||||
|
||||
@ -774,7 +774,7 @@ contain an arbitrary number of values, represented as nested pairs:
|
||||
jim = ("Jim", 25, "Cambridge")
|
||||
|
||||
Dependent Pairs
|
||||
~~~~~~~~~~~~~~~
|
||||
---------------
|
||||
|
||||
Dependent pairs allow the type of the second element of a pair to depend
|
||||
on the value of the first element. Traditionally, these are referred to
|
||||
@ -852,10 +852,10 @@ We will see more on ``with`` notation later.
|
||||
.. _sect-more-expr:
|
||||
|
||||
More Expressions
|
||||
----------------
|
||||
================
|
||||
|
||||
``let`` bindings
|
||||
~~~~~~~~~~~~~~~~
|
||||
----------------
|
||||
|
||||
Intermediate values can be calculated using ``let`` bindings:
|
||||
|
||||
@ -884,7 +884,7 @@ pattern matching at the top level:
|
||||
name ++ " is " ++ show age ++ " years old"
|
||||
|
||||
List comprehensions
|
||||
~~~~~~~~~~~~~~~~~~~
|
||||
-------------------
|
||||
|
||||
Idris provides *comprehension* notation as a convenient shorthand
|
||||
for building lists. The general form is:
|
||||
@ -911,7 +911,7 @@ by the difference between ``a`` and ``b``. This works for any numeric
|
||||
type, using the ``count`` function from the prelude.
|
||||
|
||||
``case`` expressions
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
--------------------
|
||||
|
||||
Another way of inspecting intermediate values of *simple* types is to
|
||||
use a ``case`` expression. The following function, for example, splits
|
||||
@ -965,7 +965,7 @@ matching ``let`` and lambda bindings. It will *only* work if:
|
||||
itself.
|
||||
|
||||
Dependent Records
|
||||
-----------------
|
||||
=================
|
||||
|
||||
*Records* are data types which collect several values (the record's
|
||||
*fields*) together. Idris provides syntax for defining records and
|
||||
@ -1036,7 +1036,7 @@ length because it will not affect the type of the record:
|
||||
: Class
|
||||
|
||||
Nested record update
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
--------------------
|
||||
|
||||
Idris also provides a convenient syntax for accessing and updating
|
||||
nested records. For example, if a field is accessible with the
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
.. _sec-views:
|
||||
|
||||
=============================
|
||||
*****************************
|
||||
Views and the “``with``” rule
|
||||
=============================
|
||||
*****************************
|
||||
|
||||
Dependent pattern matching
|
||||
--------------------------
|
||||
==========================
|
||||
|
||||
Since types can depend on values, the form of some arguments can be
|
||||
determined by the value of others. For example, if we were to write
|
||||
@ -25,7 +25,7 @@ case, the definition would not be well typed.
|
||||
.. _sect-nattobin:
|
||||
|
||||
The ``with`` rule — matching intermediate values
|
||||
------------------------------------------------
|
||||
================================================
|
||||
|
||||
Very often, we need to match on the result of an intermediate
|
||||
computation. Idris provides a construct for this, the ``with``
|
||||
|
||||
Loading…
Reference in New Issue
Block a user