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 A72267ED11 for ; Mon, 19 Sep 2016 10:58:33 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=octa@polychoron.fr; spf=None smtp.mailfrom=octa@polychoron.fr; spf=None smtp.helo=postmaster@relay3-d.mail.gandi.net Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=pra; client-ip=217.70.183.195; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=mailfrom; client-ip=217.70.183.195; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@relay3-d.mail.gandi.net) identity=helo; client-ip=217.70.183.195; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="postmaster@relay3-d.mail.gandi.net"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AiAC3yBOecm65G37E+isl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0KPj/rarrMEGX3/hxlliBBdydsKMdzbqK++C4ACpbsM7H6ChDOLV3FDY9wf?= =?us-ascii?q?0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5?= =?us-ascii?q?K6zPF5LIiIzvjqbpqsSVM1kAxGLkJ+gjdFPu9USZn/JVqLMqErw2xBrNrykAUM?= =?us-ascii?q?Vt7kQsG2iumQ3h7Ny75p9p/ncYkfsg88ldTfeyJPxgHvQLRAghZms84cmusRjY?= =?us-ascii?q?USOO4GEdWyMYiElmGQ/AuRbxQp76sjH9sKIp3yKGNOXuSrQlUjSl9aBtDhHy3n?= =?us-ascii?q?RUfwUl+X3a35QjxJlQpwis8kRy?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DNAAB7p99XhsO3RtlcRwEBFgEBBQEBg?= =?us-ascii?q?wIBAQEBAYEfWbhsggOGHgKBQzgUAQEBAQEBAQEBAQESAQEBCgkLCRkvgjIYghg?= =?us-ascii?q?BAQMBIwQLAQVGCwsaAiYCAlcTCAEBiD4MtSSMMwEBASOBBoUwgX0IglCERIMCg?= =?us-ascii?q?loFiDSRO16BUYl6hTiHYIYFkF0CHoNGgVyHUwF+AQEB?= X-IPAS-Result: =?us-ascii?q?A0DNAAB7p99XhsO3RtlcRwEBFgEBBQEBgwIBAQEBAYEfWbh?= =?us-ascii?q?sggOGHgKBQzgUAQEBAQEBAQEBAQESAQEBCgkLCRkvgjIYghgBAQMBIwQLAQVGC?= =?us-ascii?q?wsaAiYCAlcTCAEBiD4MtSSMMwEBASOBBoUwgX0IglCERIMCgloFiDSRO16BUYl?= =?us-ascii?q?6hTiHYIYFkF0CHoNGgVyHUwF+AQEB?= X-IronPort-AV: E=Sophos;i="5.30,361,1470693600"; d="scan'208";a="193880543" Received: from relay3-d.mail.gandi.net ([217.70.183.195]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 19 Sep 2016 10:58:32 +0200 Received: from mfilter6-d.gandi.net (mfilter6-d.gandi.net [217.70.178.135]) by relay3-d.mail.gandi.net (Postfix) with ESMTP id 44268A811F for ; Mon, 19 Sep 2016 10:58:32 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at mfilter6-d.gandi.net Received: from relay3-d.mail.gandi.net ([IPv6:::ffff:217.70.183.195]) by mfilter6-d.gandi.net (mfilter6-d.gandi.net [::ffff:10.0.15.180]) (amavisd-new, port 10024) with ESMTP id IX6tKy0Xb9X1 for ; Mon, 19 Sep 2016 10:58:29 +0200 (CEST) X-Originating-IP: 194.57.247.3 Received: from [172.22.8.73] (fw.enpc.fr [194.57.247.3]) (Authenticated sender: octa@polychoron.fr) by relay3-d.mail.gandi.net (Postfix) with ESMTPSA id EF02FA813A for ; Mon, 19 Sep 2016 10:58:29 +0200 (CEST) To: caml-list@inria.fr References: From: octachron Message-ID: Date: Mon, 19 Sep 2016 10:58:29 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Covariant GADTs Hi Markus, > Taking an element link can be done without > having to introduce superfluous pattern matches, because the GADT > guarantees via the type system that a link is non-empty. I fear that you are misinterpreting the guarantees giving to you by the type ('el, 'kind) Link.t. This type can be rewritten as type ('el, _) t = | Empty : ('el, [ `empty ]) t | Elt : { mutable prev : ('el, [< kind ] as 'prev ) t; el : 'el; mutable next : ('el, [< kind ] as 'next ) t; } -> ('el, [ `elt ]) t Notice the existential types 'prev and 'next within the Elt constructor: they mean that outside of the context of Elt, the type system simply does not know the subtype of the prev and next fields. Even within the context of the `Elt` constructor, the type system only knows that there exists two types p and n such that Elt r is typed Elt {prev:p;next:n;el:el}. But the information about which precise type was present when constructing the value is lost. Therefore, these fields are neither readable nor writable directly. A direct manifestation of the problem is that, as you observed, you cannot assign new values to either prev or next without use of `Obj.magic`. For instance, let set_next (Elt r) x = r.next <- x;; fails with Error: This expression has type 'a but an expression was expected of type ('b, [< kind ]) t. The type constructor $Elt_'next would escape its scope. because the type checker tries to unify the type 'a of x with the existential type $Elt_'next of `next`. Using a fantasy syntax, we have let set_next (type a) (Elt (type p n) {next:n; prev:p; _} ) (x:a) = r.next:p <- x:a;; and the types `a` and `p` cannot be unified because `p` should not escape the context of the constructor Elt. Consequently writing `set_next` requires to use Obj.magic: let set_next (Elt r) x = r.next <- Obj.magic x;; This use of Obj.magic should be fine, since it is impossible to access the field prev and next directly. Contrarily, your coerce function is unsafe: let current (Elt {el;_}) = el let crash () = current (coerce @@ Empty) On the other side of the problem, this is the reason why you need to wrap access with an option in `get_opt_next`. Note that I am not certain that this wrapping does not completely defeat your optimisation objective. Regards − octachron. Le 09/19/16 à 03:52, Markus Mottl a écrit : > Hi Petter, > > thanks, the above approach obviously works with my previous example, > which I had sadly oversimplified. In my case I was actually dealing > with inlined, mutable records where the above won't work, because then > I can't overwrite fields. The somewhat more complete example also > contains strange type system behavior I don't understand that may even > be a bug. > > The example below shows how GADTs + inline records + (if available) > covariance could help implement doubly linked lists much more > efficiently. The memory representation using mutable inline records > is essentially optimal. Taking an element link can be done without > having to introduce superfluous pattern matches, because the GADT > guarantees via the type system that a link is non-empty. > > I had to use "Obj.magic" due to the lack of covariance support with > GADTs in the "coerce" function, which I believe to be sound. > > The strange behavior is in the "insert_first" function and also the > "create" function: "Empty" is not of covariant type, but nevertheless > can be used for allocation in that way (e.g. in the "let res = ..." > part). But the commented out lines show that I cannot overwrite the > exact same field in the just allocated value with the exact same > value. I can understand the reason why the latter is not possible, > but why is allocation allowed that way? Maybe a type system guru can > explain what's going on. > > ---------- > module Link = struct > type kind = [ `empty | `elt ] > > type ('el, _) t = > | Empty : ('el, [ `empty ]) t > | Elt : { > mutable prev : ('el, [< kind ]) t; > el : 'el; > mutable next : ('el, [< kind ]) t; > } -> ('el, [ `elt ]) t > > let coerce (t : ('el, [< kind ]) t) : ('el, [< kind ]) t = Obj.magic t > > let get_opt_elt : type a. ('el, a) t -> ('el, [ `elt ]) t option = function > | Empty -> None > | Elt _ as elt -> Some elt > > let cut : type a. ('el, a) t -> unit = function > | Empty -> () > | Elt { prev = prev_elt; next = next_elt } -> > match prev_elt, next_elt with > | Empty, Empty -> () > | Empty, Elt next -> next.prev <- coerce Empty > | Elt prev, Empty -> prev.next <- coerce Empty > | Elt prev, Elt next -> > prev.next <- coerce next_elt; > next.prev <- coerce prev_elt > end (* Link *) > > module Doubly_linked : sig > type 'el t > type 'el elt > > val create : unit -> 'el t > val first : 'el t -> 'el elt option > val insert_first : 'el t -> 'el -> unit > val remove : 'el elt -> unit > end = struct > open Link > > type 'el t = Head : { mutable head : ('el, [< Link.kind ]) Link.t } -> 'el t > type 'el elt = ('el, [ `elt ]) Link.t > > let create () = Head { head = Empty } > > let first (Head h) = Link.get_opt_elt h.head > > let insert_first (Head h) el = > h.head <- > match h.head with > | Empty -> > let res = Elt { prev = Empty; el; next = Empty } in > (* let Elt foo = res in *) > (* foo.prev <- Empty; *) > coerce res > | Elt _ as next -> coerce (Elt { prev = Empty; el; next }) > > let remove = Link.cut > end (* Doubly_linked *) > ---------- > > Regards, > Markus > >