From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 42E2E7F0BA for ; Mon, 6 Feb 2017 17:46:05 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ivg@ieee.org; spf=Pass smtp.mailfrom=ivg@ieee.org; spf=None smtp.helo=postmaster@mail-it0-f42.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of ivg@ieee.org) identity=pra; client-ip=209.85.214.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of ivg@ieee.org designates 209.85.214.42 as permitted sender) identity=mailfrom; client-ip=209.85.214.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-it0-f42.google.com) identity=helo; client-ip=209.85.214.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="postmaster@mail-it0-f42.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AidaOmRAqiOc82gNnsFANUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSP76o8bcNUDSrc9gkEXOFd2CrakV16yJ7OuxAyRAuc/H6y9SNsQUFlcsso?= =?us-ascii?q?Y/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0Iu?= =?us-ascii?q?frymUqabtcm81viz9pvPeE0IwWPlOfIhZCmx+CnYsMgbhbxIvqAjzhqB9ndBfe?= =?us-ascii?q?VbwSViOF+VjRL9zsqq5pd/8j1NtrQq95gTf7/9evEZU7VeRBshL2cr783qqQKL?= =?us-ascii?q?GQqR6VMdX2gb1B1SDF6Wv1nBQp7tv36i5aJG0y6AMJizFOhsVA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BnAACjp5hYhirWVdFdGQEBAQEBAQEBA?= =?us-ascii?q?QEBBwEBAQEBFAEBAQEBAQEBAQEBBwEBAQEBhAmBCQeDUZwTkAuHOCqEaIEQAoJ?= =?us-ascii?q?HB0MUAQEBAQEBAQEBAQESAQEBCAsLCh0vgjMEARYBBIIWAQEBAwEjBBkBATcBB?= =?us-ascii?q?AsLBAcNKgICIhIBBQEcBhOJZgUIDqJQP4saaIFrOoMIAQEFiBwBAQEBBgEBAQE?= =?us-ascii?q?BARoIEoY6hG+EOoMggl+QQIsrhmiLIYJOjjSRRRQegRUPJ4EfXAg8FwWEGSCCC?= =?us-ascii?q?yI1AYdGgU4BAQE?= X-IPAS-Result: =?us-ascii?q?A0BnAACjp5hYhirWVdFdGQEBAQEBAQEBAQEBBwEBAQEBFAE?= =?us-ascii?q?BAQEBAQEBAQEBBwEBAQEBhAmBCQeDUZwTkAuHOCqEaIEQAoJHB0MUAQEBAQEBA?= =?us-ascii?q?QEBAQESAQEBCAsLCh0vgjMEARYBBIIWAQEBAwEjBBkBATcBBAsLBAcNKgICIhI?= =?us-ascii?q?BBQEcBhOJZgUIDqJQP4saaIFrOoMIAQEFiBwBAQEBBgEBAQEBARoIEoY6hG+EO?= =?us-ascii?q?oMggl+QQIsrhmiLIYJOjjSRRRQegRUPJ4EfXAg8FwWEGSCCCyI1AYdGgU4BAQE?= X-IronPort-AV: E=Sophos;i="5.33,342,1477954800"; d="scan'208,217";a="259076747" Received: from mail-it0-f42.google.com ([209.85.214.42]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 06 Feb 2017 17:46:04 +0100 Received: by mail-it0-f42.google.com with SMTP id c7so58457051itd.1 for ; Mon, 06 Feb 2017 08:46:04 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=ieee-org.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=WHXdb/fCNglho3BAjAC5iWJIfpU/LfhHsl3PfOxPMwI=; b=vgaEuifBkmCzwb2cyUqPN1JBij4srdu0BV++UPhTcs1meWCpjAIOgvwOvcBvMCPds2 C/UTG1wmqBXHhyPFcf5t8NhXbI9R5/zwZLZbtecDxq1fI4jiZBUvslZMbptrlvjR3eUU r05ALwseIc1SK6/3AtANG0X5iL8rfMdmPUTIrVMnNSiMy/NkHGp8EvihxPi7gTz7wCQN HdvX1pJJQfwrcfI6wXMs9oWZJOvGhNaNB+YwsIM7nBaiPiRq4l8TePaA28yDrLW61QmN nEAMfQRySn6f7OqYNBh8O1bq0BGe+vK62+whwcsc4CkByG7GCO1bPT3+ZDqimnCYbkHr HTVA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=WHXdb/fCNglho3BAjAC5iWJIfpU/LfhHsl3PfOxPMwI=; b=UGRiEO09t0AzeXenusStuq+/8yQQ4298vw07bRBVN3EFujbq+VLQbw0xF4xV3sEJDp TTUoFVggcfXThY6xC3oObFCLqYCPiIvsRMfv0jhbpuz53HlLFIJ8jaMwJgdBwsVuS9dr BgHpIt6MEexz2l25rKZG3n7JfblnuIiymIMqQvVFllcgY8uyit/nG1o5bv1f5OPHwGBa gNrHnOpsW7QaTRCtWn4cgrXXdwXMGyfubAs66iD/nInBh2XqhsaHR3tThHH4TYkIBDpj W99tMuOS3brj9vx+hXqpT/LPhIzr4BhTulDOZqFaanOyxzA7QnJ+gods9UMYLEoObPHp QxFA== X-Gm-Message-State: AIkVDXLcmaB5jG1QAk1UnMTs2feTB7H8907tCwXpAZm/2H6RvQaZp2MZ0QzkQbRXAEP5ZY4xaHtpaIbZpZaFhKee X-Received: by 10.36.214.86 with SMTP id o83mr8381225itg.97.1486399562675; Mon, 06 Feb 2017 08:46:02 -0800 (PST) MIME-Version: 1.0 Received: by 10.107.175.130 with HTTP; Mon, 6 Feb 2017 08:46:02 -0800 (PST) In-Reply-To: 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: Ivan Gotovchits Date: Mon, 6 Feb 2017 11:46:02 -0500 Message-ID: To: =?UTF-8?Q?Daniel_B=C3=BCnzli?= Cc: Hendrik Boom , caml-list Content-Type: multipart/alternative; boundary=001a11470b38ed9c1d0547df5d02 Subject: Re: [Caml-list] where are we on the Hoogle for OCaml front? --001a11470b38ed9c1d0547df5d02 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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=C3=BCnzli 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 fu= ll > 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 > > > --001a11470b38ed9c1d0547df5d02 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Well yes, the theory is not required, but it is bette= r to know one=C2=A0:) I provided a link mostly because it is a sort of a ho= mepage for type-isomorphic search. There are links to the CamlLight impleme= ntations (yeah the idea was there for some time) and Haskel. Speaking of mo= dern implementations, Argot [1] is the only example that comes to mind. It = has the isomorphic search=C2=A0and a type manifest search. The search is im= plemented 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 r= ules:

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 buil= d a set of types that are isomorphic to the query (or partition all the typ= es into the isomoprhism groups).=C2=A0


<= div>[1]:=C2=A0http://ocaml.github.io/platform-dev/packages/argot/



On Mon, Feb 6, 2017 at 11:34 AM, Daniel B=C3=BCnzli <dan= iel.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 effectivenes= s of a full type isomorphism search vs a bag of type identifiers with funct= ional position model. Meaningfully limiting the query power to an IR system= is a problem in practice, for space, computational and user interface reas= ons.

D



--001a11470b38ed9c1d0547df5d02--