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 72BD87ED11 for ; Wed, 21 Sep 2016 21:12:48 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=andre@digirati.com.br; spf=Pass smtp.mailfrom=andre@digirati.com.br; spf=Pass smtp.helo=postmaster@mta113.f1.k8.com.br Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of andre@digirati.com.br) identity=pra; client-ip=187.73.32.185; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="andre@digirati.com.br"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of andre@digirati.com.br designates 187.73.32.185 as permitted sender) identity=mailfrom; client-ip=187.73.32.185; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="andre@digirati.com.br"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@mta113.f1.k8.com.br designates 187.73.32.185 as permitted sender) identity=helo; client-ip=187.73.32.185; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="postmaster@mta113.f1.k8.com.br"; x-conformance=sidf_compatible; x-record-type="v=spf1" IronPort-PHdr: =?us-ascii?q?9a23=3Afs2saxymQFeBXubXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?0ekSIJqq85mqBkHD//Il1AaPBtSBraoewLON6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL2PbrnD61zMOABK3bVMz?= =?us-ascii?q?fbWvXNaIxJ3sj6ibwN76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKK?= =?us-ascii?q?x8zGJsIk+PzV6nvp/jtM0rzyMFsPsk84tEUL7mV6U+V71RSjo8YE4v48i+nB/P?= =?us-ascii?q?VwbHwHIAUmwQ2k5BBQTf4Tn2X5jwqCLmt6x23yzcN9egHuN8Yiir86o+EEygsy?= =?us-ascii?q?wALTNsqGw=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BeAgDj2uJXh7kgSbteGwEBARUBAQEKA?= =?us-ascii?q?QEBAgEBAQEUAQEBAQYBAgEBAQGCfQEBAQEBgR9SuHeCBIgGOhIBAQEBAQEBAQE?= =?us-ascii?q?BARIBAQEKCwkJGS+CMhiCQQQZAQE4XAIiCwIBOwEIAQEXiDKuWWeESQEBBYgjB?= =?us-ascii?q?giIM4doggALLYJajjmFaoVXg0GBdopFTYhtEoEAhQaQYQIkAYJ4AQoBAQFTgXV?= =?us-ascii?q?YhkUBAQE?= X-IPAS-Result: =?us-ascii?q?A0BeAgDj2uJXh7kgSbteGwEBARUBAQEKAQEBAgEBAQEUAQE?= =?us-ascii?q?BAQYBAgEBAQGCfQEBAQEBgR9SuHeCBIgGOhIBAQEBAQEBAQEBARIBAQEKCwkJG?= =?us-ascii?q?S+CMhiCQQQZAQE4XAIiCwIBOwEIAQEXiDKuWWeESQEBBYgjBgiIM4doggALLYJ?= =?us-ascii?q?ajjmFaoVXg0GBdopFTYhtEoEAhQaQYQIkAYJ4AQoBAQFTgXVYhkUBAQE?= X-IronPort-AV: E=Sophos;i="5.30,375,1470693600"; d="asc'?scan'208";a="194215394" Received: from mta113.f1.k8.com.br ([187.73.32.185]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 21 Sep 2016 21:12:46 +0200 Received: from localhost (localhost [127.0.0.1]) by smtpz.f1.k8.com.br (Postfix) with ESMTP id D42AD800C9 for ; Wed, 21 Sep 2016 19:12:40 +0000 (UTC) X-Virus-Scanned: amavisd-new at k8.com.br Received: from smtpz.f1.k8.com.br ([127.0.0.1]) by localhost (mta113.f1.k8.com.br [127.0.0.1]) (amavisd-new, port 10024) with LMTP id WKymi3PEroev for ; Wed, 21 Sep 2016 19:12:38 +0000 (UTC) Received: from [10.200.12.21] (unknown [201.76.188.234]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtpz.f1.k8.com.br (Postfix) with ESMTPSA id 7C7DD800C1 for ; Wed, 21 Sep 2016 19:12:38 +0000 (UTC) X-DKIM: OpenDKIM Filter v2.6.8 smtpz.f1.k8.com.br 7C7DD800C1 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=digirati.com.br; s=default; t=1474485158; bh=earyVSV7wj5W50RcFSWJUBnlA8F5xihRtFWMEW78gzw=; h=To:From:Subject:Date; b=oViRF8gVI09ZB+1hhjbniuEWKTjSe2uc9zXaF3n7UTRKCfw4H9Z/tN05YBebY6VEu HCB/Ryqn13lJcyavWtfIoKxjAiOIv9Wkr9XrhlPPiOSCGNUDFRJqWfx8phdSX/WGpl K00wOKhT9W1uurYGNMG88Ufenu0AzhZusIXFEo2M= To: caml-list@inria.fr From: Andre Nathan Message-ID: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> Date: Wed, 21 Sep 2016 16:12:33 -0300 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="amuODVdJHoHetOTkqkAs6lU594TCGSQRU" Subject: [Caml-list] Encoding "links" with the type system This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --amuODVdJHoHetOTkqkAs6lU594TCGSQRU Content-Type: multipart/mixed; boundary="BPHF1hQOMC3tJBCghEGBLEqVN4U2NqB34"; protected-headers="v1" From: Andre Nathan To: caml-list@inria.fr Message-ID: <86a4a20a-c5de-a3b3-85c0-621f09a56b81@digirati.com.br> Subject: Encoding "links" with the type system --BPHF1hQOMC3tJBCghEGBLEqVN4U2NqB34 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hi 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 =3D struct type 'a t =3D { name : string } let create name =3D { name } end module Sink =3D struct type 'a t =3D { name : string } let create name =3D { name } end module Link =3D struct type ('a, 'b) t =3D '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? I couldn't get past something like module Set =3D struct type _ t =3D | S : 'a Sink.t -> 'a t | L : 'a t * ('b, 'a) Link.t -> ('a * 'b) t let create sink =3D S sink let add_link link set =3D L (set, link) end This allows me to insert the first link: type t1 type t2 type t3 let _ =3D let snk1 : t1 Sink.t =3D Sink.create "sink1" in let set =3D Set.create snk1 in let src1 : t2 Source.t =3D Source.create "source1" in let lnk1 =3D (src1, snk1) in let set1 =3D Set.add_link lnk1 set in ... but now "set1" has type "(t1 * t2) Set.t" and I can't call "add_link" on it anymore: ... let src2 : t3 Source.t =3D Source.create "source2" in let lnk2 =3D (src2, snk1) in let set2 =3D Set.add_link lnk2 set1 in ... which gives me "This expression has type (t1 * t2) Set.t but an expression was expected of type t1 Set.t" when passing "set1" to "add_link". I also tried to come up with a solution using difference lists for the set but hit basically the same problem as above. Any help would be appreciated. Thanks, Andre --BPHF1hQOMC3tJBCghEGBLEqVN4U2NqB34-- --amuODVdJHoHetOTkqkAs6lU594TCGSQRU Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQEcBAEBCAAGBQJX4tulAAoJED4JW1qwFY2cfTIH/1cKpl9VyNx5UmR7IXvnUp5E HdmjI6qUGK5B+yrHTgTyCH6jE7D2l8Zavuz5XblXy/2X0v+VhYMZJoy3Wg0IHPcu Lw+22vIgbW8HO1QetlPVEQMO4lG/HgLWBMHoqLNzX/5zmkEZO+3agBeJxDIpVZiK TixcmcIuBhneMfOBZRSNaYenEF1keXEEVMY8N788E5LILo3+IUO9tdooq9XfiAJH G6uyhgA5aPwGiElOZu+tKTjILHBwNtEuSkTBYd+dK2ASxhgxkoO9/iqAQzuUgl5M dDh/RJnjGn+x3sisjYmx1yJrsLiaYwuaZ66iZY+WdiUWqOh3K46NY1LnO+gxJ9g= =dXHR -----END PGP SIGNATURE----- --amuODVdJHoHetOTkqkAs6lU594TCGSQRU--