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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 5981C7FF41 for ; Mon, 19 Sep 2016 16:39:47 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=markus.mottl@gmail.com; spf=Pass smtp.mailfrom=markus.mottl@gmail.com; spf=None smtp.helo=postmaster@mail-it0-f52.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.214.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.214.52 as permitted sender) identity=mailfrom; client-ip=209.85.214.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-it0-f52.google.com) identity=helo; client-ip=209.85.214.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-it0-f52.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ArU9T0hOwJa6cbctnqhgl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0KP78rarrMEGX3/hxlliBBdydsKMdzbqK+P65ESxYuNDa7yBEKMQNHzY+yu?= =?us-ascii?q?wo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEt?= =?us-ascii?q?fre9Msfogs+2z+G//YHIK0UN3WLlIOBEFwittQjaquURhIJjLO5xlkqI8TN0fL?= =?us-ascii?q?FRzn9hLlKJmBC0ssC74JdL6yNUqvkh8NRHV+P0ZfJrY6ZfCWEDOno2+dajkB7f?= =?us-ascii?q?UQ/Hsn4VSGYLiVxNBBTZ6Dn1W57wtm3xse8ri3rSBtH/Ub1hAWfq1KxsUhK9zX?= =?us-ascii?q?peOg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CYAAC4999XhjTWVdFdGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFwEBBAEBCgEBgw8BAQEBATw5fAeNLJlQiW+IAYIDJIV6AoFHBzgUAQE?= =?us-ascii?q?BAQEBAQEBAQESAQEBCAsLCRkvgjIEARUFghEBAQQSEQQZARQHEgsBAwwGBQsNA?= =?us-ascii?q?gIJHQICIQEBEQEFAQoSBhMSEIgNAQMXDqUlgTI+Mos9gWuCXwWDZwoZJwMKVIJ?= =?us-ascii?q?TAQEBAQEBAQEBAQEBAQEBAQEBFwIGEHaFMYRUgkeBfYMCgloBBIZoDIFAkQY1g?= =?us-ascii?q?WWEQYYDQ4JwggU3jS6IVYQPgjkTHoERHoMoHoF2IjSGIoFAAQEB?= X-IPAS-Result: =?us-ascii?q?A0CYAAC4999XhjTWVdFdGgEBAQECAQEBAQgBAQEBFwEBBAE?= =?us-ascii?q?BCgEBgw8BAQEBATw5fAeNLJlQiW+IAYIDJIV6AoFHBzgUAQEBAQEBAQEBAQESA?= =?us-ascii?q?QEBCAsLCRkvgjIEARUFghEBAQQSEQQZARQHEgsBAwwGBQsNAgIJHQICIQEBEQE?= =?us-ascii?q?FAQoSBhMSEIgNAQMXDqUlgTI+Mos9gWuCXwWDZwoZJwMKVIJTAQEBAQEBAQEBA?= =?us-ascii?q?QEBAQEBAQEBFwIGEHaFMYRUgkeBfYMCgloBBIZoDIFAkQY1gWWEQYYDQ4JwggU?= =?us-ascii?q?3jS6IVYQPgjkTHoERHoMoHoF2IjSGIoFAAQEB?= X-IronPort-AV: E=Sophos;i="5.30,362,1470693600"; d="scan'208";a="237398521" Received: from mail-it0-f52.google.com ([209.85.214.52]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 19 Sep 2016 16:39:44 +0200 Received: by mail-it0-f52.google.com with SMTP id 186so72588071itf.0 for ; Mon, 19 Sep 2016 07:39:44 -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:content-transfer-encoding; bh=5iIRgCkETq4g1DXQ6PM10UrUAzEEpR+UlKd/8C8Hx2s=; b=JQn2zKDjQLg7O3/z/jPZrX88DZI4W8iunrAU+HPztJgqiu/6xcfYHUIavF3bJLSLKy ncbEHia9AAf0I33MS1xrPMwWM8wsAW+dTMbivtjqLJdhxhi9rKZ75cdiEV+ubVXeFL+M t7J3ogQeRgPf8ILmbjkfOql3UChq51AJESFs2zF+gdX4cyGDjo9p7W4BSglI0XSTWmY7 Ni+D0Ms5qjprnuBO7VaYy+Bfaxv5ilMvwajJi5rX0kFSI1e6HmWZ3eofjwRgrH6f8q02 wdfdB0ju+TyhciT9gKoxpPoB2H1tn1Juf62VMcIDPVqh4XG55mK+sbPIScJpkXn1+urV 7SRA== 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:content-transfer-encoding; bh=5iIRgCkETq4g1DXQ6PM10UrUAzEEpR+UlKd/8C8Hx2s=; b=DVJE19HxNqEinl6+x8Ebuq6+qaJwnXfbC4B5WxG+Xu8b1Q7wSMxC+LxG6/2eqpnzvW S4S/agU65MZeNVoBC4WlLYNqR04NrbIVfwRoPWvR8QJ4pNd0Onp3vF2uqm7F7lOP9UAr RC945rUzLBaZeMgm3kQaBYAbUgj8eDK03OjhVGDm+0TI0knk3g6QEiUxp+VAiuMlxdHV U8AFyx1kfFlbw5KqKM27t/sSRkoaPkmIxNYO9/I20vcUPmithuq2aB9cxqGtv7n1AW7w +jgmeVwa/JthG9cv+lj4FhnqBdS6bZCZkt6SfyE2hu+MyKXkmtC2N5vVzTmKLagkkroY liBQ== X-Gm-Message-State: AE9vXwNv/RwbK1Z8sSBPxo7Pp/XJjum1/7OUy4w+3nTOuJGVdixtGypeTO1ZrNdWvdN7jZp6C1vwJuC3MytmMQ== X-Received: by 10.36.152.5 with SMTP id n5mr10917970itd.79.1474295983674; Mon, 19 Sep 2016 07:39:43 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.131.219 with HTTP; Mon, 19 Sep 2016 07:39:42 -0700 (PDT) In-Reply-To: References: From: Markus Mottl Date: Mon, 19 Sep 2016 10:39:42 -0400 Message-ID: To: octachron Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Covariant GADTs Hi Octachron, yes, indeed, that was spot on. I somehow got sidetracked by the lack of covariance annotations for GADTs, not realizing that the implicitly defined type variables 'prev and 'next are existential within the scope of Elt only. Anything outside can't be a witness so I can't write, and anything inside can't get out without escaping scope. I guess what I would need to solve my problem efficiently are record fields that support existentially rather than only universally quantified variables. Something along the lines of: | Elt : { mutable prev : $'kind. ('el, 'kind) t } Would that make sense? Btw., the "option" type was only introduced so as not having to reveal the type representation to users of the API. The "Some" tag would typically be dropped right after the user pattern matches on the option type. They would then still benefit from the efficient representation of the link, and the GADT + inlined record would still be able to save the memory overhead associated with the indirection to a non-inlined record. Regards, Markus On Mon, Sep 19, 2016 at 4:58 AM, octachron wrote: > 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 t= ype > ('el, 'kind) Link.t. This type can be rewritten as > > type ('el, _) t =3D > | 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 va= lue > is lost. > > Therefore, these fields are neither readable nor writable directly. A dir= ect > 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 =3D 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) =3D r.n= ext: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 =3D 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;_}) =3D el > let crash () =3D 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 =E2=88=92 octachron. > > > Le 09/19/16 =C3=A0 03:52, Markus Mottl a =C3=A9crit : > >> 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 =3D ..." >> 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 =3D struct >> type kind =3D [ `empty | `elt ] >> >> type ('el, _) t =3D >> | 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 =3D Obj.magi= c t >> >> let get_opt_elt : type a. ('el, a) t -> ('el, [ `elt ]) t option =3D >> function >> | Empty -> None >> | Elt _ as elt -> Some elt >> >> let cut : type a. ('el, a) t -> unit =3D function >> | Empty -> () >> | Elt { prev =3D prev_elt; next =3D 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 =3D struct >> open Link >> >> type 'el t =3D Head : { mutable head : ('el, [< Link.kind ]) Link.t }= -> >> 'el t >> type 'el elt =3D ('el, [ `elt ]) Link.t >> >> let create () =3D Head { head =3D Empty } >> >> let first (Head h) =3D Link.get_opt_elt h.head >> >> let insert_first (Head h) el =3D >> h.head <- >> match h.head with >> | Empty -> >> let res =3D Elt { prev =3D Empty; el; next =3D Empty } in >> (* let Elt foo =3D res in *) >> (* foo.prev <- Empty; *) >> coerce res >> | Elt _ as next -> coerce (Elt { prev =3D Empty; el; next }) >> >> let remove =3D Link.cut >> end (* Doubly_linked *) >> ---------- >> >> Regards, >> Markus >> >> > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com