From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 80A715D5 for ; Thu, 17 Jan 2019 09:42:44 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208";a="364473112" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 17 Jan 2019 10:42:43 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 1B8918256B; Thu, 17 Jan 2019 10:42:43 +0100 (CET) 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 EA0937FEFC for ; Thu, 17 Jan 2019 10:42:35 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=christopher@gmerlin.de; spf=None smtp.mailfrom=christopher@gmerlin.de; spf=None smtp.helo=postmaster@mout.kundenserver.de IronPort-PHdr: =?us-ascii?q?9a23=3AMNoajxQC49TS5n+u+vjz4OezMdpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6yZRyN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf?= =?us-ascii?q?5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbD?= =?us-ascii?q?VwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlS?= =?us-ascii?q?gHLSY0/m/XhMJukaxVoxCupxJ4zYHbfI6YL/V+cr/HcN4AX2dNQthdWipcCY28?= =?us-ascii?q?dYsPCO8BMP5Goon9vVsOrAC+BRWrBOP3yj9HmGX21rA53OQgFAHG2RIvH8gLsH?= =?us-ascii?q?vOqtX1MroZXOepw6nI1zXDbuhW2Sv66IjQchAuv+uMUKl/ccrU10YvDQfFjlSW?= =?us-ascii?q?qYD/IjyayP0Avm6G5ORuUuKvjnQoqwB3ojW3yccsj5fGhpgRylDF8yV12ps6Ks?= =?us-ascii?q?OgRE91e96kEYdQuD+AO4t3WcMvRXxjtiUiyrAep5K3YTYGxI45yxLBafGLaZWE?= =?us-ascii?q?7xD5WOqMPTt0nHFodbKlixqs7ESs1PfwWtS73VtItCZJj9jBu34L2hfO8MaIUO?= =?us-ascii?q?F98V2k2TuX1wDc9OVEIUcsmKreLJ4h36IwmoAQsUTeGC/5hVv5jKmNdko64Oio?= =?us-ascii?q?9froYq/8qpCBKYB4kgD+MqIwlcyjGek0LBUCU3aB9eiiyrHu/1f1TKhIg/Esj6?= =?us-ascii?q?XVrIjWJcEBqa64Bw9V3Jwj6xG6Dzq+zNsYnWMHLFNeeBKbiIjpI1HOL+7iDfqk?= =?us-ascii?q?jFSslSlkx+rCPr3gBJXBNGXMn6n5cbZn90Fc0BYzzcxY559MFr4OOvfzWkvouN?= =?us-ascii?q?zcDx85KBC0zv38CNR904MeQXiADrWYMKPUq1+I5/ggL/OCZI8P637BLK0u7vvq?= =?us-ascii?q?yHs4gkM1fK+z3JJRZmrrMO5hJhCyYWDtmcsGCWcHpEIMTenvhUeHWDhVLyK5X7?= =?us-ascii?q?g9/S08EIKrF6/MQ423hL2Hmiu2SM4FLltaA0yBRC+7P76PXO0BPXrLc51R1wcc?= =?us-ascii?q?XL3kcLcPkBSntQv00b1id7CG9SgVr5bi0p556r+LzE1gxXlPF82Yllq1YSRshG?= =?us-ascii?q?pRHW052a1lpU17jFuOg/Ah3q5oUOdL7vYMaT8UcJ7Ry+sgUYL3XR/dONSUTlqr?= =?us-ascii?q?RM6rGy88VJQ9zo1Wbg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A/AABkTUBcgAoR49RjHgEGBwaBUggLA?= =?us-ascii?q?YJpgQInhGOTGoIND5dvgXsIBR8MAYRAAoJUGgYGMQgNAQMBAQIBAQEBARMBAQk?= =?us-ascii?q?NCQgnJQyCOiKCbwECAgEnVwsLIRMSD0gZgyOBeQwBCqtdM4ozgm2JUheBf4N1L?= =?us-ascii?q?oM1ghmFEwKiEAmBF4EZhHKDI4dCJGWBAE2HaSuHRY8Yi3aBSAOCCXFPgmwJghs?= =?us-ascii?q?ag36KIT4zgQUBAYosAQE?= X-IPAS-Result: =?us-ascii?q?A0A/AABkTUBcgAoR49RjHgEGBwaBUggLAYJpgQInhGOTGoI?= =?us-ascii?q?ND5dvgXsIBR8MAYRAAoJUGgYGMQgNAQMBAQIBAQEBARMBAQkNCQgnJQyCOiKCb?= =?us-ascii?q?wECAgEnVwsLIRMSD0gZgyOBeQwBCqtdM4ozgm2JUheBf4N1LoM1ghmFEwKiEAm?= =?us-ascii?q?BF4EZhHKDI4dCJGWBAE2HaSuHRY8Yi3aBSAOCCXFPgmwJghsag36KIT4zgQUBA?= =?us-ascii?q?YosAQE?= X-IronPort-AV: E=Sophos;i="5.56,488,1539640800"; d="scan'208";a="292234715" Received: from mout.kundenserver.de ([212.227.17.10]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-GCM-SHA256; 17 Jan 2019 10:42:34 +0100 Received: from mortimer.gmerlin.de ([85.212.147.163]) by mrelayeu.kundenserver.de (mreue108 [212.227.15.183]) with ESMTPSA (Nemesis) id 1N7zNt-1hFoGv093L-0154ai for ; Thu, 17 Jan 2019 10:42:34 +0100 Date: Thu, 17 Jan 2019 10:42:29 +0100 From: Christopher Zimmermann To: caml-list@inria.fr Message-ID: <20190117104229.3afa7d13@mortimer.gmerlin.de> In-Reply-To: <20190113084919.5cfaa055@mortimer.gmerlin.de> References: <20190113084919.5cfaa055@mortimer.gmerlin.de> X-Mailer: Claws Mail 3.17.1 (GTK+ 2.24.32; x86_64-unknown-openbsd6.4) MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; boundary="Sig_/xh/rT2cANQ/gChxM1R+iPBu"; protocol="application/pgp-signature" X-Provags-ID: V03:K1:5mnu1pHip2TsnQejqBxErJ1L6dD/45EKVMxMCBwJ/iwasEEFKXf zDgFyOE5hg5jj9aso9HSS9WR4iHzjqFTyPehWp+GVMJA9NHuJjFmCrWfNtugV8cCWMPaF+R YLbcNvJMaCO/OsIucSmM4Ur1wn6SnvcMUJaQ7jZG6dw7qzoadC2P0TNnx2CThfz7xWhzldw lEFEGmz50B3UWfyNRZ+FQ== X-Spam-Flag: NO X-UI-Out-Filterresults: notjunk:1;V03:K0:WljqKwPMatg=:vILJo5bpIGzyorRxKgyM7V T3bPzXKCd/TXk6rxgKsBMTc2BOqMBGlAylu9o36VhiXgc2Hj/X8XjA2d5WFj746HAFTIqMSiB 7RgnGPJaCQjPnX8hV37xXBDSzMX/rEpCZaj7gyuoyqCf8a0jJbZ+CqDGZnQHO1yapEiFMhJAw +NXN7F12WiwXqrpdELQqE+h26oLzTao2M2SokN23CRTraCfo7Ln1yzQ7wO2w0iswaCMchrIki 4lXO5PFYFcURzwZnwXPGyzy2/n1OreDgV8uUXqFUSpDNYMjAqQetdB+zmjFQUKyVQUv+DtKHk fj5lhngvEZ9RBkzanw6Un0wf3zDNrLlbK/iNADvYYVmEi8XV4SHPZ1GYf6mJbn1p7LZBdWpWp s1eutHCRy5fxh9w80VIb4kDpUINxh1MdfLGfa04qDkGEsXSOZHmLTPJ6xQ9OldzzD4mIvqLwT aWkb2u0Qw+TSSyu3pVWc3qSMnHK8Nd91irldDMFzrdA0cYWnoAPCW3ApXKS1ouWjyy1dKD8k8 +ci0/r5fqM1Wx8QOkaXDyl8NJzH1oByRMc09kTAnUFw8JbN0q78ONsTcOl3Q0zfc2tH9s/4+C 7w/uWMfXIZcrkZ9H61Fr4MNg0T7eMBwLKPzDKkzMLXomMj7Tm83gBFftXn5gJU/k1qkSbrRWP o9uoBh/WL2xJHg3JfJq33yccezM6vX/4ArmxaswTre3H63nUnAIEkZHjf5Q1r4N9FBWABAHZJ Z8w5CeflqxQ+VQJbBa28Tlrblr5qa9E2wP+zSUtd1I+aZU5lEd4xtgLn9xg= Subject: Re: [Caml-list] SOLVED: How to narrow polymorphic variant phantom types Reply-To: Christopher Zimmermann X-Loop: caml-list@inria.fr X-Sequence: 17305 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --Sig_/xh/rT2cANQ/gChxM1R+iPBu Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: quoted-printable It's contravariance (type -'a desc) I was looking for. This is how it can be typed: module Io : sig type 'a perm constraint 'a =3D [< `Read | `Write ] val ro : [ `Read ] perm val rw : [ `Read | `Write ] perm type -'a desc constraint 'a =3D [< `Read | `Write ] val open_file : 'a perm -> string -> 'a desc val dup : ([< `Read | `Write ] as 'a) perm -> 'a desc -> 'a desc val read : [> `Read ] desc -> string val write : [> `Read | `Write ] desc -> string -> unit end On Sun, 13 Jan 2019 08:49:19 +0100 Christopher Zimmermann wrote: > In the following simplified program I'm trying to use phantom > types to express read / write / read_write permissions. > This program fails at runtime in the call to Io.write. > Is it possible to adjust the phantom types so that it fails at > compilation time? > I'd like to express a typing like > val dup : 'a perm -> [< `Read | `Write > 'a] desc -> 'a desc > but a type variable inside the polymorphic variant type is not > allowed. >=20 > module Io : sig > type 'a perm constraint 'a =3D [< `Read | `Write ] > val ro : [ `Read ] perm > val rw : [ `Read | `Write ] perm >=20 > type 'a desc constraint 'a =3D [< `Read | `Write ] >=20 > val open_file : 'a perm -> string -> 'a desc > val dup : 'a perm -> [< `Read | `Write] desc -> 'a desc > val read : [> `Read ] desc -> string > val write : [> `Read | `Write ] desc -> string -> unit > end > =3D struct > type 'a perm =3D [ `Ro | `Rw ] constraint 'a =3D [< `Read | `Write ] > type 'a desc =3D Unix.file_descr constraint 'a =3D [< `Read | `Write ] > let ro : [ `Read ] perm =3D `Ro > let rw : [ `Read | `Write ] perm =3D `Rw >=20 > let open_file perm file =3D > Unix.(openfile > file > [match perm with |`Ro -> O_RDONLY |`Rw -> O_RDWR] > 0o000 > ) > let read desc =3D > let buf =3D Bytes.create 10 in > assert (Unix.read desc buf 0 10 =3D 10); > Bytes.unsafe_to_string buf > let write desc buf =3D > let buf =3D Bytes.unsafe_of_string buf in > assert (Unix.write desc buf 0 (Bytes.length buf) =3D Bytes.length > buf) >=20 > let dup desc =3D Unix.dup ?cloexec:None > end >=20 > let () =3D > let fd_ro =3D Io.(open_file ro "/tmp/test") in > let fd_rw =3D Io.(dup rw fd_ro) in > Io.write fd_rw "Hello, World"; > print_endline (Io.read fd_ro); >=20 >=20 --=20 http://gmerlin.de OpenPGP: http://gmerlin.de/christopher.pub CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1 --Sig_/xh/rT2cANQ/gChxM1R+iPBu Content-Type: application/pgp-signature Content-Description: OpenPGP digital signature -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE+CT73l6XX3KFKq8nJS8PWAcyqzQFAlxATgUACgkQJS8PWAcy qzTbEw/+N//NtnoWXMbjuoDqQ+j7SdSvaxLqfCgkqctQ0ACQ4EK+dWSZZ2Vo258t iAy63e43yC34umJ6USxE/0x4mXo39vzfGROX/b0/JvNzFwNkIiFvGMCnJfwSt9VA pXxsbsB219VHIBUmzenQ62cYiv3P50LsmnX4/Bo+g3uWBcFBbFAxKdL6Npum0zwT /m4Jj3krJQ04uA4dCANBuBYkUxCyOmqOVKIBRcLrYhEbXRl43ri0EPONdZMnNUG/ wwP6khyAX3GbWw2WP1qwBWDIFxfJvYg/I5WYYBxvYG3MOJ7+4YMHOtBwaGFG6NrM tXfYRyeSpt5yFIAMfWE//QZQcRefWAFBU6laolme0kCwhMxghIm5YcZtfycM3Tla 4mwF7jcsuUlyjgIEdx/ZvY0iVBxz83cCM+zclV0OVPQUvTeuztDq8RuZ5LmLFiI8 edvs2RqIAPy85Cf8D4aN95TY/pnoyBjfQDRtsKpoqBRp23KfW8wM6rEoq0fucO35 tmCXgahXvWaylDhxmANcw4lkogIHpMlyM4QC9b//0yiFtZ8X1Yol5wDXi0D7BUGz 2lpcj8kGHwQbgdbJp7eGsnYALgwCdDsSLWmMdUerWG1/T0qaXOQ4W0YSQGWa6nmG 3TruP4FHe45iM1vcuOoeCFFGvF7LqmPaS0TBTnqnrfjktNQOa8g= =kj/v -----END PGP SIGNATURE----- --Sig_/xh/rT2cANQ/gChxM1R+iPBu--