mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-10-26 18:02:24 +03:00
Merge pull request #4408 from OlingCat/master
Fix some typos and normalize the use of punctuations.
This commit is contained in:
commit
ffd720aeec
@ -173,8 +173,10 @@ function back to itself. On such a path, there must be at least one
|
||||
argument which converges to a base case.
|
||||
|
||||
- Mutually recursive functions are supported
|
||||
|
||||
- However, all functions on the path must be fully applied. In particular,
|
||||
higher order applications are not supported
|
||||
|
||||
- Idris identifies arguments which converge to a base case by looking for
|
||||
recursive calls to syntactically smaller arguments of inputs. e.g.
|
||||
``k`` is syntactically smaller than ``S (S k)`` because ``k`` is a
|
||||
@ -233,14 +235,17 @@ where the install directory is unknown at build time. When passing this
|
||||
flag, the IDRIS_LIB_DIR environment variable needs to be set to the path
|
||||
where the Idris libs reside relative to the idris executable. The
|
||||
IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,
|
||||
Idris will use that path to find the C compiler.
|
||||
Idris will use that path to find the C compiler. For example:
|
||||
|
||||
Example::
|
||||
::
|
||||
|
||||
IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make
|
||||
IDRIS_LIB_DIR="./libs" \
|
||||
IDRIS_TOOLCHAIN_DIR="./mingw/bin" \
|
||||
CABALFLAGS="-fffi -ffreestanding -frelease" \
|
||||
make
|
||||
|
||||
|
||||
What does the name ‘Idris’ mean?
|
||||
What does the name “Idris” mean?
|
||||
================================
|
||||
|
||||
British people of a certain age may be familiar with this
|
||||
@ -256,16 +261,20 @@ There are several reasons why we should not support Unicode operators:
|
||||
- It's hard to type (this is important if you're using someone else's code, for
|
||||
example). Various editors have their own input methods, but you have to know
|
||||
what they are.
|
||||
|
||||
- Not every piece of software easily supports it. Rendering issues have been
|
||||
noted on some mobile email clients, terminal-based IRC clients, web browsers,
|
||||
etc. There are ways to resolve these rendering issues but they provide a
|
||||
barrier to entry to using Idris.
|
||||
|
||||
- Even if we leave it out of the standard library (which we will in any case!)
|
||||
as soon as people start using it in their library code, others have to deal
|
||||
with it.
|
||||
|
||||
- Too many characters look too similar. We had enough trouble with confusion
|
||||
between 0 and O without worrying about all the different kinds of colons and
|
||||
brackets.
|
||||
|
||||
- There seems to be a tendency to go over the top with use of Unicode. For
|
||||
example, using sharp and flat for delay and force (or is it the other way
|
||||
around?) in Agda seems gratuitous. We don't want to encourage this sort of
|
||||
@ -280,7 +289,7 @@ This seems like an instance of `Wadler's
|
||||
Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
|
||||
|
||||
This answer is based on Edwin Brady's response in the following
|
||||
`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`__.
|
||||
`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`_.
|
||||
|
||||
Where can I find the community standards for the Idris community?
|
||||
==================================================================
|
||||
|
@ -1,7 +1,7 @@
|
||||
.. _composing:
|
||||
|
||||
************************
|
||||
Composing State Machines
|
||||
Composing State Machines
|
||||
************************
|
||||
|
||||
In the previous section, we defined a ``DataStore`` interface and used it
|
||||
@ -28,7 +28,7 @@ there was a login failure in a state.
|
||||
|
||||
Furthermore, we may have *hierarchies* of state machines, in that one
|
||||
state machine could be implemented by composing several others. For
|
||||
example, we can have a state machine representing the state of a
|
||||
example, we can have a state machine representing the state of a
|
||||
graphics system, and use this to implement a *higher level* graphics API
|
||||
such as turtle graphics, which uses the graphics system plus some additional
|
||||
state for the turtle.
|
||||
@ -50,7 +50,7 @@ count to zero, a session might run as follows:
|
||||
*LoginCount> :exec main
|
||||
Enter password: Mornington Crescent
|
||||
Secret is: "Secret Data"
|
||||
Enter password: Dollis Hill
|
||||
Enter password: Dollis Hill
|
||||
Failure
|
||||
Number of failures: 1
|
||||
Enter password: Mornington Crescent
|
||||
@ -63,7 +63,7 @@ count to zero, a session might run as follows:
|
||||
We'll start by adding a state resource to ``getData`` to keep track of the
|
||||
number of failures:
|
||||
|
||||
.. code-block:: idrs
|
||||
.. code-block:: idris
|
||||
|
||||
getData : (ConsoleIO m, DataStore m) =>
|
||||
(failcount : Var) -> ST m () [failcount ::: State Integer]
|
||||
@ -116,7 +116,7 @@ match:
|
||||
Required result states here are: st2_fn
|
||||
|
||||
In other words, ``connect`` requires that there are *no* resources on
|
||||
entry, but we have *one*, the failure count!
|
||||
entry, but we have *one*, the failure count!
|
||||
This shouldn't be a problem, though: the required resources are a *subset* of
|
||||
the resources we have, after all, and the additional resources (here, the
|
||||
failure count) are not relevant to ``connect``. What we need, therefore,
|
||||
@ -214,7 +214,7 @@ ordering of resources is allowed to change, although resources which
|
||||
appear in ``old`` can't appear in the ``sub`` list more than once (you will
|
||||
get a type error if you try this).
|
||||
|
||||
The function ``updateWith`` takes the *output* resources of the
|
||||
The function ``updateWith`` takes the *output* resources of the
|
||||
called function, and updates them in the current resource list. It makes
|
||||
an effort to preserve ordering as far as possible, although this isn't
|
||||
always possible if the called function does some complicated resource
|
||||
@ -338,7 +338,7 @@ representing a surface on which we'll draw lines and rectangles:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Draw (m : Type -> Type) where
|
||||
interface Draw (m : Type -> Type) where
|
||||
Surface : Type
|
||||
|
||||
We'll need to be able to create a new ``Surface`` by opening a window:
|
||||
@ -369,7 +369,7 @@ succeeds (that is, returns a result of the form ``Just val``.
|
||||
an operation returns ``Just ty``, there's also ``addIfRight``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
||||
addIfJust : Type -> Action (Maybe Var)
|
||||
addIfRight : Type -> Action (Either a Var)
|
||||
|
||||
@ -378,10 +378,10 @@ succeeds (that is, returns a result of the form ``Just val``.
|
||||
of an operation:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
||||
Add : (ty -> Resources) -> Action ty
|
||||
|
||||
Using this, you can create your own actions to add resources
|
||||
|
||||
Using this, you can create your own actions to add resources
|
||||
based on the result of an operation, if required. For example,
|
||||
``addIfJust`` is implemented as follows:
|
||||
|
||||
@ -479,7 +479,7 @@ For example, assuming we have a surface ``win`` to draw onto, we can write a
|
||||
|
||||
The ``flip win`` at the end is necessary because the drawing primitives
|
||||
are double buffered, to prevent flicker. We draw onto one buffer, off-screen,
|
||||
and display the other. When we call ``flip``, it displays the off-screen
|
||||
and display the other. When we call ``flip``, it displays the off-screen
|
||||
buffer, and creates a new off-screen buffer for drawing the next frame.
|
||||
|
||||
To include this in a program, we'll write a main loop which renders our
|
||||
@ -496,7 +496,7 @@ application:
|
||||
|
||||
Finally, we can create a main program which initialises a window, if
|
||||
possible, then runs the main loop:
|
||||
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
drawMain : (ConsoleIO m, Draw m) => ST m () []
|
||||
@ -593,7 +593,7 @@ is implemented using the following type, defined by ``Control.ST``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Composite : List Type -> Type
|
||||
data Composite : List Type -> Type
|
||||
|
||||
If we have a composite resource, we can split it into its constituent
|
||||
resources, and create new variables for each of those resources, using
|
||||
@ -604,7 +604,7 @@ the *split* function. For example:
|
||||
splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]
|
||||
splitComp comp = do [int, str] <- split comp
|
||||
?whatNow
|
||||
|
||||
|
||||
The call ``split comp`` extracts the ``State Int`` and ``State String`` from
|
||||
the composite resource ``comp``, and stores them in the variables ``int``
|
||||
and ``str`` respectively. If we check the type of ``whatNow``, we'll see
|
||||
@ -713,7 +713,7 @@ A ``Line`` is defined as a start location, and end location, and a colour:
|
||||
Line : Type
|
||||
Line = ((Int, Int), (Int, Int), Col)
|
||||
|
||||
To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``
|
||||
To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``
|
||||
if this is impossible), we begin by initialising the drawing surface then
|
||||
all of the components of the state. Finally, we combine all of these
|
||||
into a composite resource for the turtle:
|
||||
|
@ -23,7 +23,6 @@ editor, and specifically how to do so in `Vim
|
||||
for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also
|
||||
available.
|
||||
|
||||
|
||||
Editing at the REPL
|
||||
===================
|
||||
|
||||
@ -64,9 +63,9 @@ Editing Commands
|
||||
:addclause
|
||||
----------
|
||||
|
||||
The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a
|
||||
The ``:addclause n f`` command, abbreviated ``:ac n f``, creates a
|
||||
template definition for the function named ``f`` declared on line
|
||||
``n``. For example, if the code beginning on line 94 contains:
|
||||
``n``. For example, if the code beginning on line 94 contains:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -129,7 +128,7 @@ ys`` would lead to a unification error.
|
||||
|
||||
The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the
|
||||
clauses which are required to make the function ``f`` on line ``n``
|
||||
cover all inputs. For example, if the code beginning on line 94 is
|
||||
cover all inputs. For example, if the code beginning on line 94 is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -143,7 +142,7 @@ then ``:am 96 vzipWith`` gives:
|
||||
|
||||
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
|
||||
|
||||
That is, it notices that there are no cases for non-empty vectors,
|
||||
That is, it notices that there are no cases for empty vectors,
|
||||
generates the required clauses, and eliminates the clauses which would
|
||||
lead to unification errors.
|
||||
|
||||
|
@ -11,8 +11,8 @@ data types. For example, we would like arithmetic operators to work on
|
||||
to display different types in a uniform way.
|
||||
|
||||
To achieve this, we use *interfaces*, which are similar to type classes in
|
||||
Haskell or traits in Rust. To define an interface, we provide a collection of
|
||||
overloadable functions. A simple example is the ``Show``
|
||||
Haskell or traits in Rust. To define an interface, we provide a collection of
|
||||
overloadable functions. A simple example is the ``Show``
|
||||
interface, which is defined in the prelude and provides an interface for
|
||||
converting values to ``String``:
|
||||
|
||||
@ -31,8 +31,7 @@ This generates a function of the following type (which we call a
|
||||
We can read this as: “under the constraint that ``a`` has an implementation
|
||||
of ``Show``, take an input ``a`` and return a ``String``.” An implementation
|
||||
of an interface is defined by giving definitions of the methods of the interface.
|
||||
For example, the
|
||||
``Show`` implementation for ``Nat`` could be defined as:
|
||||
For example, the ``Show`` implementation for ``Nat`` could be defined as:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -49,7 +48,7 @@ Only one implementation of an interface can be given for a type — implementati
|
||||
not overlap. Implementation declarations can themselves have constraints.
|
||||
To help with resolution, the arguments of an implementation must be
|
||||
constructors (either data or type constructors) or variables
|
||||
(i.e. you cannot give an implementation for a function). For
|
||||
(i.e. you cannot give an implementation for a function). For
|
||||
example, to define a ``Show`` implementation for vectors, we need to know
|
||||
that there is a ``Show`` implementation for the element type, because we are
|
||||
going to use it to convert each element to a ``String``:
|
||||
@ -534,7 +533,7 @@ Named Implementations
|
||||
|
||||
It can be desirable to have multiple implementations of an interface for the
|
||||
same type, for example to provide alternative methods for sorting or printing
|
||||
values. To achieve this, implementations can be *named* as follows:
|
||||
values. To achieve this, implementations can be *named* as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -574,7 +573,7 @@ the prelude defines the following ``Semigroup`` interface:
|
||||
interface Semigroup ty where
|
||||
(<+>) : ty -> ty -> ty
|
||||
|
||||
Then it defines ``Monoid``, which extends ``Semigroup`` with a "neutral"
|
||||
Then it defines ``Monoid``, which extends ``Semigroup`` with a “neutral”
|
||||
value:
|
||||
|
||||
.. code-block:: idris
|
||||
|
@ -106,7 +106,7 @@ the ``Var`` constructor:
|
||||
|
||||
Var : HasType i G t -> Expr G t
|
||||
|
||||
So, in an expression ``\x,\y. x y``, the variable ``x`` would have a
|
||||
So, in an expression ``\x. \y. x y``, the variable ``x`` would have a
|
||||
de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
|
||||
represented as ``Stop``. We find these by counting the number of
|
||||
lambdas between the definition and the use.
|
||||
@ -194,7 +194,7 @@ each constructor, we translate it into the corresponding Idris value:
|
||||
interp env (If x t e) = if interp env x then interp env t
|
||||
else interp env e
|
||||
|
||||
Let us look at each case in turn. To translate a variable, we simply look it
|
||||
Let us look at each case in turn. To translate a variable, we simply look it
|
||||
up in the environment:
|
||||
|
||||
.. code-block:: idris
|
||||
|
@ -8,7 +8,7 @@ In this section we discuss a variety of additional features:
|
||||
|
||||
+ auto, implicit, and default arguments;
|
||||
+ literate programming;
|
||||
+ interfacing with external libraries through the foreign function
|
||||
+ interfacing with external libraries through the foreign function;
|
||||
+ interface;
|
||||
+ type providers;
|
||||
+ code generation; and
|
||||
@ -23,7 +23,7 @@ omitted when they can be inferred by the type checker, e.g.
|
||||
.. code-block:: idris
|
||||
|
||||
index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
|
||||
|
||||
|
||||
Auto implicit arguments
|
||||
------------------------
|
||||
|
||||
@ -69,17 +69,17 @@ In the case that a proof is not found, it can be provided explicitly as normal:
|
||||
.. code-block:: idris
|
||||
|
||||
head xs {p = ?headProof}
|
||||
|
||||
|
||||
Default implicit arguments
|
||||
---------------------------
|
||||
|
||||
Besides having Idris automatically find a value of a given type, sometimes we
|
||||
Besides having Idris automatically find a value of a given type, sometimes we
|
||||
want to have an implicit argument with a specific default value. In Idris, we can
|
||||
do this using the ``default`` annotation. While this is primarily intended to assist
|
||||
in automatically constructing a proof where auto fails, or finds an unhelpful value,
|
||||
it might be easier to first consider a simpler case, not involving proofs.
|
||||
in automatically constructing a proof where auto fails, or finds an unhelpful value,
|
||||
it might be easier to first consider a simpler case, not involving proofs.
|
||||
|
||||
If we want to compute the n'th fibonacci number (and defining the 0th fibonacci
|
||||
If we want to compute the n'th fibonacci number (and defining the 0th fibonacci
|
||||
number as 0), we could write:
|
||||
|
||||
.. code-block:: idris
|
||||
@ -89,8 +89,8 @@ number as 0), we could write:
|
||||
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
|
||||
|
||||
After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
|
||||
and will return the 5th fibonacci number. Note that while this works, this is not the
|
||||
intended use of the ``default`` annotation. It is included here for illustrative purposes
|
||||
and will return the 5th fibonacci number. Note that while this works, this is not the
|
||||
intended use of the ``default`` annotation. It is included here for illustrative purposes
|
||||
only. Usually, ``default`` is used to provide things like a custom proof search script.
|
||||
|
||||
|
||||
@ -329,13 +329,13 @@ are available in an external collection [1]_.
|
||||
C Target
|
||||
========
|
||||
|
||||
The default target of Idris is C. Compiling via :
|
||||
The default target of Idris is C. Compiling via:
|
||||
|
||||
::
|
||||
|
||||
$ idris hello.idr -o hello
|
||||
|
||||
is equivalent to :
|
||||
is equivalent to:
|
||||
|
||||
::
|
||||
|
||||
@ -344,14 +344,14 @@ is equivalent to :
|
||||
When the command above is used, a temporary C source is generated, which
|
||||
is then compiled into an executable named ``hello``.
|
||||
|
||||
In order to view the generated C code, compile via :
|
||||
In order to view the generated C code, compile via:
|
||||
|
||||
::
|
||||
|
||||
$ idris hello.idr -S -o hello.c
|
||||
|
||||
To turn optimisations on, use the ``%flag C`` pragma within the code, as
|
||||
is shown below :
|
||||
is shown below:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -368,7 +368,7 @@ is shown below :
|
||||
|
||||
To compile the generated C with debugging information e.g. to use
|
||||
``gdb`` to debug segmentation faults in Idris programs, use the
|
||||
``%flag C`` pragma to include debugging symbols, as is shown below :
|
||||
``%flag C`` pragma to include debugging symbols, as is shown below:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -503,13 +503,13 @@ And for use in the browser:
|
||||
|
||||
The given files will be added to the top of the generated code.
|
||||
For library packages you can also use the ipkg objs option to include the
|
||||
js file in the installation, and use
|
||||
js file in the installation, and use:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%include Node "package/external.js"
|
||||
|
||||
This javascript and node backends idris will also lookup for the file on
|
||||
The *JavaScript* and *NodeJS* backends of Idris will also lookup for the file
|
||||
on that location.
|
||||
|
||||
Including *NodeJS* modules
|
||||
@ -552,7 +552,7 @@ types themselves have types. For example:
|
||||
*universe> :t Vect
|
||||
Vect : Nat -> Type -> Type
|
||||
|
||||
But what about the type of ``Type``? If we ask Idris it reports
|
||||
But what about the type of ``Type``? If we ask Idris it reports:
|
||||
|
||||
::
|
||||
|
||||
@ -560,8 +560,8 @@ But what about the type of ``Type``? If we ask Idris it reports
|
||||
Type : Type 1
|
||||
|
||||
If ``Type`` were its own type, it would lead to an inconsistency due to
|
||||
`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_ , so internally there is a
|
||||
*hierarchy* of types (or *universes*):
|
||||
`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
|
||||
so internally there is a *hierarchy* of types (or *universes*):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
@ -53,8 +53,7 @@ Then, this gives a main program (in a file
|
||||
print (Btree.toList t)
|
||||
|
||||
The same names can be defined in multiple modules: names are *qualified* with
|
||||
the name of the module. The names defined in the ``Btree`` module are, in
|
||||
full:
|
||||
the name of the module. The names defined in the ``Btree`` module are, in full:
|
||||
|
||||
+ ``Btree.BTree``
|
||||
+ ``Btree.Leaf``
|
||||
@ -74,7 +73,7 @@ directories. For example, ``import foo.bar`` would import the file
|
||||
``foo/bar.idr``, which would conventionally have the module declaration
|
||||
``module foo.bar``. The only requirement for module names is that the
|
||||
main module, with the ``main`` function, must be called
|
||||
``Main``—although its filename need not be ``Main.idr``.
|
||||
``Main`` — although its filename need not be ``Main.idr``.
|
||||
|
||||
Export Modifiers
|
||||
================
|
||||
@ -82,18 +81,16 @@ Export Modifiers
|
||||
Idris allows for fine-grained control over the visibility of a
|
||||
module's contents. By default, all names defined in a module are kept
|
||||
private. This aides in specification of a minimal interface and for
|
||||
internal details to be left hidden. Idris allows for functions,
|
||||
internal details to be left hidden. Idris allows for functions,
|
||||
types, and interfaces to be marked as: ``private``, ``export``, or
|
||||
``public export``. Their general meaning is as follows:
|
||||
``public export``. Their general meaning is as follows:
|
||||
|
||||
- ``private`` meaning that it's not exported at all. This is the
|
||||
default.
|
||||
- ``private`` meaning that it's not exported at all. This is the default.
|
||||
|
||||
- ``export`` meaning that its top level type is exported.
|
||||
|
||||
- ``public export`` meaning that the entire definition is exported.
|
||||
|
||||
|
||||
A further restriction in modifying the visibility is that definitions
|
||||
must not refer to anything within a lower level of visibility. For
|
||||
example, ``public export`` definitions cannot use private names, and
|
||||
@ -129,10 +126,9 @@ Meaning for Data Types
|
||||
|
||||
For data types, the meanings are:
|
||||
|
||||
- ``export`` the type constructor is exported
|
||||
- ``export`` the type constructor is exported
|
||||
|
||||
- ``public export`` the type constructor and data constructors are
|
||||
exported
|
||||
- ``public export`` the type constructor and data constructors are exported
|
||||
|
||||
|
||||
Meaning for Interfaces
|
||||
@ -141,6 +137,7 @@ Meaning for Interfaces
|
||||
For interfaces, the meanings are:
|
||||
|
||||
- ``export`` the interface name is exported
|
||||
|
||||
- ``public export`` the interface name, method names and default
|
||||
definitions are exported
|
||||
|
||||
|
@ -1,26 +1,31 @@
|
||||
.. _sect-packages:
|
||||
|
||||
********
|
||||
Packages
|
||||
********
|
||||
|
||||
|
||||
Idris includes a simple build system for building packages and executables from a named package description file.
|
||||
These files can be used with the Idris compiler to manage the development process .
|
||||
Idris includes a simple build system for building packages and executables
|
||||
from a named package description file. These files can be used with the
|
||||
Idris compiler to manage the development process .
|
||||
|
||||
Package Descriptions
|
||||
====================
|
||||
|
||||
A package description includes the following:
|
||||
|
||||
+ A header, consisting of the keyword package followed by the package
|
||||
+ A header, consisting of the keyword ``package`` followed by a package
|
||||
name. Package names can be any valid Idris identifier. The iPKG
|
||||
format also takes a quoted version that accepts any valid filename.
|
||||
+ Fields describing package contents, ``<field> = <value>``
|
||||
|
||||
+ Fields describing package contents, ``<field> = <value>``.
|
||||
|
||||
At least one field must be the modules field, where the value is a
|
||||
comma separated list of modules. For example, given an idris package
|
||||
comma separated list of modules. For example, given an idris package
|
||||
``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
|
||||
``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
|
||||
package file would be::
|
||||
package file would be:
|
||||
|
||||
::
|
||||
|
||||
package maths
|
||||
|
||||
@ -38,7 +43,6 @@ of the main Idris repository, and in `third-party libraries
|
||||
Using Package files
|
||||
===================
|
||||
|
||||
|
||||
Idris itself is aware about packages, and special commands are
|
||||
available to help with, for example, building packages, installing
|
||||
packages, and cleaning packages. For instance, given the ``maths``
|
||||
@ -54,7 +58,9 @@ package from earlier we can use Idris as follows:
|
||||
|
||||
Once the maths package has been installed, the command line option
|
||||
``--package maths`` makes it accessible (abbreviated to ``-p maths``).
|
||||
For example::
|
||||
For example:
|
||||
|
||||
::
|
||||
|
||||
idris -p maths Main.idr
|
||||
|
||||
@ -66,20 +72,18 @@ The integrated build system includes a simple testing framework.
|
||||
This framework collects functions listed in the ``ipkg`` file under ``tests``.
|
||||
All test functions must return ``IO ()``.
|
||||
|
||||
|
||||
When you enter ``idris --testpkg yourmodule.ipkg``,
|
||||
the build system creates a temporary file in a fresh environment on your machine
|
||||
by listing the ``tests`` functions under a single ``main`` function.
|
||||
It compiles this temporary file to an executable and then executes it.
|
||||
|
||||
|
||||
The tests themselves are responsible for reporting their success or failure.
|
||||
Test functions commonly use ``putStrLn`` to report test results.
|
||||
The test framework does not impose any standards for reporting and consequently
|
||||
does not aggregate test results.
|
||||
|
||||
|
||||
For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
|
||||
For example, lets take the following list of functions that are defined in a
|
||||
module called ``NumOps`` for a sample package ``maths``:
|
||||
|
||||
.. name: Math/NumOps.idr
|
||||
.. code-block:: idris
|
||||
@ -94,7 +98,8 @@ For example, lets take the following list of functions that are defined in a mod
|
||||
triple : Num a => a -> a
|
||||
triple a = a + double a
|
||||
|
||||
A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
|
||||
|
||||
A simple test module, with a qualified name of ``Test.NumOps`` can be declared as:
|
||||
|
||||
.. name: Math/TestOps.idr
|
||||
.. code-block:: idris
|
||||
@ -122,8 +127,11 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a
|
||||
testTriple = assertNotEq (triple 2) 5
|
||||
|
||||
|
||||
The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
|
||||
The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
|
||||
The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing,
|
||||
and failing, equality tests. The actual tests are ``testDouble`` and ``testTriple``,
|
||||
and are declared in the ``maths.ipkg`` file as follows:
|
||||
|
||||
::
|
||||
|
||||
package maths
|
||||
|
||||
@ -134,7 +142,9 @@ The actual tests are ``testDouble`` and ``testTriple``, and are declared in the
|
||||
, Test.NumOps.testTriple
|
||||
|
||||
|
||||
The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
|
||||
The testing framework can then be invoked using ``idris --testpkg maths.ipkg``:
|
||||
|
||||
::
|
||||
|
||||
> idris --testpkg maths.ipkg
|
||||
Type checking ./Maths/NumOps.idr
|
||||
@ -146,25 +156,25 @@ The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
|
||||
Note how both tests have reported success by printing ``Test Passed``
|
||||
as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.
|
||||
|
||||
Package Dependencies Using Atom
|
||||
Package Dependencies Using Atom
|
||||
===============================
|
||||
|
||||
If you are using the Atom editor and have a dependency on another package,
|
||||
corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,
|
||||
you need to let Atom know that it should be loaded. The easiest way to
|
||||
accomplish that is with a .ipkg file. The general contents of an ipkg file
|
||||
will be described in the next section of the tutorial, but for now here is
|
||||
a simple recipe for this trivial case.
|
||||
If you are using the Atom editor and have a dependency on another package,
|
||||
corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,
|
||||
you need to let Atom know that it should be loaded. The easiest way to
|
||||
accomplish that is with a .ipkg file. The general contents of an ipkg file
|
||||
will be described in the next section of the tutorial, but for now here is
|
||||
a simple recipe for this trivial case:
|
||||
|
||||
- Create a folder myProject.
|
||||
- Create a folder myProject.
|
||||
|
||||
- Add a file myProject.ipkg containing just a couple of lines:
|
||||
- Add a file myProject.ipkg containing just a couple of lines:
|
||||
|
||||
``package myProject``
|
||||
``package myProject``
|
||||
|
||||
``pkgs = pruviloj, lightyear``
|
||||
``pkgs = pruviloj, lightyear``
|
||||
|
||||
- In Atom, use the File menu to Open Folder myProject.
|
||||
- In Atom, use the File menu to Open Folder myProject.
|
||||
|
||||
More information
|
||||
================
|
||||
|
@ -34,7 +34,7 @@ rule, and the right hand side describes its expansion. The syntax rule
|
||||
itself consists of:
|
||||
|
||||
- **Keywords** — here, ``if``, ``then`` and ``else``, which must be
|
||||
valid identifiers
|
||||
valid identifiers.
|
||||
|
||||
- **Non-terminals** — included in square brackets, ``[test]``, ``[t]``
|
||||
and ``[e]`` here, which stand for arbitrary expressions. To avoid
|
||||
@ -44,9 +44,9 @@ itself consists of:
|
||||
- **Names** — included in braces, which stand for names which may be
|
||||
bound on the right hand side.
|
||||
|
||||
- **Symbols** — included in quotations marks, e.g. ``:=``. This can
|
||||
- **Symbols** — included in quotations marks, e.g. ``":="``. This can
|
||||
also be used to include reserved words in syntax rules, such as
|
||||
``let`` or ``in``.
|
||||
``"let"`` or ``"in"``.
|
||||
|
||||
The limitations on the form of a syntax rule are that it must include
|
||||
at least one symbol or keyword, and there must be no repeated
|
||||
@ -63,7 +63,7 @@ recursive. The following syntax extensions would therefore be valid:
|
||||
syntax select [x] from [t] "where" [w] = SelectWhere x t w;
|
||||
syntax select [x] from [t] = Select x t;
|
||||
|
||||
Syntax macros can be further restricted to apply only in patterns (i.e.,
|
||||
Syntax macros can be further restricted to apply only in patterns (i.e.
|
||||
only on the left hand side of a pattern match clause) or only in terms
|
||||
(i.e. everywhere but the left hand side of a pattern match clause) by
|
||||
being marked as ``pattern`` or ``term`` syntax rules. For example, we
|
||||
|
@ -115,8 +115,8 @@ We can do the same for the reduction behaviour of plus on successors:
|
||||
|
||||
Even for trivial 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’.
|
||||
becomes too much to think about to construct proofs in this “batch
|
||||
mode”.
|
||||
|
||||
Idris provides interactive editing capabilities, which can help with
|
||||
building proofs. For more details on building proofs interactively in
|
||||
@ -383,7 +383,7 @@ will always be smaller than ``(x :: xs)``:
|
||||
= qsort (filter (< x) xs) ++
|
||||
(x :: qsort (filter (>= x) xs))
|
||||
|
||||
The function ``assert_smaller``, defined in the Prelude, is intended to
|
||||
The function ``assert_smaller``, defined in the prelude, is intended to
|
||||
address this problem:
|
||||
|
||||
.. code-block:: idris
|
||||
|
@ -13,8 +13,7 @@ manipulation, and ``Ptr`` which represents foreign pointers. There are
|
||||
also several data types declared in the library, including ``Bool``,
|
||||
with values ``True`` and ``False``. We can declare some constants with
|
||||
these types. Enter the following into a file ``Prims.idr`` and load it
|
||||
into the Idris interactive environment by typing ``idris
|
||||
Prims.idr``:
|
||||
into the Idris interactive environment by typing ``idris Prims.idr``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -38,7 +37,7 @@ collection of declarations and definitions. In this example no imports
|
||||
have been specified. However Idris programs can consist of several
|
||||
modules and the definitions in each module each have their own
|
||||
namespace. This is discussed further in Section
|
||||
:ref:`sect-namespaces`). When writing Idris programs both the order in which
|
||||
:ref:`sect-namespaces`. When writing Idris programs both the order in which
|
||||
definitions are given and indentation are significant. Functions and
|
||||
data types must be defined before use, incidentally each definition must
|
||||
have a type declaration, for example see ``x : Int``, ``foo :
|
||||
@ -343,7 +342,7 @@ Vectors
|
||||
|
||||
A standard example of a dependent data type is the type of “lists with
|
||||
length”, conventionally called vectors in the dependent type
|
||||
literature. They are available as part of the Idris library, by
|
||||
literature. They are available as part of the Idris library, by
|
||||
importing ``Data.Vect``, or we can declare them as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
@ -521,8 +520,8 @@ help document a function by making the purpose of an argument more
|
||||
clear.
|
||||
|
||||
Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.
|
||||
``{var = pat}`` gets an implicit variable and attempts to pattern match on "pat";
|
||||
For example :
|
||||
``{var = pat}`` gets an implicit variable and attempts to pattern match on “pat”;
|
||||
For example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -559,7 +558,6 @@ vector. For example:
|
||||
inVect : IsElem 5 Main.testVec
|
||||
inVect = There (There Here)
|
||||
|
||||
|
||||
.. important:: Implicit Arguments and Scope
|
||||
|
||||
Within the type signature the typechecker will treat all variables
|
||||
@ -569,7 +567,6 @@ vector. For example:
|
||||
``testVec``. In the example above, we have assumed that the code
|
||||
lives within the ``Main`` module.
|
||||
|
||||
|
||||
If the same implicit arguments are being used a lot, it can make a
|
||||
definition difficult to read. To avoid this problem, a ``using`` block
|
||||
gives the types and ordering of any implicit arguments which can
|
||||
@ -582,15 +579,13 @@ appear within the block:
|
||||
Here : IsElem x (x :: xs)
|
||||
There : IsElem x xs -> IsElem 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 type
|
||||
checking can rely on how particular functions are defined (though this
|
||||
is only true of total functions; see Section :ref:`sect-totality`)).
|
||||
is only true of total functions; see Section :ref:`sect-totality`).
|
||||
However, this restriction can be relaxed by using a ``mutual`` block,
|
||||
which allows data types and functions to be defined simultaneously:
|
||||
|
||||
@ -673,7 +668,7 @@ Note that several of these return ``Either``, since they may fail.
|
||||
I/O programs will typically need to sequence actions, feeding the
|
||||
output of one computation into the input of the next. ``IO`` is an
|
||||
abstract type, however, so we can’t access the result of a computation
|
||||
directly. Instead, we sequence operations with ``do`` notation:
|
||||
directly. Instead, we sequence operations with ``do`` notation:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -713,7 +708,7 @@ not always the best approach. Consider the following function:
|
||||
|
||||
This function uses one of the ``t`` or ``e`` arguments, but not both
|
||||
(in fact, this is used to implement the ``if...then...else`` construct
|
||||
as we will see later. We would prefer if *only* the argument which was
|
||||
as we will see later). We would prefer if *only* the argument which was
|
||||
used was evaluated. To achieve this, Idris provides a ``Lazy``
|
||||
data type, which allows evaluation to be suspended:
|
||||
|
||||
@ -797,7 +792,7 @@ infinite loop and cause a stack overflow.
|
||||
To fix this we must add explicit ``Inf`` declarations to the constructor
|
||||
parameter types, since codata will not add it to constructor parameters of a
|
||||
**different** type from the one being defined. For example, the following
|
||||
outputs "1".
|
||||
outputs ``1``.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -902,7 +897,7 @@ For more details of the functions available on ``List`` and
|
||||
|
||||
- ``libs/base/Data/VectType.idr``
|
||||
|
||||
Functions include filtering, appending, reversing, and so on.
|
||||
Functions include filtering, appending, reversing, and so on.
|
||||
|
||||
Aside: Anonymous functions and operator sections
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
@ -999,7 +994,7 @@ Dependent Pairs
|
||||
---------------
|
||||
|
||||
Dependent pairs allow the type of the second element of a pair to depend
|
||||
on the value of the first element.
|
||||
on the value of the first element:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -1009,7 +1004,7 @@ on the value of the first element.
|
||||
Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type
|
||||
of a pair of A and P, where the name ``a`` can occur inside ``P``.
|
||||
``( a ** p )`` constructs a value of this type. For example, we can
|
||||
pair a number with a ``Vect`` of a particular length.
|
||||
pair a number with a ``Vect`` of a particular length:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -1017,7 +1012,7 @@ pair a number with a ``Vect`` of a particular length.
|
||||
vec = (2 ** [3, 4])
|
||||
|
||||
If you like, you can write it out the long way, the two are precisely
|
||||
equivalent.
|
||||
equivalent:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -1070,7 +1065,7 @@ intermediate values:
|
||||
|
||||
We will see more on ``with`` notation later.
|
||||
|
||||
Dependent pairs are sometimes referred to as “sigma types”.
|
||||
Dependent pairs are sometimes referred to as “Sigma types”.
|
||||
|
||||
Records
|
||||
-------
|
||||
@ -1080,7 +1075,7 @@ Records
|
||||
automatically generating field access and update functions. Unlike
|
||||
the syntax used for data structures, records in Idris follow a
|
||||
different syntax to that seen with Haskell. For example, we can
|
||||
represent a person's name and age in a record:
|
||||
represent a person’s name and age in a record:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -1092,12 +1087,11 @@ represent a person's name and age in a record:
|
||||
fred : Person
|
||||
fred = MkPerson "Fred" "Joe" "Bloggs" 30
|
||||
|
||||
|
||||
The constructor name is provided using the ``constructor`` keyword,
|
||||
and the *fields* are then given which are in an indented block
|
||||
following the `where` keyword (here, ``firstName``, ``middleName``,
|
||||
``lastName``, and ``age``). You can declare multiple fields on a
|
||||
single line, provided that they have the same type. The field names
|
||||
single line, provided that they have the same type. The field names
|
||||
can be used to access the field values:
|
||||
|
||||
::
|
||||
@ -1171,7 +1165,7 @@ syntax:
|
||||
record { a->b->c = val } x
|
||||
|
||||
This returns a new record, with the field accessed by the path
|
||||
``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {
|
||||
``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {
|
||||
a->b->c = val }`` itself has a function type. Symmetrically, the field
|
||||
can also be accessed with the following syntax:
|
||||
|
||||
@ -1196,12 +1190,10 @@ name. For example, a pair type could be defined as follows:
|
||||
fst : a
|
||||
snd : b
|
||||
|
||||
|
||||
Using the ``class`` record from earlier, the size of the class can be
|
||||
restricted using a ``Vect`` and the size included in the type by parameterising
|
||||
the record with the size. For example:
|
||||
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
record SizedClass (size : Nat) where
|
||||
@ -1214,7 +1206,7 @@ function from earlier, since that would change the size of the class. A
|
||||
function to add a student must now specify in the type that the
|
||||
size of the class has been increased by one. As the size is specified
|
||||
using natural numbers, the new value can be incremented using the
|
||||
``S`` constructor.
|
||||
``S`` constructor:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -1327,7 +1319,7 @@ matching ``let`` and lambda bindings. It will *only* work if:
|
||||
- Each branch *matches* a value of the same type, and *returns* a
|
||||
value of the same type.
|
||||
|
||||
- The type of the result is "known". i.e. the type of the expression
|
||||
- The type of the result is “known”. i.e. the type of the expression
|
||||
can be determined *without* type checking the ``case``-expression
|
||||
itself.
|
||||
|
||||
@ -1337,7 +1329,7 @@ Totality
|
||||
Idris distinguishes between *total* and *partial* functions.
|
||||
A total function is a function that either:
|
||||
|
||||
+ Terminates for all possible inputs, or
|
||||
+ Terminates for all possible inputs, or
|
||||
+ Produces a non-empty, finite, prefix of a possibly infinite result
|
||||
|
||||
If a function is total, we can consider its type a precise description of what
|
||||
@ -1345,12 +1337,12 @@ that function will do. For example, if we have a function with a return
|
||||
type of ``String`` we know something different, depending on whether or not
|
||||
it's total:
|
||||
|
||||
+ If it's total, it will return a value of type ``String`` in finite time
|
||||
+ If it's total, it will return a value of type ``String`` in finite time;
|
||||
+ If it's partial, then as long as it doesn't crash or enter an infinite loop,
|
||||
it will return a ``String``.
|
||||
|
||||
Idris makes this distinction so that it knows which functions are safe to
|
||||
evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,
|
||||
evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,
|
||||
if it tries to evaluate a function during type checking which doesn't
|
||||
terminate, then type checking won't terminate!
|
||||
Therefore, only total functions will be evaluated during type checking.
|
||||
|
Loading…
Reference in New Issue
Block a user