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 1EDC07ED11 for ; Thu, 22 Sep 2016 00:22:25 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-qt0-f174.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.216.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of yallop@gmail.com designates 209.85.216.174 as permitted sender) identity=mailfrom; client-ip=209.85.216.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@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-qt0-f174.google.com) identity=helo; client-ip=209.85.216.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-qt0-f174.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AwXEgrhcNEm12qgLoZrYndjk2lGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxc68bB7h7PlgxGXEQZ/co6odzbGH6ea4AidYv96oizMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3Dwdp?= =?us-ascii?q?POO9QteU1JXtkbjpsMWNKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP?= =?us-ascii?q?5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nB/P?= =?us-ascii?q?VwbHwHIAUmwQ2k5BBQTf4Tn2X5jwqCLmt6x23yzcN9egHp4uXjH3zapxRRr5wB?= =?us-ascii?q?YOMzo+6CmDm8V0iKVDiB2krh17hYXTZdfGZ7JFYqrBcIZCFiJ6VcFLWnkEW9vk?= =?us-ascii?q?Yg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DbAACjB+NXhq7YVdFdGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFgEBAQMBAQEJAQEBgxABAQEBAYFxB60Wi1uCBIYeAoFfBzkTAQEBAQE?= =?us-ascii?q?BAQEBAQESAQEBCAsLCRkvgjIEARUBBIIRAQEEEhEEGQEbHQEDDAYFCw0CAiYCA?= =?us-ascii?q?iIBEQEFARwGEwgaiA4BAxeiSIEyPjKLPYFrgl8Fg3wKGScNVIJeAQEBAQYBAQE?= =?us-ascii?q?BARoCBhB2igWEFYMzgloFjjSFaoVXj2KPbIxngjoTHoERHwGDPx+BXD00hQWBQ?= =?us-ascii?q?AEBAQ?= X-IPAS-Result: =?us-ascii?q?A0DbAACjB+NXhq7YVdFdGgEBAQECAQEBAQgBAQEBFgEBAQM?= =?us-ascii?q?BAQEJAQEBgxABAQEBAYFxB60Wi1uCBIYeAoFfBzkTAQEBAQEBAQEBAQESAQEBC?= =?us-ascii?q?AsLCRkvgjIEARUBBIIRAQEEEhEEGQEbHQEDDAYFCw0CAiYCAiIBEQEFARwGEwg?= =?us-ascii?q?aiA4BAxeiSIEyPjKLPYFrgl8Fg3wKGScNVIJeAQEBAQYBAQEBARoCBhB2igWEF?= =?us-ascii?q?YMzgloFjjSFaoVXj2KPbIxngjoTHoERHwGDPx+BXD00hQWBQAEBAQ?= X-IronPort-AV: E=Sophos;i="5.30,375,1470693600"; d="scan'208";a="194225287" Received: from mail-qt0-f174.google.com ([209.85.216.174]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 22 Sep 2016 00:22:23 +0200 Received: by mail-qt0-f174.google.com with SMTP id 93so29943145qtg.2 for ; Wed, 21 Sep 2016 15:22:23 -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=VR71zV9LIS2wYKx1Wirezo5mxH2BUxt00iK9pEn11xQ=; b=MCbZMeut2jCg5y5FoQSASukMRTq/yvNfJALOZZn41flTf1l7CH/AmlHhaLvx8xjf0Y 4nMICNsTqP/hk7Xwzxw1zcTN+fGU8ezn/SCJe8UtMO2EsfHmBol1ItAncvvRVYvNWbu2 Bk87u4lEC7neznV6QG1tPL4fT4A5wSlwbt7gBa7e79JQPs0MZEWbMuKHHnVOS6/1kW6l yHwHbzURj1Uz578pHfn1qgiCSyJwHegpzsvJBFX50TbUIUVDZc6al3ogQV6HD1ZZrU2I 9Vebc8Blnt0hRr9OxQzZlVFNNddTjpjd0xhYlhAgSPYOA6gQsPe38kVXzPV7z+C4ptOl Q36g== 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=VR71zV9LIS2wYKx1Wirezo5mxH2BUxt00iK9pEn11xQ=; b=RqwYx2VAC5lC/X/DZWsp5p+Bet8Yw5sJQ+iwyj74Dc158FOViGb+ccdcl+SM9cXneI sPkBtLzXFIbxwcdVW5qz8B7mr67waIX/sWbAhikG9IlOhfT33ZtXYRhsFlgYLdFDIWcB gTSlrta9IVUXB/H8pckeatAjlpeJHppjXj6283UvUqeo3kCzkxzxz2sqTiySeImoUOsR Y3LQPp0E1qykPl67s/YP95jgyUuSc3FF6eqzObkOsLUR3dqtJISyZrIRnOUjDFjI0/aF AvQJYceIbC3JHPMe6rqRNqa0BsxvKmL5XBSQSuBnxmSJhkD6pNmuoK+YKhT7fzA+Gy/S Uc0A== X-Gm-Message-State: AE9vXwORFA8x+xy7+VGC+18v5PkwGkR2powe7ImsLWt9TvTx53nm1+n8isNRM/YSk4IgykAsq3klzs+py8KVwg== X-Received: by 10.200.38.17 with SMTP id u17mr35317989qtu.150.1474496542322; Wed, 21 Sep 2016 15:22:22 -0700 (PDT) MIME-Version: 1.0 Received: by 10.55.152.199 with HTTP; Wed, 21 Sep 2016 15:22:21 -0700 (PDT) In-Reply-To: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> References: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> From: Jeremy Yallop Date: Wed, 21 Sep 2016 23:22:21 +0100 Message-ID: To: Andre Nathan Cc: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Encoding "links" with the type system Dear Andre, On 21 September 2016 at 20:12, Andre Nathan wrote: > I'm trying to encode links (an example would be directed graph edges) > using the type system. > > The idea is to have types such as > > module Source = struct > type 'a t = { name : string } > let create name = { name } > end > > module Sink = struct > type 'a t = { name : string } > let create name = { name } > end > > module Link = struct > type ('a, 'b) t = 'a Source.t * 'b Sink.t > end > > > and then define a "link set" with the following characteristics: > > * You initialize a link set with a sink; > * You can add links to set such that > * The first link's sink must be of the type of the sink; > * Additional links can have as sink types the original sink type > from the set creation, or the source types of previously added > links. > > In other words, if a set is created from a "t1 Sink.t", the first link > on the set must be of type "t2 Source.t * t1 Sink.t", the second link > can be either "t3 Source.t * t1 Sink.t" or "t3 Source.t * t2 Sink.t" and > so on. > > Is it possible at all to encode such invariants using the type system? It is! Here's one approach, which is based on two ideas: 1. generating a fresh, unique type for each set (the paper "Lightweight Static Capabilities" calls these "type eigenvariables") 2. an encoding of a set as a collection of evidence about membership. 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.) First, we'll need types for the objects in the domain: sources, sinks, sets and links. type _ source and _ sink and _ set and ('source, 'sink) link Besides these we'll also need a type of membership evidence. A value of type '(sink, set) accepts' is evidence that 'set' will accept a link with sink type 'sink': type ('sink, 'set) accepts Then there are two operations on sets: creating a fresh set and adding a link to a set. In both cases the operation returns multiple values, so I'll use records for the return types. Furthermore, both operations create fresh types (since sets have unique types), so I'll use records with existential types. First, here's the type of the result of the create_set operation: type 'sink fresh_set = Fresh_set :{ (* :{ *) set: 't set; accepts: ('sink, 't) accepts; } -> 'sink fresh_set There's a type parameter 'sink, which'll be instantiated with the type of the sink used to create the set, and two fields: 1. 'set' is the new set 2. 'accepts' is evidence that 'set' will accept a link with sink type 'sink' (or, if you like, a capability that will allow us to add such a link) Note that 'sink is a type parameter, since we need to ensure that it is the same as another type in the program (the sink used to create the set), but 't is existential, since we need to ensure that it is distinct from every other type in the program (since it uniquely identifies 'set'). The create_set operation builds a fresh set from a sink: val create_set : 'sink sink -> 'sink fresh_set Next, here's the type of the result of the add_link operation: type ('sink, 'parent) augmented_set = Augmented_set :{ set: 't set; accepts: ('sink, 't) accepts; cc: 's. ('s, 'parent) accepts -> ('s, 't) accepts; } -> ('sink, 'parent) augmented_set This time there are three elements to the result: 1. 'set' is the new set (as before) 2. 'accepts' is evidence that 'set' will accept a link with sink type 'sink' (as before) 3. 'cc' is a capability converter, that turns evidence that the "parent" set will accept a link into evidence that 'set' will accept the same link. (Another of looking at this is that 'augmented_set' bundles the new set up along with evidence that 'sink' is a member and evidence that every member of the parent set is also a member.) (And it's again worth looking at the scope of the type variables: 'sink and 'parent are parameters, since they correspond to the types of inputs to the operation; 't is fresh, and 's is universally-quantified, since the capability converter must work for any piece of evidence involving the parent.) The insert_link operation takes three arguments: the link to insert, the set into which the link is inserted, and evidence that the insertion is acceptable: val insert_link : ('source, 'sink) link -> (* the link *) 't set -> (* the set *) ('sink, 't) accepts -> (* evidence that the set accepts the link *) ('source, 't) augmented_set Here's the interface in action. Let's assume that we have your sinks, sources and links: type t1 and t2 and t3 val snk1 : t1 sink val src1 : t2 source val src2 : t3 source val lnk1 : (t2, t1) link val lnk2 : (t3, t1) link val lnk3 : (t3, t2) link Let's start by building a set from snk1: let Fresh_set { set = set; accepts = a } = create_set snk1 in Now, since 'set' accepts links with sink type 't1' (as attested by 'a') we can insert a new link: let Augmented_set { set = set1; accepts = a1; cc = cc1 } = insert_link lnk1 set a in We now have the following evidence available: 'a' says that 'set' accepts 't1' 'a1' says that 'set1' accepts 't2' 'cc1' says that 'set1' accepts anything that 'set' accepts, and so 'cc1 a' says that set1' accepts 't1' and so we can insert links with sink type either 't1' or 't2' into 'set1': insert_link lnk3 set1 a1 insert_link lnk2 set1 (cc1 a) And, of course, since we can only insert links when we have evidence that the set will accept them, there's no way to perform invalid insertions. One drawback of the above is a possible lack of efficiency, mostly depending on how 'cc' is implemented. In fact, there's also a cost-free approach to capability conversions based on evidence subtyping and private types, but I'll leave it as an exercise for the reader. I hope that helps! Kind regards, Jeremy.