7By now, we have seen several examples of how Idris’ dependent type
8system can give extra confidence in a function’s correctness by giving
9a more 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
14are *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
19hole, and even a basic proof search mechanism. In this
20section, we explain how these features can be exploited by a text
21editor, and specifically how to do so in `Vim
22<https://github.com/idris-hackers/idris-vim>`_. An interactive mode
23for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also
29The REPL provides a number of commands, which we will describe
30shortly, which generate new program fragments based on the currently
31loaded module. These take the general form:
35 :command [line number] [name]
37That is, each command acts on a specific source line, at a specific
38name, and outputs a new program fragment. Each command has an
39alternative form, which *updates* the source file in-place:
43 :command! [line number] [name]
45When the REPL is loaded, it also starts a background process which
46accepts and responds to REPL commands, using ``idris --client``. For
47example, if we have a REPL running elsewhere, we can execute commands
52 $ idris --client ':t plus'
53 Prelude.Nat.plus : Nat -> Nat -> Nat
54 $ idris --client '2+2'
57A text editor can take advantage of this, along with the editing
58commands, in order to provide interactive editing support.
66The ``:addclause n f`` command, abbreviated ``:ac n f``, creates a
67template definition for the function named ``f`` declared on line
68``n``. For example, if the code beginning on line 94 contains:
72 vzipWith : (a -> b -> c) ->
73 Vect n a -> Vect n b -> Vect n c
75then ``:ac 94 vzipWith`` will give:
79 vzipWith f xs ys = ?vzipWith_rhs
81The names are chosen according to hints which may be given by a
82programmer, and then made unique by the machine by adding a digit if
83necessary. Hints can be given as follows:
87 %name Vect xs, ys, zs, ws
89This declares that any names generated for types in the ``Vect`` family
90should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.
95The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the
96pattern variable ``x`` on line ``n`` into the various pattern forms it
97may take, removing any cases which are impossible due to unification
98errors. For example, if the code beginning on line 94 is:
102 vzipWith : (a -> b -> c) ->
103 Vect n a -> Vect n b -> Vect n c
104 vzipWith f xs ys = ?vzipWith_rhs
106then ``:cs 96 xs`` will give:
110 vzipWith f [] ys = ?vzipWith_rhs_1
111 vzipWith f (x :: xs) ys = ?vzipWith_rhs_2
113That is, the pattern variable ``xs`` has been split into the two
114possible cases ``[]`` and ``x :: xs``. Again, the names are chosen
115according to the same heuristic. If we update the file (using
116``:cs!``) then case split on ``ys`` on the same line, we get:
120 vzipWith f [] [] = ?vzipWith_rhs_3
122That is, the pattern variable ``ys`` has been split into one case
123``[]``, Idris having noticed that the other possible case ``y ::
124ys`` would lead to a unification error.
129The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the
130clauses which are required to make the function ``f`` on line ``n``
131cover all inputs. For example, if the code beginning on line 94 is:
135 vzipWith : (a -> b -> c) ->
136 Vect n a -> Vect n b -> Vect n c
137 vzipWith f [] [] = ?vzipWith_rhs_1
139then ``:am 96 vzipWith`` gives:
143 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
145That is, it notices that there are no cases for empty vectors,
146generates the required clauses, and eliminates the clauses which would
147lead to unification errors.
152The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to
153find a value for the hole ``f`` on line ``n`` by proof search,
154trying values of local variables, recursive calls and constructors of
155the required family. Optionally, it can take a list of *hints*, which
156are functions it can try applying to solve the hole. For
157example, if the code beginning on line 94 is:
161 vzipWith : (a -> b -> c) ->
162 Vect n a -> Vect n b -> Vect n c
163 vzipWith f [] [] = ?vzipWith_rhs_1
164 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
166then ``:ps 96 vzipWith_rhs_1`` will give
172This works because it is searching for a ``Vect`` of length 0, of
173which the empty vector is the only possibility. Similarly, and perhaps
174surprisingly, there is only one possibility if we try to solve ``:ps
179 f x y :: (vzipWith f xs ys)
181This works because ``vzipWith`` has a precise enough type: The
182resulting vector has to be non-empty (a ``::``); the first element
183must have type ``c`` and the only way to get this is to apply ``f`` to
184``x`` and ``y``; finally, the tail of the vector can only be built
190The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a
191``with`` to a pattern clause. For example, recall ``parity``. If line
196 parity (S k) = ?parity_rhs
198then ``:mw 10 parity`` will give:
202 parity (S k) with (_)
203 parity (S k) | with_pat = ?parity_rhs
205If we then fill in the placeholder ``_`` with ``parity k`` and case
206split on ``with_pat`` using ``:cs 11 with_pat`` we get the following
211 parity (S (plus n n)) | even = ?parity_rhs_1
212 parity (S (S (plus n n))) | odd = ?parity_rhs_2
214Note that case splitting has normalised the patterns here (giving
215``plus`` rather than ``+``). In any case, we see that using
216interactive editing significantly simplifies the implementation of
217dependent pattern matching by showing a programmer exactly what the
220Interactive Editing in Vim
221==========================
223The editor mode for Vim provides syntax highlighting, indentation and
224interactive editing support using the commands described above.
225Interactive editing is achieved using the following editor commands,
226each of which update the buffer directly:
228- ``\d`` adds a template definition for the name declared on the
229 current line (using ``:addclause``).
231- ``\c`` case splits the variable at the cursor (using
234- ``\m`` adds the missing cases for the name at the cursor (using
237- ``\w`` adds a ``with`` clause (using ``:makewith``).
239- ``\o`` invokes a proof search to solve the hole under the
240 cursor (using ``:proofsearch``).
242- ``\p`` invokes a proof search with additional hints to solve the
243 hole under the cursor (using ``:proofsearch``).
245There are also commands to invoke the type checker and evaluator:
247- ``\t`` displays the type of the (globally visible) name under the
248 cursor. In the case of a hole, this displays the context
249 and the expected type.
251- ``\e`` prompts for an expression to evaluate.
253- ``\r`` reloads and type checks the buffer.
255Corresponding commands are also available in the Emacs mode. Support
256for other editors can be added in a relatively straightforward manner
257by using ``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