Unification Modulo Isomorphisms between Dependent Types for Type-Based Library Search

Type-based library search allows developers to efficiently find reusable software components by their type signatures, as exemplified by tools like Hoogle. This capability is especially important in interactive theorem provers (ITPs), where reusing existing proofs can greatly accelerate development. Previous type-based library search tools for ITPs, such as SearchIsos and Loogle, support only a subset of desirable search flexibilities, including argument reordering, currying/uncurrying, generalisation, and the inclusion of extra premises. However, none can handle all these flexibilities simultaneously, resulting in missed relevant matches. In this work, we propose a type-based library search method based on equational unification modulo a set of type isomorphisms for dependent product/sum types, enabling all the desired search flexibilities. We present a semi-algorithm for this equational unification and provide a prototype implementation to demonstrate the feasibility of our approach.