From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 AD3317F029 for ; Fri, 30 Sep 2016 15:55:14 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-it0-f54.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.54 as permitted sender) identity=mailfrom; client-ip=209.85.214.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; 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-it0-f54.google.com) identity=helo; client-ip=209.85.214.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-it0-f54.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ArzjYBx8yc9xYl/9uRHKM819IXTAuvvDOBiVQ1KB9?= =?us-ascii?q?1OMcTK2v8tzYMVDF4r011RmSDN+dsasP1LKempujcFRI2YyGvnEGfc4EfD4+ou?= =?us-ascii?q?JSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1Ek?= =?us-ascii?q?fKKvQ8WN14ye7KObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicu?= =?us-ascii?q?VSwn50dxrIx06vru/5xpNo8jxRtvQ97IYAFPyiJ+VrBYBfWR0gP3o4rOviqRnK?= =?us-ascii?q?S0Pb730QSGg+nhtHAhLM8BC8VZD09CHg4LlTwi6faOL/R6o1VDDq1KxrRQXlkm?= =?us-ascii?q?9TODcz6mDajoprh6JWuh+7jxN6yo/QJoqSMawtLevmYdoGSD8ZDY5qXCtbD9b5?= =?us-ascii?q?NtNXAg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BRAgDQbe5XfzbWVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgxQBAQEBATyBNQeNK5Z/jxGFEoIGhh4CgWAHOBQBAQEBAQEBAQE?= =?us-ascii?q?BARIBAQkLCwkXMYIyBAEVAQSCEQEBAwESEQQZARsdAQMBCwYDAgs3AgIhAQERA?= =?us-ascii?q?QUBHAYTGgEHiBABAw8Ik2mPR4EyPjKLPYFrgl8Fg3IKGScNU4MCAQEBAQEBBAE?= =?us-ascii?q?BAQEBARkCBhCGJ4RVgkeFAYJaAQSZQzWBZYsMgwCBbogdhWeIXYQRgjwTHoERH?= =?us-ascii?q?oNFghYiNIYlgUEBAQE?= X-IPAS-Result: =?us-ascii?q?A0BRAgDQbe5XfzbWVdFdHAEBBAEBCgEBFwEBBAEBCgEBgxQ?= =?us-ascii?q?BAQEBATyBNQeNK5Z/jxGFEoIGhh4CgWAHOBQBAQEBAQEBAQEBARIBAQkLCwkXM?= =?us-ascii?q?YIyBAEVAQSCEQEBAwESEQQZARsdAQMBCwYDAgs3AgIhAQERAQUBHAYTGgEHiBA?= =?us-ascii?q?BAw8Ik2mPR4EyPjKLPYFrgl8Fg3IKGScNU4MCAQEBAQEBBAEBAQEBARkCBhCGJ?= =?us-ascii?q?4RVgkeFAYJaAQSZQzWBZYsMgwCBbogdhWeIXYQRgjwTHoERHoNFghYiNIYlgUE?= =?us-ascii?q?BAQE?= X-IronPort-AV: E=Sophos;i="5.31,272,1473112800"; d="scan'208,217";a="195210428" Received: from mail-it0-f54.google.com ([209.85.214.54]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 30 Sep 2016 15:55:13 +0200 Received: by mail-it0-f54.google.com with SMTP id r192so45591190ita.0 for ; Fri, 30 Sep 2016 06:55:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=ao5ePgWOWKv419TinuKzFFGYiqCYTZ+1BNX1QFkNDs8=; b=TfIuGJBK8tZKzWF9/DS/LPp0k/aXl3zeR9KfHn/RIaT8alx0ffbHLqp0oeDKm6Wyxg 7JPZcihPND9u9U5qitR4Mvgm196ko5wjFly8XSg30YgWfRrJ7wiTuBClc7QnehxVTu1G pHSgLigtejQIOM97IaGNxvfHMKcKqhb8jn6boFMVoybxgvDzXFfWm7v1FSnjLjOiDkSY cmzBC25vChg66Ej/AAXlBhXayTlsb7y+5PenF6itpiOqJbTc6hLWdLHcf/ep1btqS72V b0YA1tpQzwn7xnnB6akvkz7iQj3CA2gmQ5wQBCJsYuJLajR+UM+NsMfp2e6Ynrm99gAC 3drg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=ao5ePgWOWKv419TinuKzFFGYiqCYTZ+1BNX1QFkNDs8=; b=DrZvJtEBXwzsXMjrBWS/DN0IOjwQIasUwOV6gvwW06AXLurJjNjJzrR5SRG8HheTic CniX3JmTIciPh8+uql2HiMi4VXSq5doytvLWoHuBA+d2n4YfDkI7rtF+BoZGOWVGaT0b WV6TCUd8R4UWWlwyD8NkusPUF96B2Zb7dd9dss1AgDAwrapS4JxqgA1GC5Jruf4Nm4ri vtZpIPJPS2WAFyBnMAVVyZnSazNAu2eyZeSwOAD0NrcmO4LR2WFZJKhsxtkVwekv3YIN zDyyt+qHLGXzKl/d3WIm7aJj/1GJ02lff0sYKSujB0OqEBg44Z4fcv6DDhOXubZiv+6c wgwQ== X-Gm-Message-State: AA6/9RkXU2ENveQN16goS7yu5n6RwQ5kVL2R1thjq0gZ4jbt3KySsQ4qAeNgz7BfQIr4YeJ36ye11BJZvAtqIA== X-Received: by 10.107.200.136 with SMTP id y130mr9046853iof.2.1475243712412; Fri, 30 Sep 2016 06:55:12 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.129.219 with HTTP; Fri, 30 Sep 2016 06:54:32 -0700 (PDT) In-Reply-To: <4B4C9521-010D-4FB7-80C0-0F2192D93614@digirati.com.br> References: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> <4B4C9521-010D-4FB7-80C0-0F2192D93614@digirati.com.br> From: Gabriel Scherer Date: Fri, 30 Sep 2016 09:54:32 -0400 Message-ID: To: Andre Nathan Cc: Jeremy Yallop , caml users Content-Type: multipart/alternative; boundary=94eb2c0bf83c6f80cf053db9f197 Subject: Re: [Caml-list] Encoding "links" with the type system --94eb2c0bf83c6f80cf053db9f197 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I came back to this thread thanks to Alan Schmitt's Caml Weekly News. Here is a fairly systematic approach to the problem, contrasting Jeremy's more virtuoso approach. It works well when the whole set is statically defined in the source code, but I'm not sure about more dynamic scenarios (when a lot of the type variables involved become existentially quantified. The idea is to first formulate a solution using logic programming. A link set can be represented as a list of accepted sinks, and I can write a small Prolog program, "insert" that takes a new link, and a link set, and traverses the link set to find the link's sink in the list, and add the link's source to the list in passing. set([sink]) :- link(source, sink). set(sinks) :- set(prev_sinks), link(source, sink), insert(prev_sinks, source, sink, sinks). (* either the sink we want to insert is first in the list *) insert([sink | _], source, sink, [source, sink | sinks]). (* or it is to be found somewhere, recursively, under some other sink [s] *) insert([s | prev_sinks], source, sink, [s | sinks]) :- insert(prev_sinks, source, sink, sinks). Once you have this logic program, it is straightforward to translate it to a GADT declaration: type 's linkset =3D | Init : ('source, 'sink) link -> ('source -> ('sink -> unit)) linkset | Insert : ('source, 'sink) link * 'set1 linkset * ('set1, 'source, 'sink, 'set2) insert -> 'set2 linkset and ('set1, 'source, 'sink, 'set2) insert =3D | Here : (('sink -> _) as 'set1, 'source, 'sink, 'source -> 'set1) insert | Next : ('set1, 'source, 'sink, 'set2) insert -> ('a -> 'set1, 'source, 'sink, 'a -> 'set2) insert let _ =3D fun (type t1 t2 t3) (lnk1 : (t2, t1) link) (lnk2 : (t3, t1) link) (lnk3 : (t3, t2) link) -> let set =3D Init lnk1 in let set =3D Insert (lnk2, set, Next Here) in let set =3D Insert (lnk3, set, Here) in set On Wed, Sep 21, 2016 at 8:50 PM, Andre Nathan wrote: > Em 21 de set de 2016, =C3=A0s 19:22, Jeremy Yallop esc= reveu: > > It is! Here's one approach, which is based on two ideas: > > > Wow, there's a lot to digest here :) Most of it is new to me, including > the use of "evidence" types... I'll have to re-read it and try to work it > out after a night of sleep. > > Thanks, > Andre > > --94eb2c0bf83c6f80cf053db9f197 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I came back to this thread thanks to Alan S= chmitt's Caml Weekly News.

Here is a fairly systematic app= roach to the problem, contrasting Jeremy's more virtuoso approach. It w= orks well when the whole set is statically defined in the source code, but = I'm not sure about more dynamic scenarios (when a lot of the type varia= bles involved become existentially quantified.

The idea is to = first formulate a solution using logic programming. A link set can be repre= sented as a list of accepted sinks, and I can write a small Prolog program,= "insert" that takes a new link, and a link set, and traverses th= e link set to find the link's sink in the list, and add the link's = source to the list in passing.

=C2=A0=C2=A0 set([sink]) :- link(sour= ce, sink).
=C2=A0=C2=A0 set(sinks) :-
=C2=A0=C2=A0=C2=A0=C2=A0 set(pr= ev_sinks),
=C2=A0=C2=A0=C2=A0=C2=A0 link(source, sink),
=C2=A0=C2=A0= =C2=A0=C2=A0 insert(prev_sinks, source, sink, sinks).

=C2=A0= =C2=A0 (* either the sink we want to insert is first in the list *)
=C2=A0=C2=A0 insert([sink | _], source, sink, [source, sink | sinks]).
=
=C2=A0=C2=A0 (* or it is to be found somewhere, recursively,= under some other sink [s] *)
=C2=A0=C2=A0 insert([s | prev_s= inks], source, sink, [s | sinks]) :-
=C2=A0=C2=A0=C2=A0=C2=A0 insert(pre= v_sinks, source, sink, sinks).

Once you have this logic p= rogram, it is straightforward to translate it to a GADT declaration:
type 's linkset =3D
=C2=A0 | Init : ('source, 'sink) link -= > ('source -> ('sink -> unit)) linkset
=C2=A0 | Insert = : ('source, 'sink) link * 'set1 linkset * ('set1, 'sour= ce, 'sink, 'set2) insert -> 'set2 linkset
and ('set1,= 'source, 'sink, 'set2) insert =3D
=C2=A0 | Here : (('si= nk -> _) as 'set1, 'source, 'sink, 'source -> 'se= t1) insert
=C2=A0 | Next : ('set1, 'source, 'sink, 'set2= ) insert -> ('a -> 'set1, 'source, 'sink, 'a ->= ; 'set2) insert

let _ =3D fun (type t1 t2 t3) (lnk1 : (t2, t1) l= ink) (lnk2 : (t3, t1) link) (lnk3 : (t3, t2) link) ->
=C2=A0 let set = =3D Init lnk1 in
=C2=A0 let set =3D Insert (lnk2, set, Next Here) in
= =C2=A0 let set =3D Insert (lnk3, set, Here) in
=C2=A0 set

<= /div>

On Wed, Sep = 21, 2016 at 8:50 PM, Andre Nathan <andre@digirati.com.br> wrote:
Em 21 de set de 2016, =C3=A0s 19:22, Jeremy Yallop <<= a href=3D"mailto:yallop@gmail.com" target=3D"_blank">yallop@gmail.com&g= t; escreveu:
=
=
It is!=C2=A0 Here= 's one approach, which is based on two ideas:

Wow, there's a lot to digest here :) Most of it is new to me, includi= ng the use of "evidence" types... I'll have to re-read it and= try to work it out after a night of sleep.

Thanks,
Andre=C2=A0

<= /div> --94eb2c0bf83c6f80cf053db9f197--