Idris2/docs/source/tutorial/miscellany.rst
2023-11-23 14:28:15 -08:00

167 lines
5.3 KiB
ReStructuredText
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

.. _sect-misc:
**********
Miscellany
**********
In this section we discuss a variety of additional features:
+ auto, implicit, and default arguments;
+ literate programming; and
+ the universe hierarchy.
Implicit arguments
==================
We have already seen implicit arguments, which allows arguments to be
omitted when they can be inferred by the type checker [#IdrisType]_, e.g.
.. code-block:: idris
index : forall a, n . Fin n -> Vect n a -> a
.. _auto-implicit-arguments:
Auto implicit arguments
-----------------------
In other situations, it may be possible to infer arguments not by type
checking but by searching the context for an appropriate value, or
constructing a proof. For example, the following definition of ``head``
which requires a proof that the list is non-empty:
.. code-block:: idris
isCons : List a -> Bool
isCons [] = False
isCons (x :: xs) = True
head : (xs : List a) -> (isCons xs = True) -> a
head (x :: xs) _ = x
If the list is statically known to be non-empty, either because its
value is known or because a proof already exists in the context, the
proof can be constructed automatically. Auto implicit arguments allow
this to happen silently. We define ``head`` as follows:
.. code-block:: idris
head : (xs : List a) -> {auto p : isCons xs = True} -> a
head (x :: xs) = x
The ``auto`` annotation on the implicit argument means that Idris
will attempt to fill in the implicit argument by searching for a value
of the appropriate type. In fact, internally, this is exactly how interface
resolution works. It will try the following, in order:
- Local variables, i.e. names bound in pattern matches or ``let`` bindings,
with exactly the right type.
- The constructors of the required type. If they have arguments, it will
search recursively up to a maximum depth of 100.
- Local variables with function types, searching recursively for the
arguments.
- Any function with the appropriate return type which is marked with the
``%hint`` annotation.
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
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.
If we want to compute the n'th fibonacci number (and defining the 0th fibonacci
number as 0), we could write:
.. code-block:: idris
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
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
only. Usually, ``default`` is used to provide things like a custom proof search script.
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
literate programs, everything is assumed to be a comment unless the line
begins with a greater than sign ``>``, for example:
::
> module literate
This is a comment. The main program is below
> main : IO ()
> main = putStrLn "Hello literate world!\n"
An additional restriction is that there must be a blank line between a
program line (beginning with ``>``) and a comment line (beginning with
any other character).
Cumulativity
============
.. warning::
NOT YET IN IDRIS 2
Since values can appear in types and *vice versa*, it is natural that
types themselves have types. For example:
::
*universe> :t Nat
Nat : Type
*universe> :t Vect
Vect : Nat -> Type -> Type
But what about the type of ``Type``? If we ask Idris it reports:
::
*universe> :t Type
Type : Type 1
If ``Type`` were its own type, it would lead to an inconsistency due to
`Girards paradox <https://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
Type : Type 1 : Type 2 : Type 3 : ...
Universes are *cumulative*, that is, if ``x : Type n`` we can also have
that ``x : Type m``, as long as ``n < m``. The typechecker generates
such universe constraints and reports an error if any inconsistencies
are found. Ordinarily, a programmer does not need to worry about this,
but it does prevent (contrived) programs such as the following:
.. code-block:: idris
myid : (a : Type) -> a -> a
myid _ x = x
idid : (a : Type) -> a -> a
idid = myid _ myid
The application of ``myid`` to itself leads to a cycle in the universe
hierarchy — ``myid``\ s first argument is a ``Type``, which cannot be
at a lower level than required if it is applied to itself.
.. [#IdrisType] https://github.com/david-christiansen/idris-type-providers