1*********************************
2Type Directed Search ``:search``
3*********************************
5Idris' ``:search`` command searches for terms according to their
6approximate type signature (much like
7`Hoogle <http://www.haskell.org/hoogle/>`__ for Haskell). For
10 Idris> :search e -> List e -> List e
11 = Prelude.List.(::) : a -> List a -> List a
14 = Prelude.List.intersperse : a -> List a -> List a
15 Insert some separator between the elements of a list.
17 > Prelude.List.delete : Eq a => a -> List a -> List a
20 < assert_smaller : a -> b -> b
21 Assert to the totality checker than y is always structurally
22 smaller than x (which is typically a pattern argument)
24 < Prelude.Basics.const : a -> b -> a
25 Constant function. Ignores its second argument.
27The best results are listed first. As we can see, ``(::)`` and
28``intersperse`` are exact matches; the ``=`` symbol to the left of those
29results tells us the types of ``(::)`` and ``intersperse`` are
30effectively the same as the type that was searched.
32The next result is ``delete``, whose type is more specific than the type
33that was searched; that's indicated by the ``>`` symbol. If we had a
34function with the signature ``e -> List e -> List e``, we could have
35given it the type ``Eq a => a -> List a -> List a``, but not necessarily
38The final two results, ``assert_smaller`` and ``const``, have types more
39general than the type that was searched, and so they have ``<`` symbols
40to their left. For example, ``e -> List e -> List e`` would be a valid
41type for ``assert_smaller``. The correspondence for ``const`` is more
42complicated than any of the four previous results. ``:search`` shows
43this result because we could change the order of the arguments! That is,
44the following definition would be legal:
48 f : e -> List e -> List e
54:search's functionality is based on the notion of type isomorphism.
55Informally, two types are isomorphic if we can identify terms of one
56type exactly with terms of the other. For example, we can consider the
57types ``Nat -> a -> List a`` and ``a -> Nat -> List a`` to be
58isomorphic, because if we have ``f : Nat -> a -> List a``, then
59``flip f : a -> Nat -> List a``. Similarly, if
60``g : a -> Nat -> List a``, then ``flip g : Nat -> a -> List a``.
62With :search, we create a partial order on types; that is, given two
63types ``A`` and ``B``, we may choose to say that ``A <= B``, ``A >= B``,
64or both (in which case we say ``A == B``), or neither. For :search, we
65say that ``A >= B`` if all of the terms inhabiting ``A`` correspond to
66terms of ``B``, but it need not necessarily be the case that *all* the
67terms of ``B`` correspond to terms of ``A``. Here's an example:
73The left-hand type has just a single inhabitant, ``id``, which
74corresponds to the term ``id {a = Nat}``, which has the right-hand type.
75However, there are various terms inhabiting the right-hand type (such as
76``S``) which cannot correspond with terms of type ``a -> a``.
78We can consider the partial order for ``:search`` to be, in some sense,
79inductively generated by several classes of "edits" which are described
85Here is a simple approximate list of the edits that are possible in
86``:search``. They are not entirely formal, and do not necessarily
87reflect the ``:search`` command's actual behavior. For example, the
88*argument application* rule may be used directly on arguments that are
89bound after other arguments, without using several applications of the
90*argument transposition* rule.
92- **Argument transposition**
96 A : Type B : Type a : A, b : B |- M : Type
97 ----------------------------------------------------------------------------
98 (x : A) -> (y : B) -> [x,y/a,b]M == (y : B) -> (x : A) -> [x,y/a,b]M
106 a -> Vect n a -> Vect (S n) a == Vect n a -> a -> Vect (S n) a
108Note that in order for it to make sense to change the order of
109arguments, neither of the arguments' types may depend on the value bound
110by the other argument!
112- **Symmetry of equality**
116 A = B : Type t : Type |- M : Type
117 ----------------------------------------
118 [A = B/t]M == [B = A/t]M
126 (x,y,z : Nat) -> x + (y + z) = (x + y) + z
128 (x,y,z : Nat) -> (x + y) + z = x + (y + z)
130Note that this rule means that we can flip equalities anywhere they
131occur (i.e., not only in the return type).
133- **Argument application**
137 e : A |- M : Type y1 : T1, ..., yn : Tn |- x : A
138 -----------------------------------------------------------------
139 (z : A) -> [z/e]M >= (y1 : T1) -> ... -> (yn :Tn) -> [x/e]M
141 Score: <= : 3 points, >= : 9 points
148 a -> a >= List e -> List e
149 Vect k (Fin k) >= Vect 5 (Fin 5)
151Note that the ``n`` shown in the scheme above may be 0; that is, there
152are no Pi terms to be added on the right side. For example, that's the
153case for the first example shown above. This is probably the most
154important, and most widely used, rule of all.
156- **Type class application**
160 C : Type -> TypeClass
161 , y1 : T1, ..., yn : Tn |- A : Type, instance : C A
162 , t : Type |- M : Type
163 -----------------------------------------------------------------
164 C a => [a/t]M >= (y1 : T1) -> ... -> (yn : Tn) -> [A/t]M
166 Score: <= : 4 points, >= : 12 points
173 Show (List e) => List e -> String >= Show a => List a -> String
175This rule is used by looking at the instances for a particular type
176class. While the scheme is shown only for single-parameter type classes,
177it naturally generalizes to multi-parameter type classes. This rule is
178particularly useful in conjunction with argument application. Again,
179note that the ``n`` in the scheme above may be 0.
181- **Type class introduction**
185 t : Type |- M : Type C : Type -> TypeClass
186 -----------------------------------------------
187 (t : Type) -> M >= C t => M
189 Score: <= : 2 points, >= : 6 points
195 a -> a -> Bool >= Eq a => a -> a -> Bool
197Scoring and listing search results
198~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
200When a type ``S`` is searched, the type is compared against the types of
201all of the terms which are currently in context. When :search compares
202two types ``S`` and ``T``, it essentially tries to find a chain of
208 S <= A1 <= ... <= An <= T
210using the edit rules listed above. It also tries to find chains going
211the other way (i.e., showing ``S >= T``) as well. Each rule has an
212associated score which indicates how drastic of a change the rule
213corresponds to. These scores are listed above. Note that for the rules
214which are not symmetric, the score depends on the direction in which the
215rule is used. Finding types which are more general that the searched
216typed (``S <= T``) is preferred to finding types which are less general.
218The score for the entire chain is, at minimum, the sum of the scores of
219the individual rules (some non-linear interactions may be added). The
220:search function tries to find the chain between ``S`` and ``T`` which
221results in the lowest score, and this is the score associated to the
222search result for ``T``.
224Search results are listed in order of ascending score. The symbol which
225is shown along with the search result reflects the type of the chain
226which resulted in the minimum score.
228Implementation of :search
229-------------------------
231Practically, naive and undirected application of the rules enumerated
232above is not possible; not only is this obviously inefficient, but the
233two application rules (particularly *argument application*) are really
234impossible to use without context given by other types. Therefore, we
235use a heuristic algorithm that is meant to be practical, though it might
236not find ways to relate two types which may actually be related by the
239Suppose we wish to match two types, ``S`` and ``T``. We think of the
240problem as a non-deterministic state machine. There is a ``State``
241datatype which keeps track of how well we've matched ``S`` and ``T`` so
244- Names of argument variables (Pi-bound variables) in either type which
245 have yet to be matched
246- A directed acyclic graph (DAG) of arguments (Pi-bindings) for ``S``
247 and ``T`` which have yet to be matched
248- A list of typeclass constraints for ``S`` and ``T`` which have yet to
250- A record of the rules which have been used so far to get to this
253A function ``nextSteps : State -> [State]`` finds the next states which
254may follow from a given state. Some states, where everything has been
255matched, are considered final. The algorithm can be roughly broken down
256into multiple stages; if we start from having two types, ``S`` and
257``T``, which we wish to match, they are as follows:
2591. For each of ``S`` and ``T``, split the types up into their return
260 types and directed acyclic graphs of the arguments, where there is an
261 edge from argument A to argument B if the term bound in A appears in
262 the type of B. The topological sorts of the DAG represent all the
263 possible ways in which the arguments may be permuted.
2642. For type ``T``, recursively find (saturated) uses of the ``=`` type
265 constructor and produce a list of modified versions of ``T``
266 containing all possible flips of the ``=`` constructor (this
267 corresponds to the *symmetry of equality rule*).
2683. For each modified type for ``T``, try to unify the return type of the
269 modified ``T`` with ``S``, considering arguments from both ``S`` and
270 ``T`` to be holes, so that the unifier may match pieces of the two
271 types. For each modified version of ``T`` where this succeeds, an
272 initial ``State`` can be made. The arguments and typeclasses are
273 updated accordingly with the results of unification. The remainder of
274 the algorithm involves applying ``nextSteps`` to these states until
275 either no states remain (corresponding to no path from ``S`` to
276 ``T``) or a final state is found. ``nextSteps`` also has several
2784. Try to unify arguments of ``S`` with arguments of ``T``, much like is
279 done with the return types. We work "backwards" through the
280 arguments: we try matching all remaining arguments of ``S`` which
281 lack outgoing edges in the DAG of remaining arguments (that is, the
282 bound value doesn't appear in the type of any other remaining
283 arguments) with the all of the corresponding remaining arguments of
284 ``T``. This is done recursively until no arguments remain for both
285 ``S`` and ``T``; otherwise, we give up at this point. This step
286 corresponds to application of the *argument application rule*, as
287 well as the *argument transposition* rule.
2885. Now, we try to match the type classes. First, we take all possible
289 subsets of type class constraints for ``S`` and ``T``. So if ``S``
290 and ``T`` have a total of ``n`` type class constraints, this produces
291 ``2^n`` states for every state, and this quickly becomes infeasible
292 as ``n`` grows large. This is probably the biggest bottleneck of the
293 algorithm at the moment. This step corresponds to applications of the
294 *type class introduction* rule.
2956. Try to match type class constraints for ``S`` with those for ``T``.
296 We attempt to unify each type class constraint for ``S`` with each
297 constraint for ``T``. This may result in applications of the *type
298 class application* rule. Once we are unable to match any more type
299 class constraints between ``S`` and ``T``, we proceed to the final
3017. Try instantiating type classes with their instances (in either ``S``
302 or ``T``). This corresponds to applications of the *type class
303 application* rule. After instantiating a type class, we hopefully
304 open up more opportunities to match typeclass constraints of ``S``
305 with those of ``T``, so we return to the previous step.
307The code for :search is located in the `Idris.TypeSearch
308module <https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/TypeSearch.hs>`__.
313The search for chains of rules/edits which relate two types can be
314viewed as a shortest path problem where nodes correspond to types and
315edges correspond to rules relating two types. The weights or distances
316on each edge correspond to the score of each rule. We then may imagine
317that we have a single start node, our search type ``S``, and several
318final nodes: all of the types for terms which are currently in context.
319The problem, then, is to find the shortest paths (where they exist) to
320all of the final nodes. In particular, we wish to find the "closest"
321types (those with the minimum score) first, as we'd like to display them
324This problem nicely maps to usage of Dijkstra's algorithm. We search for
325all types simultaneously so we can find the closest ones with the
326minimum amount of work. In practice, this results in using a priority
327queue of priority queues. We first ask "which goal type should we work
328on next?", and then ask "which state should we expand upon next?" By
329using this strategy, the best results can be shown quickly, even if it
330takes a bit of time to find worse results (or at least rule them out).
335Whether arguments are explicit or implicit does not affect search
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