1********************************************
2Running example: Addition of Natural Numbers
3********************************************
5Throughout this tutorial, we will be working with the following
6function, defined in the Idris prelude, which defines addition on
11 plus : Nat -> Nat -> Nat
13 plus (S k) m = S (plus k m)
15It is defined by the above equations, meaning that we have for free the
16properties that adding ``m`` to zero always results in ``m``, and that
17adding ``m`` to any non-zero number ``S k`` always results in
18``S (plus k m)``. We can see this by evaluation at the Idris REPL (i.e.
19the prompt, the read-eval-print loop):
26 Idris> \k,m => plus (S k) m
27 \k => \m => S (plus k m) : Nat -> Nat -> Nat
29Note that unlike many other language REPLs, the Idris REPL performs
30evaluation on *open* terms, meaning that it can reduce terms which
31appear inside lambda bindings, like those above. Therefore, we can
32introduce unknowns ``k`` and ``m`` as lambda bindings and see how
35The ``plus`` function has a number of other useful properties, for
38- It is *commutative*, that is for all ``Nat`` inputs ``n`` and ``m``,
39 we know that ``plus n m = plus m n``.
41- It is *associative*, that is for all ``Nat`` inputs ``n``, ``m`` and
42 ``p``, we know that ``plus n (plus m p) = plus (plus m n) p``.
44We can use these properties in an Idris program, but in order to do so
50Idris has a built-in propositional equality type, conceptually defined
55 data (=) : a -> b -> Type where
58Note that this must be built-in, rather than defined in the library,
59because ``=`` is a reserved operator — you cannot define this directly
62It is *propositional* equality, where the type states that any two
63values in different types ``a`` and ``b`` may be proposed to be equal.
64There is only one way to *prove* equality, however, which is by
65reflexivity (``Refl``).
67We have a *type* for propositional equality here, and correspondingly a
68*program* inhabiting an instance of this type can be seen as a proof of
69the corresponding proposition [1]_. So, trivially, we can prove that
77However, trying to prove that ``4 = 5`` results in failure:
84The type ``4 = 5`` is a perfectly valid type, but is uninhabited, so
85when trying to type check this definition, Idris gives the following
90 When elaborating right hand side of four_eq_five:
96Type checking equality proofs
97-----------------------------
99An important step in type checking Idris programs is *unification*,
100which attempts to resolve implicit arguments such as the implicit
101argument ``x`` in ``Refl``. As far as our understanding of type checking
102proofs is concerned, it suffices to know that unifying two terms
103involves reducing both to normal form then trying to find an assignment
104to implicit arguments which will make those normal forms equal.
106When type checking ``Refl``, Idris requires that the type is of the form
107``x = x``, as we see from the type of ``Refl``. In the case of
108``four_eq_five``, Idris will try to unify the expected type ``4 = 5``
109with the type of ``Refl``, ``x = x``, notice that a solution requires
110that ``x`` be both ``4`` and ``5``, and therefore fail.
112Since type checking involves reduction to normal form, we can write the
113following equalities directly:
117 twoplustwo_eq_four : 2 + 2 = 4
118 twoplustwo_eq_four = Refl
120 plus_reduces_Z : (m : Nat) -> plus Z m = m
121 plus_reduces_Z m = Refl
123 plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
124 plus_reduces_Sk k m = Refl
126Heterogeneous Equality
127======================
129Equality in Idris is *heterogeneous*, meaning that we can even propose
130equalities between values in different types:
134 idris_not_php : 2 = "2"
136Obviously, in Idris the type ``2 = "2"`` is uninhabited, and one might
137wonder why it is useful to be able to propose equalities between values
138in different types. However, with dependent types, such equalities can
139arise naturally. For example, if two vectors are equal, their lengths
144 vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) ->
147In the above declaration, ``xs`` and ``ys`` have different types because
148their lengths are different, but we would still like to draw a
149conclusion about the lengths if they happen to be equal. We can define
150``vect_eq_length`` as follows:
154 vect_eq_length xs xs Refl = Refl
156By matching on ``Refl`` for the third argument, we know that the only
157valid value for ``ys`` is ``xs``, because they must be equal, and
158therefore their types must be equal, so the lengths must be equal.
160Alternatively, we can put an underscore for the second ``xs``, since
161there is only one value which will type check:
165 vect_eq_length xs _ Refl = Refl
167Properties of ``plus``
168======================
170Using the ``(=)`` type, we can now state the properties of ``plus``
171given above as Idris type declarations:
175 plus_commutes : (n, m : Nat) -> plus n m = plus m n
176 plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p
178Both of these properties (and many others) are proved for natural number
179addition in the Idris standard library, using ``(+)`` from the ``Num``
180interface rather than using ``plus`` directly. They have the names
181``plusCommutative`` and ``plusAssociative`` respectively.
183In the remainder of this tutorial, we will explore several different
184ways of proving ``plus_commutes`` (or, to put it another way, writing
185the function.) We will also discuss how to use such equality proofs, and
186see where the need for them arises in practice.
189 This is known as the Curry-Howard correspondence.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list