Well yes, the theory is not required, but it is better to know one :) I provided a link mostly because it is a sort of a homepage for type-isomorphic search. There are links to the CamlLight implementations (yeah the idea was there for some time) and Haskel. Speaking of modern implementations, Argot [1] is the only example that comes to mind. It has the isomorphic search and a type manifest search. The search is implemented mostly in Javascript (generated from OCaml). (Probably, you heard the story that it is broken and abandoned, and yadda yadda...)

The digest of the theory, is that we have the following rules:

1. a -> b -> c ~ b -> a -> c
2. a * b -> c ~ a -> b -> c
3. unit -> a ~ a

And by applying these rules recursively we can build a set of types that are isomorphic to the query (or partition all the types into the isomoprhism groups). 


[1]: http://ocaml.github.io/platform-dev/packages/argot/



On Mon, Feb 6, 2017 at 11:34 AM, Daniel Bünzli <daniel.buenzli@erratique.ch> wrote:
On Monday, 6 February 2017 at 17:07, Ivan Gotovchits wrote:
> That's why the search should be up-to some isomorphism, e.g.,
>
> int -> float -> bool
>
>
> is isomoprhic to
>
> float -> int -> bool

The papers you mention seem to be about the type ismorophism theory but I can't see any that tries to asses end-user information needs and retrieval evaluation. I'm not sure you need the full theory to build an effective system to support a programmer, e.g. what about the effectiveness of a full type isomorphism search vs a bag of type identifiers with functional position model. Meaningfully limiting the query power to an IR system is a problem in practice, for space, computational and user interface reasons.

D