idris-lang/Idris-dev — pull request #1333 by bmsherman (2014-06-26 13:13:41+00:00)
Title: Improved performance for :search

I've made a few more changes to :search:
- I now use a special logic for using typeclass instances to prevent the matching process from being potentially unbounded. Previously, it went something like this: say we have a type
```
Ord t => t
```
. If we use the instance
```
Ord a -> Ord b -> Ord (a, b)
```
, then we can possibly specialize this type to
```
(Ord a, Ord b) => (a, b)
```
. Well, we can keep doing this, and soon we have
```
(Ord a1, Ord a2, Ord b1, Ord b2) => ((a1, a2), (b1, b2))
```
and we can keep going forever.

Now, I'll only try using a typeclass instance if it *doesn't* require any new variables. So
```
Ord (a, b) => (a, b)
```
can be *reduced* (I can now really call this reducing) to
```
(Ord a, Ord b) => (a, b)
```
but we can't do the other nonsense above.

- I've broken the matching process more distinctly into phases. First, we match the return type. Then, we match arguments, and finally, we match typeclasses. If we fail at any stage, we don't proceed to try the later stages.

- I now use a priority queue when matching types. The type-matching process is essentially a non-deterministic computation where it tries a bunch of different ways to match types and sees what sticks. Now, I always search outward from the states with the lowest score; it's essentially Dijkstra's algorithm. Additionally, this allows the search to be cutoff once all current states exceed the maximum score that we're willing to return as a result. Due to this change, I've added a dependency on the *fingertree* package.

The actual search *results* shouldn't change very much (there are some minor differences not worth elaborating on). But result of these changes performance-wise is that on my computer, (after admittedly not too much trying), I haven't been able to find a search term that takes more than about a second to execute! For example, previously,
```
(Ord a, Ord b) => (a, b) -> (a, b) -> Bool
```
took maybe 8 seconds for me to run. Now, it's shorter than I can reliably count (almost instant).