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 sympa.inria.fr (Postfix) with ESMTPS id 7E4207ED11 for ; Mon, 19 Sep 2016 15:37:22 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mandrykin@ispras.ru; spf=None smtp.mailfrom=mandrykin@ispras.ru; spf=None smtp.helo=postmaster@smtp.ispras.ru Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=pra; client-ip=83.149.199.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=mailfrom; client-ip=83.149.199.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp.ispras.ru) identity=helo; client-ip=83.149.199.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="postmaster@smtp.ispras.ru"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ANLeSDxEbuWgm0rvmNvppI51GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ76rsSwAkXT6L1XgUPTWs2DsrQf2rOQ4/yrBTNIoc7Y9itdINoUD15NoP?= =?us-ascii?q?5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9?= =?us-ascii?q?fbytScb6xv663OGq+pDVfx4AxH/kOeszf12KqlDav8wSxI9jMboZyx3To3IOdf?= =?us-ascii?q?4F63lvIAe2nhX878a0tLtq9ShKqvEg8YYUVKz8c74pTr1eJDU9K3o8/4vxqE+Q?= =?us-ascii?q?HkO0+nIAXzBOwVJzCA/f4US/B8+pvw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BlAwDW6d9X/8THlVNdHAYMGRgHgwQBA?= =?us-ascii?q?QEBAXVKATGwR4gsggMggxSCagKCARQBAQEBAQEBAQEBAV0ngjIEARUBBIIRAQE?= =?us-ascii?q?EIwRSEAkCGAICBSECAg8BRxmITpVynSaMLwwlgQaKBYRETII2gloBBI8likqGJ?= =?us-ascii?q?oskTocbhhOHAoVig3seNoRtOzSGIoFAAQEB?= X-IPAS-Result: =?us-ascii?q?A0BlAwDW6d9X/8THlVNdHAYMGRgHgwQBAQEBAXVKATGwR4g?= =?us-ascii?q?sggMggxSCagKCARQBAQEBAQEBAQEBAV0ngjIEARUBBIIRAQEEIwRSEAkCGAICB?= =?us-ascii?q?SECAg8BRxmITpVynSaMLwwlgQaKBYRETII2gloBBI8likqGJoskTocbhhOHAoV?= =?us-ascii?q?ig3seNoRtOzSGIoFAAQEB?= X-IronPort-AV: E=Sophos;i="5.30,361,1470693600"; d="scan'208";a="237387080" Received: from bran.ispras.ru (HELO smtp.ispras.ru) ([83.149.199.196]) by mail2-smtp-roc.national.inria.fr with ESMTP; 19 Sep 2016 15:37:20 +0200 Received: from molnar.localnet (molnar.intra.ispras.ru [10.10.2.183]) by smtp.ispras.ru (Postfix) with ESMTP id 5D2766129D; Mon, 19 Sep 2016 16:37:19 +0300 (MSK) From: Mikhail Mandrykin To: caml-list@inria.fr Cc: Markus Mottl Date: Mon, 19 Sep 2016 16:37:19 +0300 Message-ID: <3439197.u3LigSGb2F@molnar> User-Agent: KMail/5.1.3 (Linux/4.4.0-36-generic; KDE/5.18.0; x86_64; ; ) In-Reply-To: <2161155.JggR3X9ZFM@molnar> References: <2161155.JggR3X9ZFM@molnar> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" Subject: Re: [Caml-list] Covariant GADTs 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. 13:18:19 MSK = Mikhail Mandrykin wrote: > Hello, >=20 > 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, > >=20 > > 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, >=20 > As far as I know quite common approach in this case is introduction of o= ne- > constructor wrapper types to hide the existential variable and allow > mutability e.g. >=20 > type ('el, _) t =3D >=20 > | Empty : ('el, [ `empty ]) t > | Elt : { >=20 > mutable prev : 'el link; > el : 'el; > mutable next : 'el link; > } -> ('el, [ `elt ]) t > and 'el link =3D Link : ('el, _) t -> 'el link;; >=20 > 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 > 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 matching: >=20 > 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 };; >=20 > 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;; This is actually buggy (although typesafe), more like this: let add : type a. _ -> (_, a) t -> (_, [`elt]) t =3D fun el -> function | Empty -> Elt { el; prev =3D Link Empty; next =3D Link Empty } | Elt ({ prev =3D Link p as prev; _ } as n) as next -> let r =3D Elt { el; prev; next =3D Link next } in (match p with Empty -> () | Elt p -> p.next <- Link r); n.prev <- Link r; r;; let remove : type a. (_, a) t -> (_, a) t * _ =3D function | Empty -> Empty, Link Empty | Elt ({ prev =3D Link p as prev; next =3D Link n as next} as e) as elt -> (match p with Empty -> () | Elt p -> p.next <- next); (match n with Empty -> () | Elt n -> n.prev <- prev); e.next <- Link Empty; e.prev <- Link Empty; elt, next;; Regards, Mikhail --=20 Mikhail Mandrykin Linux Verification Center, ISPRAS web: http://linuxtesting.org e-mail: mandrykin@ispras.ru