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 E307580023 for ; Tue, 11 Oct 2016 02:16:44 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@mailhost.math.nagoya-u.ac.jp Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3An/Bj4x/XM0VoJP9uRHKM819IXTAuvvDOBiVQ1KB9?= =?us-ascii?q?2u8cTK2v8tzYMVDF4r011RmSDN+dsKIP0rqG+4nbGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwu?= =?us-ascii?q?d76zQd6Z1pTnn8mJuLTrKz1SgzS8Zb4gZD6Xli728vcsvI15N6wqwQHIqHYbM8?= =?us-ascii?q?5fxGdvOE7B102kvpT41NdZ/i9Ro/Ms8dJbGeW/JvxgDO8QMDNzCGA89cvm/TfH?= =?us-ascii?q?QBeE5nYGGjENkhNZBQWD4hX3QpzxvzG867JV1yyTPMmwRrcxD2eM9aBuHT3hgz?= =?us-ascii?q?4aOiVx32jNkM1/ka8T9B2ovQZ+zJPZSIScKPo4eKrSesITAHcHV80XVTQXUdD0?= =?us-ascii?q?VJcGE+dUZbUQlIL6vVZb6ELmXQQ=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ASAAAXL/xXlwWCBoVdGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBgxEBAQEBAXR8pDaHW45iAR2GAgKCKxEBAQEBAQEBAQE?= =?us-ascii?q?BARIBAQEBAQgWB0iCMgQBFQEEghABAQEDASMEGQMBNQEBAwsLGAICGA4CAiE2B?= =?us-ascii?q?hOINgMPB7NaZ4RJBwKERg0rGYMjAQEBAQEBAQMBAQEBAQEYAQmBB4czgliCR4I?= =?us-ascii?q?Agkw4LIIvhkwHh2x3ihk1jHKDC490iGOEARODfzRrgnyBbWMBhk2BQQEBAQ?= X-IPAS-Result: =?us-ascii?q?A0ASAAAXL/xXlwWCBoVdGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBgxEBAQEBAXR8pDaHW45iAR2GAgKCKxEBAQEBAQEBAQEBARIBAQEBAQgWB?= =?us-ascii?q?0iCMgQBFQEEghABAQEDASMEGQMBNQEBAwsLGAICGA4CAiE2BhOINgMPB7NaZ4R?= =?us-ascii?q?JBwKERg0rGYMjAQEBAQEBAQMBAQEBAQEYAQmBB4czgliCR4IAgkw4LIIvhkwHh?= =?us-ascii?q?2x3ihk1jHKDC490iGOEARODfzRrgnyBbWMBhk2BQQEBAQ?= X-IronPort-AV: E=Sophos;i="5.31,327,1473112800"; d="scan'208";a="196303705" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 11 Oct 2016 02:16:17 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 9465463CE for ; Tue, 11 Oct 2016 09:16:14 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172.math.nagoya-u.ac.jp [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 22E6D4142; Tue, 11 Oct 2016 09:16:14 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=3CbQ+BD5vRKFnlvSyOixSSfDj4M=; b=kLN/4bgk0hx7Y/ya4nh6hmg2TChs x+CW7t+e5BjPv+35V9TU4UqfbraP1cVE/QT099m1jZiROISYXChuzJvMFP0iLmOL JGP8XeDAARmQkPN7Srn6N3keS6mRMi9xwR6f6umfT38a3zO4+BOUYMLzQz6WdyVq zJV1wtOdKQL0dy0= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=HTVfEj6LAst8hhMwdqE+y3/hj5A2Z3qsdiCeHw3ok47OYDlbpktVDvz/hFt4AwsQc5hr3mH/0kbmBQpUlW4VRbFnrCPlVa2qFUFkvv3yEmoJoeFHZDhp20i0synqhwe5ZWazS6x9zFvBw2j7JJ9W1khnUWyvk/0iW+jP44POwiU=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id F3D4710E5; Tue, 11 Oct 2016 09:10:15 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) From: Jacques Garrigue In-Reply-To: Date: Tue, 11 Oct 2016 09:16:16 +0900 Cc: Jeremy Yallop , Andre Nathan , OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: References: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> To: Shayne Fletcher X-Mailer: Apple Mail (2.3124) Subject: Re: [Caml-list] Encoding "links" with the type system On 2016/10/09 06:51, Shayne Fletcher wrote: >=20 > On Fri, Oct 7, 2016 at 1:02 PM, Shayne Fletcher wrote: > 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.) >=20 > =E2=80=8BHow's this? >=20 > module M : S =3D struct > ... > =E2=80=8B > I've hit a problem with my attempt at an implementation actually :( >=20 > The issue is, the program below as written seems to work, but, if the typ= e [_ set] is made abstract in the signature [S], typing breaks. Can somebod= y explain where I'm going wrong? Making a type abstract loses some information (independently of hiding the = precise definition): * its uniqueness (i.e. it could be equal to any other type) * its injectivity (i.e. whether "t1 t =3D t2 t=E2=80=9D implies =E2=80=9Ct1= =3D t2=E2=80=9D) * its contractiveness (i.e. whether =E2=80=9Ct1 t=E2=80=9D might actually b= e equal to to =E2=80=9Ct1=E2=80=9D) All of these properties have an impact of the behavior of type indices of G= ADTs. If you want to use a type as GADT index, it is fine to hide the actual impl= ementation, but it is better to have a visible constructor. For instance, you could define in the interface: type set_impl type _ set =3D private Set of set_impl (* private ensure that the type pa= rameter is invariant *) and in the implementation: type set_impl =3D (string * string) list type _ set =3D Set of set_impl Jacques > module type S =3D sig >=20 > type _ sink > type _ source > type _ set =3D (string * string) list (*Why can't this be abstract?*) > type ('source, 'sink) link >=20 > type ('sink, 'set) accepts=20 >=20 > val mk_sink : string -> 'sink sink > val mk_source : string -> 'source source > val mk_link : 'source source * 'sink sink -> ('source, 'sink) link >=20 > type 'sink fresh_set =3D=20 > | Fresh_set : { > set : 'set set; > accepts : ('sink, 'set) accepts; > } -> 'sink fresh_set >=20 > val create_set : 'sink sink -> 'sink fresh_set >=20 > type ('sink, 'parent) augmented_set =3D > | Augmented_set : { > set : 'set set; > accepts: ('sink, 'set) accepts; > cc : 's. ('s, 'parent) accepts -> ('s, 'set) accepts > } -> ('sink, 'parent) augmented_set >=20 > val insert_link :=20 > ('source, 'sink) link -> > 'parent set ->=20 > ('sink, 'parent) accepts -> > ('source, 'parent) augmented_set >=20 > end >=20 > module M : S =3D struct >=20 > type 'sink sink =3D { name : string } > type 'source source =3D { name : string } >=20 > type 'set set =3D (string * string) list > type ('source, 'sink) link =3D ('source source * 'sink sink) >=20 > let mk_sink (name : string) : 'sink sink =3D {name} > let mk_source (name : string) : 'source source =3D {name} > let mk_link ((source, sink) : 'source source * 'sink sink)=20 > : ('source, 'sink) link =3D (source, sink) >=20 > type ('sink, 'set) accepts =3D=20 > | Accepts : ('sink, 'set) accepts >=20 > type 'sink fresh_set =3D=20 > | Fresh_set : { > set : 'set set; > accepts : ('sink, 'set) accepts;=20 > } -> 'sink fresh_set >=20 > let create_set (s : 'sink sink) : 'sink fresh_set =3D > Fresh_set { set =3D ([] : 'set set);=20 > accepts =3D (Accepts : ('sink, 'set) accepts) } >=20=20=20 > 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 >=20 > let insert_link=20 > (l : ('source, 'sink) link)=20 > (s : 'parent set) > (a : ('sink, 'parent) accepts) : ('source, 'parent) augmented_set = =3D > let {name =3D src} : 'source source =3D fst l in > let {name =3D dst} : 'sink sink =3D snd l in > Augmented_set { > set : 't set =3D (src, dst) :: s; > accepts =3D (Accepts : ('source, 't) accepts); > cc =3D fun (_ : (_, 'parent) accepts) -> (Accepts : (_, 'parent) ac= cepts) > } >=20 > end >=20 > module Test (E : S) =3D struct >=20 > open E >=20 > type t1 and t2 and t3 and t4 >=20 > let snk1 : t1 sink =3D mk_sink "sink1" > let snk2 : t2 sink =3D mk_sink "sink2" > let snk3 : t4 sink =3D mk_sink "sink3" >=20 > let src1 : t2 source =3D mk_source "source1" > let src2 : t3 source =3D mk_source "source2" >=20 > let link1 : (t2, t1) link =3D mk_link (src1, snk1) (*t2 src, t1 sink*) > let link2 : (t3, t1) link =3D mk_link (src2, snk1) (*t3 src, t1 sink*) > let link3 : (t3, t2) link =3D mk_link (src2, snk2) (*t3 src, t2 sink*) > let link4 : (t3, t4) link =3D mk_link (src2, snk3) (*t3 src, t4 sink*) >=20 > let test () =3D=20 >=20 > (*Create a fresh set from a sink of type [t1]*) > let (Fresh_set {set; accepts =3D a} : t1 fresh_set) =3D=20 > create_set snk1 in > (* > - [a] is evidence [set] accepts links with sink type [t1] > *) >=20 > (*Insert a [(t2, t1) link]*) > let Augmented_set=20 > {set =3D set1; accepts =3D a1; cc =3D cc1} =3D=20 > insert_link link1 set a in > (* > - [a1] is evidence [set1] accepts links with sink type [t2] ([t2] is > the source type of [link1]) > - [cc] says that [set1] accepts links with sink types that its > parent [set] does: > - [cc1 a] provides evidence that says that [set1] will accept > [link2] which has sink type [t1] *) >=20 > (*Insert a [(t3, t1)] link*) > let Augmented_set > {set =3D set2; accepts =3D a2; cc =3D cc2} =3D > insert_link link2 set (cc1 a) in > (* > - [a2] says that [set2] accepts links with sink type [t3] ([t3] is > the source type of [link2]) > - [cc2] says that [set2] accepts links with sink types that its > parent does: > - [cc2 a1] provides evidence that says that [set2] will accept > [link3] which has sink type [t2] > *) >=20 > (*Insert a [(t3, t2)] link*) > let (Augmented_set > {set =3D set3; accepts =3D a3; cc =3D cc3} : (t3, _) augmented_se= t) =3D > insert_link link3 set (cc2 a1) in > (* > - [a3] says that [set3] accepts links with sink type [t3] ([t3]is > the source type of [link3]) > - [cc3] says that [set3] accepts links with sink types that its > parent does (that is, any links with sink types [t1], [t2] or [t3= ]) > *) >=20 > (*There is just no way we can get insert [link4] into [set3]. The > is no evidence we can produce that will allow a link with sink > type [t4]. Try the below with any of [a1], [a2], [a3])*) > (* > let (Augmented_set > {set =3D set4; accepts =3D a4; cc =3D cc4} =3D > insert_link link4 set (cc3 a3) : (t3, _) augmented_set) in > *) >=20 > () > end >=20 > let _ =3D let module T =3D Test (M) in T.test ()