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
19metavariable, 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-emacs>`_ is also
30The REPL provides a number of commands, which we will describe
31shortly, which generate new program fragments based on the currently
32loaded module. These take the general form
36 :command [line number] [name]
38That is, each command acts on a specific source line, at a specific
39name, and outputs a new program fragment. Each command has an
40alternative form, which *updates* the source file in-place:
44 :command! [line number] [name]
46When the REPL is loaded, it also starts a background process which
47accepts and responds to REPL commands, using ``idris --client``. For
48example, if we have a REPL running elsewhere, we can execute commands
53 $ idris --client ':t plus'
54 Prelude.Nat.plus : Nat -> Nat -> Nat
55 $ idris --client '2+2'
58A text editor can take advantage of this, along with the editing
59commands, in order to provide interactive editing support.
67The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a
68template definition for the function named ``f`` declared on line
69``n``. For example, if the code beginning on line 94 contains:
73 vzipWith : (a -> b -> c) ->
74 Vect n a -> Vect n b -> Vect n c
76then ``:ac 94 vzipWith`` will give:
80 vzipWith f xs ys = ?vzipWith_rhs
82The names are chosen according to hints which may be given by a
83programmer, and then made unique by the machine by adding a digit if
84necessary. Hints can be given as follows:
88 %name Vect xs, ys, zs, ws
90This declares that any names generated for types in the ``Vect`` family
91should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.
96The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the
97pattern variable ``x`` on line ``n`` into the various pattern forms it
98may take, removing any cases which are impossible due to unification
99errors. For example, if the code beginning on line 94 is:
103 vzipWith : (a -> b -> c) ->
104 Vect n a -> Vect n b -> Vect n c
105 vzipWith f xs ys = ?vzipWith_rhs
107then ``:cs 96 xs`` will give:
111 vzipWith f [] ys = ?vzipWith_rhs_1
112 vzipWith f (x :: xs) ys = ?vzipWith_rhs_2
114That is, the pattern variable ``xs`` has been split into the two
115possible cases ``[]`` and ``x :: xs``. Again, the names are chosen
116according to the same heuristic. If we update the file (using
117``:cs!``) then case split on ``ys`` on the same line, we get:
121 vzipWith f [] [] = ?vzipWith_rhs_3
123That is, the pattern variable ``ys`` has been split into one case
124``[]``, Idris having noticed that the other possible case ``y ::
125ys`` would lead to a unification error.
130The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the
131clauses which are required to make the function ``f`` on line ``n``
132cover all inputs. For example, if the code beginning on line 94 is
136 vzipWith : (a -> b -> c) ->
137 Vect n a -> Vect n b -> Vect n c
138 vzipWith f [] [] = ?vzipWith_rhs_1
140then ``:am 96 vzipWith`` gives:
144 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
146That is, it notices that there are no cases for non-empty vectors,
147generates the required clauses, and eliminates the clauses which would
148lead to unification errors.
153The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to
154find a value for the metavariable ``f`` on line ``n`` by proof search,
155trying values of local variables, recursive calls and constructors of
156the required family. Optionally, it can take a list of *hints*, which
157are functions it can try applying to solve the metavariable. For
158example, if the code beginning on line 94 is:
162 vzipWith : (a -> b -> c) ->
163 Vect n a -> Vect n b -> Vect n c
164 vzipWith f [] [] = ?vzipWith_rhs_1
165 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
167then ``:ps 96 vzipWith_rhs_1`` will give
173This works because it is searching for a ``Vect`` of length 0, of
174which the empty vector is the only possibiliy. Similarly, and perhaps
175surprisingly, there is only one possibility if we try to solve ``:ps
180 f x y :: (vzipWith f xs ys)
182This works because ``vzipWith`` has a precise enough type: The
183resulting vector has to be non-empty (a ``::``); the first element
184must have type ``c`` and the only way to get this is to apply ``f`` to
185``x`` and ``y``; finally, the tail of the vector can only be built
191The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a
192``with`` to a pattern clause. For example, recall ``parity``. If line
197 parity (S k) = ?parity_rhs
199then ``:mw 10 parity`` will give:
203 parity (S k) with (_)
204 parity (S k) | with_pat = ?parity_rhs
206If we then fill in the placeholder ``_`` with ``parity k`` and case
207split on ``with_pat`` using ``:cs 11 with_pat`` we get the following
212 parity (S (plus n n)) | even = ?parity_rhs_1
213 parity (S (S (plus n n))) | odd = ?parity_rhs_2
215Note that case splitting has normalised the patterns here (giving
216``plus`` rather than ``+``). In any case, we see that using
217interactive editing significantly simplifies the implementation of
218dependent pattern matching by showing a programmer exactly what the
221Interactive Editing in Vim
222==========================
224The editor mode for Vim provides syntax highlighting, indentation and
225interactive editing support using the commands described above.
226Interactive editing is achieved using the following editor commands,
227each of which update the buffer directly:
229- ``\d`` adds a template definition for the name declared on the
230 current line (using ``:addclause``).
232- ``\c`` case splits the variable at the cursor (using
235- ``\m`` adds the missing cases for the name at the cursor (using
238- ``\w`` adds a ``with`` clause (using ``:makewith``).
240- ``\o`` invokes a proof search to solve the metavariable under the
241 cursor (using ``:proofsearch``).
243- ``\p`` invokes a proof search with additional hints to solve the
244 metavariable under the cursor (using ``:proofsearch``).
246There are also commands to invoke the type checker and evaluator:
248- ``\t`` displays the type of the (globally visible) name under the
249 cursor. In the case of a metavariable, this displays the context
250 and the expected type.
252- ``\e`` prompts for an expression to evaluate.
254- ``\r`` reloads and type checks the buffer.
256Corresponding commands are also available in the Emacs mode. Support
257for other editors can be added in a relatively straighforward manner
258by 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