One essential task of programmers it to use the right library and function. But what is the right function? Most developers use their experience and knowledge of the ecosystem to intuit where to look for. Tools like Sherlodoc or Hoogle provide textual search in an ecosystem of functions, easing the quest of the developer.

To go further, Dowsing allow searching OCaml functions by their types: the developer provides a type, and Dowsing finds a function whose type is suitable. More precisely, it finds any functions whose type is more general, up to a set of isomorphisms such as currying or reordering of arguments. Results are guaranteed to be sound (the type does match) and complete (all such functions are found).

Unfortunately such search is costly, relying on “unification modulo isomorphisms” (which is NP-complete). So far, Dowsing relied on database-style indexation techniques and state-of-the-art unification algorithms, enabling search over a set of local libraries, but exhibiting poor performances for very polymorphic queries.

In this article, we present several improvements to unification modulo isomorphism which makes Dowsing up to 500 times faster on complex queries. This brings Dowsing in a new area where it can be used interactively by developers.