Now I get on to the fun bit, how to do type search. I've done type search in three entirely separate ways:
- Hoogle 1: Alpha conversion with missing arguments
- Hoogle 2: Unification
- Hoogle 3: Edit distance
Of course, it wouldn't be a new version of Hoogle if I didn't have a new way to perform type searches :) The new type searches are based on six operations, the idea is that you start with a target type (what the user queried for), and transform the type into the source type (from the source code). Each transformation has a cost associated with it, and can be run in both directions. I finalised the six tranformation steps some time ago, and they have been floating around on my desk as a piece of paper - not a safe place for paper to live. As such, I've decided to write them up there, in the hope that Google won't loose them.
Each operation has an associated symbol, I've included these symbols in \tex as as well Unicode.
Alpha conversion \alpha (α): a --> b. The standard lambda calculus rule, but this time alpha conversion is not free.
Unboxing \box (□) : m a --> a. Given something in a box, take it out. For example Maybe a --> a would be an example.
Restriction (!): M --> a. Given something concrete like Bool, turn it into a free variable.
Aliasing (=): a --> alias(a). This makes use of the type keyword in Haskell, for example String --> [Char], because type String = [Char].
Context \Rightarrow (⇒): C a => a --> a. Drops the context on a variable, i.e. Eq a => a --> a.
Membership \in (∈): C M => M --> C a => a. For example, Bool --> Eq a => a.
There are some additional restrictions, and methods for applying these rules, but these are the core of the system.