Use discrimination trees for type search

There is a data structure called a discrimination tree that allows one to compactly store a large number of terms (rose trees) with metavariables and then, given another term with metavariables, efficiently filter the set of contained terms down to a subset that may unify with the given term.

Discrimination trees are, at their core, just tries whose nodes are of type Maybe Node where Node is a type with one nullary constructor for each AST (term) constructor. Adding a term to a discrimination tree involves doing a preorder traversal of the term to get [Either Var Node] and then mapping either (const Nothing) Just and inserting the result into the underlying trie. Querying the discrimination tree involves a backtracking search. The leaves of the trie should have the set of terms whose preorder traversal is equivalent to that path through the trie.

If you hash-cons the discrimination tree, it can take up less space, which would be desirable for an on-disk representation, but may not be worth the effort. If you want to store a discrimination tree on disk, it would probably be wise to use Word32 offsets instead of pointers (or Word16 if the tree is small enough, which it will often be if someone is running the Hoogle indexer on lots of small packages and then combining the indexes). Discrimination trees are really just about filtering a large set of terms to yield a subset that contains the set that unify with some term, so if you have an implementation of unification that handles Haskell constraints, you can easily handle searching with constraints by running the unification algorithm on each term the discrimination tree outputs and throwing out the ones that fail to unify due to unsatisfied constraints.

This problem in general is called term indexing. There are many data structures that can be used for term indexing, and a discrimination tree is one of the simplest. There are other options, like substitution trees, that may be more efficient. You may want to consult the resources below for more details:

• Substitution Tree Indexing
• Handbook of Automated Reasoning: Chapter 26: Term Indexing
  • This is an extremely useful resource.
  • If you need a copy of this, I may be able to help you.
• Discrimination Nets: Improvement and Extension to Bang Graphs
  • Page 28 is the relevant area.

If you implement discrimination trees for Hoogle, please consider putting the result of your efforts as a separate package on Hackage, as there is no package existing for them. I am working on an implementation (permalink) but it may take some time for it to be ready.

Start by reading the linked EqSat/DiscriminationNet.hs implementation and the term-indexing resources, then locate Hoogle’s existing type-search entry point; no Hoogle file or test is named in the issue. Done means integrating a discrimination tree that filters candidate terms for type search and validating the candidates with unification.