idris-lang/Idris-dev — pull request #1263 by bmsherman (2014-05-29 04:19:17+00:00)
Title: Add type-directed search functionality (like Hoogle)

With some support from @david-christiansen, I have written an algorithm which does a fuzzy type-directed search, like [Hoogle](http://haskell.org/hoogle) does for Haskell. Perhaps it would befit Idris to call the type-directed search *Iris*?

Matching is performed by elaborating types to TT types and then doing hacky unification-like procedures from there.

This system can take account of several types of variations between types:
1. rearrangement of arguments
2. application of arguments (for example, applying `Nat` to `{a : Type} -> _|_ -> a` to get `_|_ -> Nat`)
3. application of (fully "saturated") typeclasses (for example, applying `Show Int` to `Show a => a -> String`to get `Int -> String`)

The second and third modifications can be applied in different ways: to find functions more general than the searched type, and those more specific than the searched type. My scoring function prefers types which are more general than the one searched. Perfect matches get a score of 0, and the score climbs from there.

There is lots more to be done!
- Currently, my handling of typeclasses is very hacky! I'm definitely doing it the wrong way. Additionally, this is hampering me from doing more complicated typeclass transformations, such as transforming between superclasses and subclasses, or handling typeclasses with variable arguments (such as `Functor (Vect n)`).
- The performance characteristics ought to be horrible. For example, `:s a -> b -> c -> d -> e -> f` takes too long, because the type is very flexible, and tries to match itself to other types in oh-so-many ways.
- It would be awesome to have support for "inlining" of datatypes which are not sum types. For example, it would be nice to match `Exists a p -> b` with `(x : a) -> p x -> b`.
- There are other edge cases that I believe I handle improperly...
- I'm sure there are other exciting ideas and transformations that I haven't thought of!

I apologize for the absurdly hideous code! I hope to clean it up soon.

I'd love to get some feedback!

Here are a few examples:
```
Idris> :s List s -> (s -> t) -> List t
List s -> (s -> t) -> List t
Prelude.Applicative.liftA : Applicative f => (a -> b) ->
f a -> f b
Score: 9

Prelude.Functor.map : Functor f => (a -> b) -> f a -> f b
Score: 9
```

```
Idris> :s List Nat -> Nat
List Nat -> Nat
Prelude.List.length : List a -> Nat
Score: 3

believe_me : a -> b
Score: 6

really_believe_me : a -> b
Score: 6

Prelude.Foldable.product : Foldable t => Num a => t a -> a
Score: 14

Prelude.Foldable.sum : Foldable t => Num a => t a -> a
Score: 14
```

```
Idris> :s (a -> Additive) -> List a -> Additive
(a -> Additive) -> List a -> Additive
Prelude.Foldable.concatMap : Foldable t => Monoid m => (a ->
m) ->
t a -> m
Score: 16
```

```
Idris> :s Vect n a
Vect n a
Prelude.Vect.range : Vect n (Fin n)
Score: 9

Prelude.Vect.Nil : Vect 0 a
Score: 10

Prelude.asciiTab : Vect (fromInteger 32) String
Score: 18
```