From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id E85A67F72D for ; Mon, 6 Feb 2017 17:55:49 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=frederic.bour@lakaban.net; spf=Pass smtp.mailfrom=frederic.bour@lakaban.net; spf=None smtp.helo=postmaster@mail.lakaban.net Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of frederic.bour@lakaban.net) identity=pra; client-ip=213.251.185.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="frederic.bour@lakaban.net"; x-sender="frederic.bour@lakaban.net"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of frederic.bour@lakaban.net designates 213.251.185.180 as permitted sender) identity=mailfrom; client-ip=213.251.185.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="frederic.bour@lakaban.net"; x-sender="frederic.bour@lakaban.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail.lakaban.net) identity=helo; client-ip=213.251.185.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="frederic.bour@lakaban.net"; x-sender="postmaster@mail.lakaban.net"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AGaAXgRUHScvp+JCXGtS7kfJH+QbV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYbBWAt8tkgFKBZ4jH8fUM07OQ6PG8HzNfqsfc+Fk5M7V0Hycfjs?= =?us-ascii?q?sXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6?= =?us-ascii?q?KfroEYDOkcu3y/qy+5rOaAlUmTaxe71/IRG5oAnLtMQbg4RuJ6IxxxDUvnZGZu?= =?us-ascii?q?NayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnD?= =?us-ascii?q?VhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0ji?= =?us-ascii?q?oMKjg0+3zVhMNtlqJWuA+vqQJxw4DUY4+bOvRxcazfctwGXmdORNpdWjZbD4+g?= =?us-ascii?q?YYYCDewMNvtYoYnnoFsOqAOzCwm2BOT11zBPnGX23awm3O88DAzG2xEgH8gTu3?= =?us-ascii?q?nTotX1LrkdXv2rw6nSzDXMc+la1iz66IjVaBAsuvWMUqhzccXL0kYgDQXFgk+W?= =?us-ascii?q?qYP7IzOYz+IAuHWV4epnUOKgkW8nqwdprzir3MgsiZPGiZkPxVDC7yl5xpg6Jc?= =?us-ascii?q?GgRE50YN6kDJtQtzyBOIdsQ8MiRGdlszs5xL0eoZO3YjUGxZo9yxLBa/GLbpKE?= =?us-ascii?q?7g/gWeuROzt0mXFodK6nixux/kWs0PPwWtW23VpQsCZInNbBumoM2hHT7MWMV+?= =?us-ascii?q?Fz8V272TmV0gDe8uFELl4wlarcM5Mhx6Q/lpsXsUjZGi/5gkb2g7WNeUo+/Oik?= =?us-ascii?q?8eLnbav6ppOENo90jB/xMrg2l8ChHOg1PBICU3ab9OihzrHv4E70TbVQgvErka?= =?us-ascii?q?TVrIjWJcEBqa64Bw9V3Jwj6xG6Dzq+3tQYh2cII09bdxKdjojmJ0vCL+v/Dfei?= =?us-ascii?q?mVShizNryOrFPrL7GZrCNH7DnK3nfblj905Q0BAzwsxH55JIFrEBJ+r+VVPru9?= =?us-ascii?q?zdCh81Kgi0w+f8CNVhzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbS?= =?us-ascii?q?iioykFoZOK2oxoc/aXaiH/0gLV/KT2Drh4IvC+YGPxA/R6TAj0CYGWpdfXu+Ur?= =?us-ascii?q?g97XcxD5+8JYPKRYmnibrH2iqnSM4FLltaA0yBRC+7P76PXO0BPXqf?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BuCABGqZhY/7S5+9VdFgUBAQEDAQEBC?= =?us-ascii?q?QEBARYBAQEDAQEBCQEBAYQJKl+DWIp6kHofl0MqhGiBEAKDERQBAQEBAQEBAQE?= =?us-ascii?q?BAWEoQg6BYxmCHgEFIwQZAQE4DwsYJwMCAkYREwYCAQGJcwquImiBazorgl0BA?= =?us-ascii?q?QWIHQELAR0IiFEIgmKEOoJmDC6CX5trhmiLI4JMh26GRpMMNiF+MihGhDWCDXU?= =?us-ascii?q?BhSCDdAEBAQ?= X-IPAS-Result: =?us-ascii?q?A0BuCABGqZhY/7S5+9VdFgUBAQEDAQEBCQEBARYBAQEDAQE?= =?us-ascii?q?BCQEBAYQJKl+DWIp6kHofl0MqhGiBEAKDERQBAQEBAQEBAQEBAWEoQg6BYxmCH?= =?us-ascii?q?gEFIwQZAQE4DwsYJwMCAkYREwYCAQGJcwquImiBazorgl0BAQWIHQELAR0IiFE?= =?us-ascii?q?IgmKEOoJmDC6CX5trhmiLI4JMh26GRpMMNiF+MihGhDWCDXUBhSCDdAEBAQ?= X-IronPort-AV: E=Sophos;i="5.33,342,1477954800"; d="scan'208,217";a="212235763" Received: from pepper.lakaban.net (HELO mail.lakaban.net) ([213.251.185.180]) by mail3-smtp-sop.national.inria.fr with ESMTP; 06 Feb 2017 17:55:48 +0100 Received: from [30.66.35.214] (unknown [84.207.234.65]) (Authenticated sender: defre@ygg-drasil.fr) by mail.lakaban.net (Postfix) with ESMTPSA id B45BA8A0011 for ; Mon, 6 Feb 2017 16:52:20 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=lakaban.net; s=default; t=1486399940; bh=7py5+hvpgevQsONr4JivP5PDjH0MNeKvtlCHpXqI/kU=; h=Subject:To:References:From:Date:In-Reply-To:From; b=rViEpsXb/GXwz+3a+pgASGYUTSDQdf5t3SoxbMFzcsWm7KucE2EG9i3GMSwc4leKG pcGVF/SJlnAjdAuJbznhtJ/3ySr6PIVbbdymZ0Dxl9MNu6QvsgwNZx8VBR/uwygK6J bdciTT7g/ztIgAUl8Mabxp5udVSQxchBQpccu4KA= To: caml-list@inria.fr References: <20170127142246.919C212146E@mcclellan.cs.miami.edu> <416beaa2-9430-20fe-d8fa-e9f02761378f@vanderbilt.edu> <67BCE44C836B466EBD22FC5CE5A4CD13@erratique.ch> <20170206140253.GA20685@topoi.pooq.com> <047710BD79374AC295A49E129B38B01B@erratique.ch> From: =?UTF-8?B?RnLDqWTDqXJpYyBCb3Vy?= Message-ID: <83522776-37b5-754b-aa01-f05e6af8f56f@lakaban.net> Date: Mon, 6 Feb 2017 16:55:47 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/alternative; boundary="------------60F76A784EF227215716B95C" Subject: Re: [Caml-list] where are we on the Hoogle for OCaml front? This is a multi-part message in MIME format. --------------60F76A784EF227215716B95C Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit 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 > > 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 > > > --------------60F76A784EF227215716B95C Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit

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). 





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




--------------60F76A784EF227215716B95C--