7By now, we have seen several examples of how ``Idris``’ dependent type
8system can give extra confidence in a function’s correctness by giving a
9more precise description of its intended behaviour in its *type*. We
10have also seen an example of how the type system can help with EDSL
11development by allowing a programmer to describe the type system of an
12object language. However, precise types give us more than verification
13of programs — we can also exploit types to help write programs which are
14*correct by construction*.
16The ``Idris`` REPL provides several commands for inspecting and
17modifying parts of programs, based on their types, such as case
18splitting on a pattern variable, inspecting the type of a metavariable,
19and even a basic proof search mechanism. In this section, we explain how
20these features can be exploited by a text editor, and specifically how
21to do so in `Vim <https://github.com/idris-hackers/idris-vim>`_. An interactive mode for `Emacs <https://github.com/idris-hackers/idris-emacs>`_ is also
28The REPL provides a number of commands, which we will describe shortly,
29which generate new program fragments based on the currently loaded
30module. These take the general form
34 :command [line number] [name]
36That is, each command acts on a specific source line, at a specific
37name, and outputs a new program fragment. Each command has an
38alternative form, which *updates* the source file in-place:
42 :command! [line number] [name]
44When the REPL is loaded, it also starts a background process which
45accepts and responds to REPL commands, using ``idris --client``. For
46example, if we have a REPL running elsewhere, we can execute commands
51 $ idris --client ':t plus'
52 Prelude.Nat.plus : Nat -> Nat -> Nat
53 $ idris --client '2+2'
56A text editor can take advantage of this, along with the editing
57commands, in order to provide interactive editing support.
65The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a
66template definition for the function named ``f`` declared on line ``n``.
67For example, if the code beginning on line 94 contains:
71 vzipWith : (a -> b -> c) ->
72 Vect n a -> Vect n b -> Vect n c
74then ``:ac 94 vzipWith`` will give:
78 vzipWith f xs ys = ?vzipWith_rhs
80The names are chosen according to hints which may be given by a
81programmer, and then made unique by the machine by adding a digit if
82necessary. Hints can be given as follows:
86 %name Vect xs, ys, zs, ws
88This declares that any names generated for types in the ``Vect`` family
89should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.
94The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the
95pattern variable ``x`` on line ``n`` into the various pattern forms it
96may take, removing any cases which are impossible due to unification
97errors. For example, if the code beginning on line 94 is:
101 vzipWith : (a -> b -> c) ->
102 Vect n a -> Vect n b -> Vect n c
103 vzipWith f xs ys = ?vzipWith_rhs
105then ``:cs 96 xs`` will give:
109 vzipWith f [] ys = ?vzipWith_rhs_1
110 vzipWith f (x :: xs) ys = ?vzipWith_rhs_2
112That is, the pattern variable ``xs`` has been split into the two
113possible cases ``[]`` and ``x :: xs``. Again, the names are chosen
114according to the same heuristic. If we update the file (using ``:cs!``)
115then case split on ``ys`` on the same line, we get:
119 vzipWith f [] [] = ?vzipWith_rhs_3
121That is, the pattern variable ``ys`` has been split into one case
122``[]``, ``Idris`` having noticed that the other possible case
123``y :: ys`` would lead to a unification error.
128The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the
129clauses which are required to make the function ``f`` on line ``n``
130cover all inputs. For example, if the code beginning on line 94 is…
134 vzipWith : (a -> b -> c) ->
135 Vect n a -> Vect n b -> Vect n c
136 vzipWith f [] [] = ?vzipWith_rhs_1
138then ``:am 96 vzipWith`` gives:
142 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
144That is, it notices that there are no cases for non-empty vectors,
145generates the required clauses, and eliminates the clauses which would
146lead to unification errors.
151The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to
152find a value for the metavariable ``f`` on line ``n`` by proof search,
153trying values of local variables, recursive calls and constructors of
154the required family. Optionally, it can take a list of *hints*, which
155are functions it can try applying to solve the metavariable. For
156example, if the code beginning on line 94 is:
160 vzipWith : (a -> b -> c) ->
161 Vect n a -> Vect n b -> Vect n c
162 vzipWith f [] [] = ?vzipWith_rhs_1
163 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
165then ``:ps 96 vzipWith_rhs_1`` will give
171This works because it is searching for a ``Vect`` of length 0, of which
172the empty vector is the only possibiliy. Similarly, and perhaps
173surprisingly, there is only one possibility if we try to solve
174``:ps 97 vzipWith_rhs_2``:
178 f x y :: (vzipWith f xs ys)
180This works because ``vzipWith`` has a precise enough type: The resulting
181vector has to be non-empty (a ``::``); the first element must have type
182``c`` and the only way to get this is to apply ``f`` to ``x`` and ``y``;
183finally, the tail of the vector can only be built recursively.
188The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a ``with``
189to a pattern clause. For example, recall ``parity``. If line 10 is:
193 parity (S k) = ?parity_rhs
195then ``:mw 10 parity`` will give:
199 parity (S k) with (_)
200 parity (S k) | with_pat = ?parity_rhs
202If we then fill in the placeholder ``_`` with ``parity k`` and case
203split on ``with_pat`` using ``:cs 11 with_pat`` we get the following
208 parity (S (plus n n)) | even = ?parity_rhs_1
209 parity (S (S (plus n n))) | odd = ?parity_rhs_2
211Note that case splitting has normalised the patterns here (giving
212``plus`` rather than ``+``). In any case, we see that using interactive
213editing significantly simplifies the implementation of dependent pattern
214matching by showing a programmer exactly what the valid patterns are.
216Interactive Editing in Vim
217--------------------------
219The editor mode for Vim provides syntax highlighting, indentation and
220interactive editing support using the commands described above.
221Interactive editing is achieved using the following editor commands,
222each of which update the buffer directly:
224- ``\d`` adds a template definition for the name declared on the
225 current line (using ``:addclause``).
227- ``\c`` case splits the variable at the cursor (using ``:casesplit``).
229- ``\m`` adds the missing cases for the name at the cursor (using
232- ``\w`` adds a ``with`` clause (using ``:makewith``).
234- ``\o`` invokes a proof search to solve the metavariable under the
235 cursor (using ``:proofsearch``).
237- ``\p`` invokes a proof search with additional hints to solve the
238 metavariable under the cursor (using ``:proofsearch``).
240There are also commands to invoke the type checker and evaluator:
242- ``\t`` displays the type of the (globally visible) name under the
243 cursor. In the case of a metavariable, this displays the context and
246- ``\e`` prompts for an expression to evaluate.
248- ``\r`` reloads and type checks the buffer.
250Corresponding commands are also available in the Emacs mode. Support for
251other editors can be added in a relatively straighforward manner by
252using ``idris –client``.
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