Re: [Caml-list] where are we on the Hoogle for OCaml front?

["Frédéric Bour" <frederic.bour@lakaban.net>]

[-- Attachment #1: Type: text/plain, Size: 2453 bytes --]

The experimental version of Merlin implements a similar feature (however 
it looks only in loaded packages, not the whole opam universe).

It is based on names (normalizing type constructors to resolve aliases), 
and uses variance information (types occurring in positive and negative 
positions) to guide the search.

The prototype query language looks like "-int +string" for "string of 
int". You can see a demo here: 
http://alfred.lakaban.net/~def/polarity.webm .


On 06/02/2017 16:46, Ivan Gotovchits wrote:
> 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 <mailto: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
>
>
>


[-- Attachment #2: Type: text/html, Size: 4359 bytes --]