@@ -0,0 +1,336 @@
1+*********************************
2+Type Directed Search ``:search``
3+*********************************
5+Idris' ``:search`` command searches for terms according to their
6+approximate 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.
27+The best results are listed first. As we can see, ``(::)`` and
28+``intersperse`` are exact matches; the ``=`` symbol to the left of those
29+results tells us the types of ``(::)`` and ``intersperse`` are
30+effectively the same as the type that was searched.
32+The next result is ``delete``, whose type is more specific than the type
33+that was searched; that's indicated by the ``>`` symbol. If we had a
34+function with the signature ``e -> List e -> List e``, we could have
35+given it the type ``Eq a => a -> List a -> List a``, but not necessarily
38+The final two results, ``assert_smaller`` and ``const``, have types more
39+general than the type that was searched, and so they have ``<`` symbols
40+to their left. For example, ``e -> List e -> List e`` would be a valid
41+type for ``assert_smaller``. The correspondence for ``const`` is more
42+complicated than any of the four previous results. ``:search`` shows
43+this result because we could change the order of the arguments! That is,
44+the following definition would be legal:
48+ f : e -> List e -> List e
54+:search's functionality is based on the notion of type isomorphism.
55+Informally, two types are isomorphic if we can identify terms of one
56+type exactly with terms of the other. For example, we can consider the
57+types ``Nat -> a -> List a`` and ``a -> Nat -> List a`` to be
58+isomorphic, 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``.
62+With :search, we create a partial order on types; that is, given two
63+types ``A`` and ``B``, we may choose to say that ``A <= B``, ``A >= B``,
64+or both (in which case we say ``A == B``), or neither. For :search, we
65+say that ``A >= B`` if all of the terms inhabiting ``A`` correspond to
66+terms of ``B``, but it need not necessarily be the case that *all* the
67+terms of ``B`` correspond to terms of ``A``. Here's an example:
73+The left-hand type has just a single inhabitant, ``id``, which
74+corresponds to the term ``id {a = Nat}``, which has the right-hand type.
75+However, there are various terms inhabiting the right-hand type (such as
76+``S``) which cannot correspond with terms of type ``a -> a``.
78+We can consider the partial order for ``:search`` to be, in some sense,
79+inductively generated by several classes of "edits" which are described
85+Here is a simple approximate list of the edits that are possible in
86+``:search``. They are not entirely formal, and do not necessarily
87+reflect the ``:search`` command's actual behavior. For example, the
88+*argument application* rule may be used directly on arguments that are
89+bound 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
108+Note that in order for it to make sense to change the order of
109+arguments, neither of the arguments' types may depend on the value bound
110+by 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)
130+Note that this rule means that we can flip equalities anywhere they
131+occur (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
147+ a -> a >= Nat -> Nat
148+ a -> a >= List e -> List e
149+ Vect k (Fin k) >= Vect 5 (Fin 5)
151+Note that the ``n`` shown in the scheme above may be 0; that is, there
152+are no Pi terms to be added on the right side. For example, that's the
153+case for the first example shown above. This is probably the most
154+important, 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
175+This rule is used by looking at the instances for a particular type
176+class. While the scheme is shown only for single-parameter type classes,
177+it naturally generalizes to multi-parameter type classes. This rule is
178+particularly useful in conjunction with argument application. Again,
179+note 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
197+Scoring and listing search results
198+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
200+When a type ``S`` is searched, the type is compared against the types of
201+all of the terms which are currently in context. When :search compares
202+two types ``S`` and ``T``, it essentially tries to find a chain of
208+ S <= A1 <= ... <= An <= T
210+using the edit rules listed above. It also tries to find chains going
211+the other way (i.e., showing ``S >= T``) as well. Each rule has an
212+associated score which indicates how drastic of a change the rule
213+corresponds to. These scores are listed above. Note that for the rules
214+which are not symmetric, the score depends on the direction in which the
215+rule is used. Finding types which are more general that the searched
216+typed (``S <= T``) is preferred to finding types which are less general.
218+The score for the entire chain is, at minimum, the sum of the scores of
219+the individual rules (some non-linear interactions may be added). The
220+:search function tries to find the chain between ``S`` and ``T`` which
221+results in the lowest score, and this is the score associated to the
222+search result for ``T``.
224+Search results are listed in order of ascending score. The symbol which
225+is shown along with the search result reflects the type of the chain
226+which resulted in the minimum score.
228+Implementation of :search
229+-------------------------
231+Practically, naive and undirected application of the rules enumerated
232+above is not possible; not only is this obviously inefficient, but the
233+two application rules (particularly *argument application*) are really
234+impossible to use without context given by other types. Therefore, we
235+use a heuristic algorithm that is meant to be practical, though it might
236+not find ways to relate two types which may actually be related by the
239+Suppose we wish to match two types, ``S`` and ``T``. We think of the
240+problem as a non-deterministic state machine. There is a ``State``
241+datatype 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
253+A function ``nextSteps : State -> [State]`` finds the next states which
254+may follow from a given state. Some states, where everything has been
255+matched, are considered final. The algorithm can be roughly broken down
256+into multiple stages; if we start from having two types, ``S`` and
257+``T``, which we wish to match, they are as follows:
259+1. 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.
264+2. 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*).
268+3. 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
278+4. 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.
288+5. 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.
295+6. 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
301+7. 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.
307+The code for :search is located in the `Idris.TypeSearch
308+module <https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/TypeSearch.hs>`__.
313+The search for chains of rules/edits which relate two types can be
314+viewed as a shortest path problem where nodes correspond to types and
315+edges correspond to rules relating two types. The weights or distances
316+on each edge correspond to the score of each rule. We then may imagine
317+that we have a single start node, our search type ``S``, and several
318+final nodes: all of the types for terms which are currently in context.
319+The problem, then, is to find the shortest paths (where they exist) to
320+all of the final nodes. In particular, we wish to find the "closest"
321+types (those with the minimum score) first, as we'd like to display them
324+This problem nicely maps to usage of Dijkstra's algorithm. We search for
325+all types simultaneously so we can find the closest ones with the
326+minimum amount of work. In practice, this results in using a priority
327+queue of priority queues. We first ask "which goal type should we work
328+on next?", and then ask "which state should we expand upon next?" By
329+using this strategy, the best results can be shown quickly, even if it
330+takes a bit of time to find worse results (or at least rule them out).
335+Whether arguments are explicit or implicit does not affect search