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 6D21F7ED11 for ; Mon, 19 Sep 2016 16:46:25 +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-f47.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.47; 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.47 as permitted sender) identity=mailfrom; client-ip=209.85.214.47; 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-f47.google.com) identity=helo; client-ip=209.85.214.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-it0-f47.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AOTL9vR1JYshWdd+QsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?segXLfad9pjvdHbS+e9qxAeQG96KsrQU16GI6uigATVGusnR9ihaMdRlbFwst4?= =?us-ascii?q?Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVIm?= =?us-ascii?q?bsy8IIPZjty22uau4NWTJlwQ3HvuKY91eTC3rgXYt81epIJkJrwgyRrP6i9Ncu?= =?us-ascii?q?Ja33JrJFS7ng3k/M6ruoR+pXd+ofUkoutJS6bnZOwdSqBECHxyNmkv59Dw8xzE?= =?us-ascii?q?UReLznQZW2QS1BFPBl6Wv1nBQp7tv36i5aJG0y6AMJizFOhsVA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CYAAAd+d9Xhi/WVdFdGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFgEBAQMBAQEJAQEBgw8BAQEBATw5fAeNLKtAggMghX4CgUcHOBQBAQE?= =?us-ascii?q?BAQEBAQEBARIBAQEICwsJGS+CMgQBFQEEghEBAQQSEQQZARQHHQEDDAYDAgsNA?= =?us-ascii?q?gImAgIhAQERAQUBHAYTIogNAQMXDpVfj0eBMj4yiz2Ba4JfBYNoChknDVSCUwE?= =?us-ascii?q?BAQEBAQQBAQEBAQEZAgYQdoUxhFSCR4F9gwKCWgEEmTo1gWWEQYZGgnCBbk6NL?= =?us-ascii?q?ocCgVOED4I5Ex6BER6DKB6BdiI0hiKBQAEBAQ?= X-IPAS-Result: =?us-ascii?q?A0CYAAAd+d9Xhi/WVdFdGgEBAQECAQEBAQgBAQEBFgEBAQM?= =?us-ascii?q?BAQEJAQEBgw8BAQEBATw5fAeNLKtAggMghX4CgUcHOBQBAQEBAQEBAQEBARIBA?= =?us-ascii?q?QEICwsJGS+CMgQBFQEEghEBAQQSEQQZARQHHQEDDAYDAgsNAgImAgIhAQERAQU?= =?us-ascii?q?BHAYTIogNAQMXDpVfj0eBMj4yiz2Ba4JfBYNoChknDVSCUwEBAQEBAQQBAQEBA?= =?us-ascii?q?QEZAgYQdoUxhFSCR4F9gwKCWgEEmTo1gWWEQYZGgnCBbk6NLocCgVOED4I5Ex6?= =?us-ascii?q?BER6DKB6BdiI0hiKBQAEBAQ?= X-IronPort-AV: E=Sophos;i="5.30,362,1470693600"; d="scan'208";a="237399641" Received: from mail-it0-f47.google.com ([209.85.214.47]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 19 Sep 2016 16:46:24 +0200 Received: by mail-it0-f47.google.com with SMTP id 15so20495774ita.1 for ; Mon, 19 Sep 2016 07:46:24 -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=A2TEOhEyOJz1nKxbScuRTXDZxtqAYaGjOnEktxa82HE=; b=HB1wO+2M+ax9iImDbun7DIp1ChJ1eap2rmZ/El95+R9mdDaWV0iKl1Y6LVD/WNPv/d e9hURMp8s1eitBixJUUZ7jPtnXD7ME1izfgANOgRSlDH5pNmfa3j9zqdUSj97BA8cgZa SqyVTkIk/2qDvC/woX84CcTZKbLL4gu+qiMhOlNRIY7WvD2Nlx5rsXC1BevHYB6+PXGr f6xTXk1GVpYdXUAYGBKuVXLk+fh8gp4QQEoSzESn3aGw8nZwaKuVpA2BpcsXkbr5cD7z NdSA5nB/JhGTGZgX4Hg09na4rkVMUjoouvSNaQ4zfm61VVHdFPFNb94VM+NTjQDmX0Al a0HQ== 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=A2TEOhEyOJz1nKxbScuRTXDZxtqAYaGjOnEktxa82HE=; b=VK3oHVVAtiWjuwYT+l9p/OZkKBaCtYnoejJAVmBQIYIhOn36P0ppulE5W1rEKsiaBT gmGPcBkAwZyeTztWLp3zX+/vfQri63gCDhmv23+uuoVrUJ36LUyPjniR+6G0GMuEYQK4 OCVHhrVJH/IBl1ql/pp16HfiiK03nl2EV5va9+lsRMViOURZ1Cr99PdyyUfFUS8+3PYQ sgxcKEMnDFtPHsBGrZqZqU7Q0s+RlB2HpCNGXMRRglcxmaGp4MDXp9iGSOjSL6Lf04gl +7cRwIk9m+j13L+IMjXxPQOzBdf54zJoSUPz6EeWtD5oXh7cEKdHribKIwzl2L75IcGH HwRQ== X-Gm-Message-State: AE9vXwOpjq6EDxmEYS6+upCiUX3kFKvS3HNQbl/EqyKWN+uLsmRae5pChBFJsTwdAvc0r+A71PvYunFO+DqAlQ== X-Received: by 10.36.10.145 with SMTP id 139mr11611913itw.68.1474296383163; Mon, 19 Sep 2016 07:46:23 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.131.219 with HTTP; Mon, 19 Sep 2016 07:46:22 -0700 (PDT) In-Reply-To: <2161155.JggR3X9ZFM@molnar> References: <2161155.JggR3X9ZFM@molnar> From: Markus Mottl Date: Mon, 19 Sep 2016 10:46:22 -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 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. Regards, Markus On Mon, Sep 19, 2016 at 6:18 AM, Mikhail Mandrykin wr= ote: > 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 allow > 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 wi= th > the element of exactly same type that doesn't allow e.g. deleting an elem= ent > at the end of the list without reallocating the corresponding record of t= he > 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). W= ith > the link wrapper as above it's possible to define add, remove and also a = get > operation without and extra pattern matching: > > > > 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 shou= ld > 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 --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com