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 851777FFE2 for ; Fri, 7 Oct 2016 19:03:15 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=shayne.fletcher.50@gmail.com; spf=Pass smtp.mailfrom=shayne.fletcher.50@gmail.com; spf=None smtp.helo=postmaster@mail-yw0-f169.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of shayne.fletcher.50@gmail.com) identity=pra; client-ip=209.85.161.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shayne.fletcher.50@gmail.com"; x-sender="shayne.fletcher.50@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of shayne.fletcher.50@gmail.com designates 209.85.161.169 as permitted sender) identity=mailfrom; client-ip=209.85.161.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shayne.fletcher.50@gmail.com"; x-sender="shayne.fletcher.50@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-yw0-f169.google.com) identity=helo; client-ip=209.85.161.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shayne.fletcher.50@gmail.com"; x-sender="postmaster@mail-yw0-f169.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AQyWs8h9/UmcHUP9uRHKM819IXTAuvvDOBiVQ1KB9?= =?us-ascii?q?2+ocTK2v8tzYMVDF4r011RmSDN+dsK4P0rKG+4nbGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwu?= =?us-ascii?q?d76zQdKZ1pznn8mJuLTrKz1SgzS8Zb4gZD6Xli728vcsvI15N6wqwQHIqHYbM8?= =?us-ascii?q?5fxGdvOE7B102kvpT41NdZ/i9Ro/Ms8dJbGeW/JvxgDO8QMDNzEW0v6cj6/SjK?= =?us-ascii?q?SQ+I/jNIQ2wSlh1QKwfA5RD+GJz2t32pmPB63XyhPcTnS718dzCv86xrRQWg3D?= =?us-ascii?q?wHPi8//SfZjsFsh6JWulT8/zRwxofVZMeeM/8oLfCVRs8TWWcUBpUZbCdGGI7p?= =?us-ascii?q?KtJXV+c=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BTAQAv1PdXhqmhVdFcHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgxIBAQEBAYFiDweNLJcAjESHaIILhiACgXgHOBQBAQEBAQEBAQE?= =?us-ascii?q?BARIBAQEICwsJGS+CMgQBFQEEghEBAQMBEhEEGQEbHQEDAQsGAwILNwICIQEBE?= =?us-ascii?q?QEFARwGEyKIEwEDDwiVUI9NgTI+MotCgWuCXwWDbQoZJw1TgxEBAQEBAQEEAQE?= =?us-ascii?q?BAQEBGQMGEIsBgkeFBIJbBYEhAY0YixArCAEBgSaLTYMIj3SIY4QUgj0THoERH?= =?us-ascii?q?oNdIIF6IjSGToFBAQEB?= X-IPAS-Result: =?us-ascii?q?A0BTAQAv1PdXhqmhVdFcHAEBBAEBCgEBFwEBBAEBCgEBgxI?= =?us-ascii?q?BAQEBAYFiDweNLJcAjESHaIILhiACgXgHOBQBAQEBAQEBAQEBARIBAQEICwsJG?= =?us-ascii?q?S+CMgQBFQEEghEBAQMBEhEEGQEbHQEDAQsGAwILNwICIQEBEQEFARwGEyKIEwE?= =?us-ascii?q?DDwiVUI9NgTI+MotCgWuCXwWDbQoZJw1TgxEBAQEBAQEEAQEBAQEBGQMGEIsBg?= =?us-ascii?q?keFBIJbBYEhAY0YixArCAEBgSaLTYMIj3SIY4QUgj0THoERHoNdIIF6IjSGToF?= =?us-ascii?q?BAQEB?= X-IronPort-AV: E=Sophos;i="5.31,456,1473112800"; d="scan'208,217";a="196024805" Received: from mail-yw0-f169.google.com ([209.85.161.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 07 Oct 2016 19:03:14 +0200 Received: by mail-yw0-f169.google.com with SMTP id w3so8644965ywg.1 for ; Fri, 07 Oct 2016 10:03:14 -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=BsBLl+4ozNNK7dktXTlbPFxpjgAQWmmvfkNcw4iCa8k=; b=N8LVjokk229woVjrdF6PRlz9H71d/ieVb8Lhzxb2fGDLtc2AwXJoTXjuYr5jQ8EWsr N0Bolmkgr0YXA0tU38CIgJYW8q+xcbQfv4VqWH355y0NxHN5IcuNQIK05OJsDdzWWY4w VmHI9y93k07bMSpmbcX7LymNpzP4XtXvLznMA+SQgSQodP3xjmOz3MvAsFsdwYcRmW27 q8hbg6xhFhIhMgi1l5Igm373Xmm2QOX4U6GxD9VbeI+II5V5k4q9j0E029dNKYFQgASy V/TBIZJZgQjm3LHsiiBryv4fyvXMHJAEHMKlvPHULfAFJ5ZtbvgFIPYTs9rADamnt4Aa MjWg== 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=BsBLl+4ozNNK7dktXTlbPFxpjgAQWmmvfkNcw4iCa8k=; b=CwLmISPevSexdG0ebAnu8q6ujIVNIID3oYfi5g4P2mjs3wfzSiED5Q6AFEP2TlQuEg 0S2VK2tJ5TjmT/JoPkwHtI/0i4mWURRYBgVqD9ZFchCBUQ1Fddt1SKmPhf69v+4VC9Am tquTOpxgKwnO70FIR2n88fHJrHCH5PzTWTqrLBA3qGjyVJAd84j/ztt853yUCSvrkWPM Ql+AoGFKJs/kL+p4QYsCFZxT3Gqn60V4N3kck1hW0AB8dM960WqIipjoff6sfjGf+QPy iJ6OVJTdwWisbhjP1vU2W5XLxKxighGFK1YxkZe54A1trwqfmZIlBdf4jrsoZhu/fjDc r8Hg== X-Gm-Message-State: AA6/9RnQsnR4pToQ/3Zm0lzSTY5fHX+rRuwIVMAtyJpnJW4gQInsewEp+OduFb82PJfbMy2MBm1/R9n4kfSq/A== X-Received: by 10.129.55.211 with SMTP id e202mr16055467ywa.256.1475859793082; Fri, 07 Oct 2016 10:03:13 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.39.202 with HTTP; Fri, 7 Oct 2016 10:02:52 -0700 (PDT) In-Reply-To: References: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> From: Shayne Fletcher Date: Fri, 7 Oct 2016 13:02:52 -0400 Message-ID: To: Jeremy Yallop Cc: Andre Nathan , "caml-list@inria.fr users" Content-Type: multipart/alternative; boundary=001a1143fb7ab47fe9053e49623e Subject: Re: [Caml-list] Encoding "links" with the type system --001a1143fb7ab47fe9053e49623e Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Wed, Sep 21, 2016 at 6:22 PM, Jeremy Yallop wrote: > I'll describe an interface based on these ideas that maintains the > properties you stipulate. I'll leave the problem of building an > implementation that satisfies the interface to you. (In fact, the > interface is the tricky part and the implementation is straightforward > if you can treat all the type parameters as phantom.) > =E2=80=8BHow's this? module M : S =3D struct type _ sink =3D { name : string } type _ source =3D { name : string } type _ set =3D (string * string) list type ('source, 'sink) link =3D ('source source * 'sink sink) type ('sink, 'set) accepts =3D | Accepts : ('sink, 'set) accepts type 'sink fresh_set =3D | Fresh_set : { set : 't set; accepts : ('sink, 't) accepts; } -> 'sink fresh_set let create_set (s : 'sink sink) : 'sink fresh_set =3D Fresh_set { set =3D ([] : 't set); accepts =3D (Accepts : ('sink, 't) accepts) } type ('sink, 'parent) augmented_set =3D | Augmented_set : { set : 't set; accepts: ('sink, 't) accepts; cc : 's. ('s, 'parent) accepts -> ('s, 't) accepts } -> ('sink, 'parent) augmented_set let insert_link (l : ('source, 'sink) link) (s : 't set) (a : ('sink, 't) accepts) : ('source, 't) augmented_set =3D let ({name =3D src}, {name =3D dst}) =3D l in Augmented_set { set : 'tt set =3D (src, dst) :: s; accepts =3D (Accepts : ('source, 'tt) accepts); cc =3D fun (_ : (_, 't) accepts) -> (Accepts : (_, 't) accepts) } end =E2=80=8B =E2=80=8BThis melts my brain Jeremy! :) --=20 Shayne Fletcher --001a1143fb7ab47fe9053e49623e Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

= On Wed, Sep 21, 2016 at 6:22 PM, Jeremy Yallop <yallop@gmail.com> wrote:
I'= ll describe an interface based on these ideas that maintains the
properties you stipulate.=C2=A0 I'll leave the problem of building an implementation that satisfies the interface to you.=C2=A0 (In fact, the
interface is the tricky part and the implementation is straightforward
if you can treat all the type parameters as phantom.)

= =E2=80=8BHow's this?

module M : S =3D struct

=C2=A0 type _ sin= k =3D { name : string }
=C2=A0 type _ source =3D { name : string }
=C2=A0 t= ype _ set =3D (string * string) list
=C2=A0 type ('source, 'sink) l= ink =3D ('source source * 'sink sink)

=C2=A0 type ('sink= , 'set) accepts =3D=C2=A0
=C2=A0 | Accepts : ('sink, 'set) acce= pts

=C2=A0 type 'sink fresh_set =3D=C2=A0
=C2=A0 | Fresh_set : {=
=C2=A0 =C2=A0 set : 't set;
<= font face=3D"tahoma, sans-serif">=C2=A0 =C2=A0 accepts : ('sink, 't= ) accepts;=C2=A0
=C2=A0 =C2=A0 } =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0-> 'sink fresh_set

=C2= =A0 let create_set (s : 'sink sink) : 'sink fresh_set =3D
=C2=A0 = =C2=A0 Fresh_set { set =3D ([] : 't set);=C2=A0
=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 accepts =3D (Accepts : ('sink, '= t) accepts) }
=C2=A0=C2=A0
=C2=A0 type ('sink, 'parent) augmented_s= et =3D
=C2=A0 | Augmented_set : {
= =C2=A0 =C2=A0 set : 't set;
=C2=A0 = =C2=A0 accepts: ('sink, 't) accepts;
=C2=A0 =C2=A0 cc : 's. (&#= 39;s, 'parent) accepts -> ('s, 't) accepts
=C2=A0 } -> (&= #39;sink, 'parent) augmented_set

=C2=A0 let insert_link=C2=A0
=C2= =A0 =C2=A0 =C2=A0 (l : ('source, 'sink) link)=C2=A0
=C2=A0 =C2=A0 = =C2=A0 (s : 't set)
=C2=A0 =C2=A0 =C2=A0 (a : ('sink, 't) accep= ts) =C2=A0: ('source, 't) augmented_set =3D
=C2=A0 =C2=A0 let ({na= me =3D src}, {name =3D dst}) =3D l in
=C2=A0 =C2=A0 Augmented_set {<= /div>
=C2=A0 = =C2=A0 =C2=A0 set : 'tt set =3D (src, dst) :: s;
=C2=A0 =C2=A0 =C2=A0 a= ccepts =3D (Accepts : ('source, 'tt) accepts);
=C2=A0 =C2=A0 =C2=A0= cc =3D fun (_ : (_, 't) accepts) -> (Accepts : (_, 't) accepts)=
=C2=A0 =C2=A0 }

end
= =E2=80=8B
=E2=80=8BThis melts my brain Jeremy! :)

--
Shayne Fletcher
--001a1143fb7ab47fe9053e49623e--