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 4BAD67ED11 for ; Mon, 19 Sep 2016 17:03:18 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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-io0-f169.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.223.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.223.169 as permitted sender) identity=mailfrom; client-ip=209.85.223.169; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io0-f169.google.com) identity=helo; client-ip=209.85.223.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-io0-f169.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ATgnb2h3kwbFiBEgEsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?sekWKvad9pjvdHbS+e9qxAeQG96KsrQU16GI7OigATVGusfZ9ihaMdRlbFwssY?= =?us-ascii?q?0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8?= =?us-ascii?q?Kum9IIPOlcP/j7n0oMyKJVUUz2TiKfMqdVPt/F2X7pFXyaJZaY8JgiPTpXVJf+?= =?us-ascii?q?kEjUhJHnm02yjG28Gr4ZR4+D5Rsf9yv+RJUKH9YrhqBecAVGduGykP6cbqrRjO?= =?us-ascii?q?SxeUrjtZCz1O00kAPw+QyRD5Xp7wtmPfv+xxwjiZPMu+GbU9Xzi4/qRqTjfpkz?= =?us-ascii?q?8dPiV/6nyB2eJqi6cOhRu7pAFki6vTfJ2RfK57d7neYMhcQG1dQsJ5WClIA4f6?= =?us-ascii?q?ZIwKWblSdd1EppXw8gNd5SC1AhOhUaa2kmdF?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BgAACI/d9XhqnfVdFdGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFQEBAQECAQEBAQgBAQEBgw8BAQEBATw5fAeNLKtAggMghX4CgUcHOBQ?= =?us-ascii?q?BAQEBAQEBAQEBARIBAQEICwsJGS+CMgQBFQEEghEBAQQSEQQZARQHHQEDDAYDA?= =?us-ascii?q?gsNAgImAgIhAQERAQUBHAYTIogNAQMXDpVEj0eBMj4yiz2Ba4JfBYNoChknDVS?= =?us-ascii?q?CUwEBAQEBBQEBAQEBAQEYAgYQdoUxhFSCR4F9gwKCWgWZOjWBZYRBhkaCcIFuT?= =?us-ascii?q?o0uhwKBU4QPgjkTHoERHoMoDREKgWwiNIZCgUABAQE?= X-IPAS-Result: =?us-ascii?q?A0BgAACI/d9XhqnfVdFdGgEBAQECAQEBAQgBAQEBFQEBAQE?= =?us-ascii?q?CAQEBAQgBAQEBgw8BAQEBATw5fAeNLKtAggMghX4CgUcHOBQBAQEBAQEBAQEBA?= =?us-ascii?q?RIBAQEICwsJGS+CMgQBFQEEghEBAQQSEQQZARQHHQEDDAYDAgsNAgImAgIhAQE?= =?us-ascii?q?RAQUBHAYTIogNAQMXDpVEj0eBMj4yiz2Ba4JfBYNoChknDVSCUwEBAQEBBQEBA?= =?us-ascii?q?QEBAQEYAgYQdoUxhFSCR4F9gwKCWgWZOjWBZYRBhkaCcIFuTo0uhwKBU4QPgjk?= =?us-ascii?q?THoERHoMoDREKgWwiNIZCgUABAQE?= X-IronPort-AV: E=Sophos;i="5.30,362,1470693600"; d="scan'208";a="193932945" Received: from mail-io0-f169.google.com ([209.85.223.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 19 Sep 2016 17:03:16 +0200 Received: by mail-io0-f169.google.com with SMTP id r145so94000526ior.0 for ; Mon, 19 Sep 2016 08:03:16 -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=YJAP4VTZdiYewwrMKxnxLJfxJxdDfGxEyrgpAy3EupU=; b=E1KwFa1rJbISZU2unzGelXF1rVjk+GzmLqDXmheyUWC7cSeWxHNQpy/5fyb9d+J5oq Km3fJdrDY9l2fNFPf40bf11e66xT4QC7LhCPg4pwIadpsZb6rx8R+FL/AUmD5hK4DRTm eE80xjbh0Tai3OORI5+8/sdEbzGtyX7+RrsViZegPb4a4qUdJ8sgWuMIiuOwejxu9hhC SWPnBErgEdQK2w6eLing75+cqANDCiEdP9OELWWnkTu11bAbHutMjMcg/ODW4Idjcem6 6pMWTaKdPwV5PONSryq9OHmHGFVndyMsoo/KgoBaT0B2njRdAdji0Pg84SvjcZIMaam3 WQ1g== 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=YJAP4VTZdiYewwrMKxnxLJfxJxdDfGxEyrgpAy3EupU=; b=dqo1+zspqY4xK3tsIJrY2EKK4Ej9CLaRtaLVgLuubiP1f5TxhlScoJc0eRljAHZZFD s4BHll952dv8tRgTPPoyhuAbH9R2VUnERfLUFdS3OLr+ktUAup0XnmiYLMNqjZgY1TfD BclsDE9Emdz2kkxib7QlUztSQ7Xr3DWXQ2qrZpUOt7P/sLQN2/Fl3RWNdGqe1j6kPOHe +bYs4CDnzmnNnr/yVc10QnJjJBPeXoQQc8RAOeHL7y86sW3ASPmyeQZh05eNq63VeSvy 8Y3+G5NYKGhcQv88oUmvO53Mjb1MXs2bSRzkvDqBBKrf+JXYdKwgVydX9zxdJQscfRk3 JmBA== X-Gm-Message-State: AE9vXwNaI9idB9EuqG8xgYI4Nvt62WNb9MP5Ucv8n5ZR1AiGPYhr/gfvWxe9nsQCkN9wHTkndGLL6eDQFlhnXg== X-Received: by 10.107.201.20 with SMTP id z20mr36560987iof.90.1474297395575; Mon, 19 Sep 2016 08:03:15 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.131.219 with HTTP; Mon, 19 Sep 2016 08:03:14 -0700 (PDT) In-Reply-To: <2324346.DfHVUap7Qc@molnar> References: <2161155.JggR3X9ZFM@molnar> <2324346.DfHVUap7Qc@molnar> From: Markus Mottl Date: Mon, 19 Sep 2016 11:03:14 -0400 Message-ID: To: Mikhail Mandrykin Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Covariant GADTs Ah, thanks a lot, I totally missed following the link. Yes, this OCaml feature would solve this problem efficiently, too. I guess an existentially quantified record field would look neater, but I'd be happy enough with GPR#606 getting into the next release. Regards, Markus On Mon, Sep 19, 2016 at 10:53 AM, Mikhail Mandrykin w= rote: > On =D0=BF=D0=BE=D0=BD=D0=B5=D0=B4=D0=B5=D0=BB=D1=8C=D0=BD=D0=B8=D0=BA, 19= =D1=81=D0=B5=D0=BD=D1=82=D1=8F=D0=B1=D1=80=D1=8F 2016 =D0=B3. 10:46:22 MSK= Markus Mottl wrote: > >> Thanks, Mikhail, that's the correct way to solve this problem from a > >> typing perspective. Sadly, this encoding using a separate GADT > >> containing a "Link" tag defeats the purpose of the idea, which was to > >> save indirections and the associated memory overhead. I wish it was > >> possible to introduce existentially quantified variables within > >> records without having to go through another GADT. > > > > In fact the purpose of GPR#606 (https://github.com/ocaml/ocaml/pull/606) = is > to avoid the indirection e.g. > > type t =3D A of string [@@unboxed] > > let x =3D A "toto" > > assert (Obj.repr x =3D=3D Obj.repr (match x with A s -> s)) > > It is also said in the comment that: > > > > This is useful (for example): > > > > --... > > -- when using a single-constructor, single-field GADT to introduce an > existential type > > > > This is merged into trunk and should appear in 4.04.0: (from CHANGES) > > - GPR#606: optimized representation for immutable records with a single > > field, and concrete types with a single constructor with a single argumen= t. > > This is triggered with a [@@unboxed] attribute on the type definition. > > (Damien Doligez) > > > > Regards, Mikhail > > > >> > >> Regards, > >> Markus > >> > >> On Mon, Sep 19, 2016 at 6:18 AM, Mikhail Mandrykin >> wrote: > >> > Hello, > >> > > >> > On =D0=BF=D0=BE=D0=BD=D0=B5=D0=B4=D0=B5=D0=BB=D1=8C=D0=BD=D0=B8=D0=BA,= 19 =D1=81=D0=B5=D0=BD=D1=82=D1=8F=D0=B1=D1=80=D1=8F 2016 =D0=B3. 10:58:29 = MSK you wrote: > >> >> Hi Markus, > >> >> > >> >> > >> >> > >> >> 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, > >> > > >> > As far as I know quite common approach in this case is introduction of > >> > one-constructor wrapper types to hide the existential variable and all= ow > >> > mutability e.g. > >> > > >> > > >> > > >> > type ('el, _) t =3D > >> > > >> > | Empty : ('el, [ `empty ]) t > >> > | > >> > | Elt : { > >> > > >> > mutable prev : 'el link; > >> > > >> > el : 'el; > >> > > >> > mutable next : 'el link; > >> > > >> > } -> ('el, [ `elt ]) t > >> > > >> > and 'el link =3D Link : ('el, _) t -> 'el link;; > >> > > >> > > >> > > >> > So the link type wraps the type parameter of the next element and thus > >> > allows safe mutation, otherwise it's only possible to update the field > >> > with > >> > the element of exactly same type that doesn't allow e.g. deleting an > >> > element at the end of the list without reallocating the corresponding > >> > record of the previous element (and if one decides to keep more precise > >> > information e.g. about the number of elements, the whole list needs to >> > be > >> > re-allocated). With the link wrapper as above it's possible to define > >> > add, remove and also a get operation without and extra pattern matchin= g: > >> > > >> > > >> > > >> > let add : type a. _ -> (_, a) t -> (_, [`elt]) t =3D fun el -> > >> > > >> > function > >> > > >> > | Empty -> Elt { el; prev =3D Link Empty; next =3D Link Empty } > >> > | > >> > | Elt _ as n -> Elt { el; prev =3D Link Empty; next =3D Link n };; > >> > > >> > let remove : type a. ('el, a) t -> 'el link =3D > >> > > >> > function > >> > > >> > | Empty -> Link Empty > >> > | > >> > | Elt { prev =3D Link p as prev; next =3D Link n as next} -> > >> > > >> > (match p with Empty -> () | Elt p -> p.next <- next); > >> > > >> > (match n with Empty -> () | Elt n -> n.prev <- prev); > >> > > >> > next;; > >> > > >> > > >> > > >> > let get : (_, [`elt]) t -> _ =3D function Elt { el; _ } -> el > >> > > >> > > >> > > >> > Also note the GPR#606(https://github.com/ocaml/ocaml/pull/606 ) that > >> > should > >> > allow constructing and deconstructing links (Link l) without overhead. > >> > > >> > > >> > > >> > Regards, Mikhail > >> > > >> > > >> > > >> > > >> > > >> > > >> > > >> > -- > >> > > >> > Mikhail Mandrykin > >> > > >> > Linux Verification Center, ISPRAS > >> > > >> > web: http://linuxtesting.org > >> > > >> > e-mail: mandrykin@ispras.ru > > > > > > -- > > Mikhail Mandrykin > > Linux Verification Center, ISPRAS > > web: http://linuxtesting.org > > e-mail: mandrykin@ispras.ru --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com