From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 AFC0D7ED11 for ; Mon, 19 Sep 2016 12:18:21 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=pra; client-ip=83.149.199.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=mailfrom; client-ip=83.149.199.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp.ispras.ru) identity=helo; client-ip=83.149.199.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="postmaster@smtp.ispras.ru"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3APSXjCRHhc2CcR3PkBVZ2CZ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ75r82wAkXT6L1XgUPTWs2DsrQf2rOQ4/yrADBIoc7Y9itTKNoUD15NoP?= =?us-ascii?q?5VtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blIt?= =?us-ascii?q?dazLE4Lfx/66y/q1s8WKJV4Z3XztPfgrcF329VyX7ZhOx9M6a+4Y8VjgmjNwYe?= =?us-ascii?q?NYxGdldxq4vi3XwYOOxqNl6DlaoPk79sRNAu3QdqU8SqFEXnx9azhmrOWijxTI?= =?us-ascii?q?TBOO630ASS1W10MQW0mWpC39C5z4ty+/sutmxAGbO9f3RPY6Q2eM9aBuHTrpiy?= =?us-ascii?q?cONjpx1WjRhtZhj6Nd6Eakrhpz2Z/XYYe9NeFmZKrGO8kHEzkSFv1NXjBMV9vv?= =?us-ascii?q?J7AECPAMaKMB99Hw?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BcAwCUut9X/8THlVNcHAEBBAEBCgEBF?= =?us-ascii?q?wYMgl4zAQEBAQF1SgExhSeIDKMTiCyCAyCDFIJqAoF+FAEBAQEBAQEBAQEBXSe?= =?us-ascii?q?CMgQBFQEEghABAQEDASMEUgULCQIYCSECAg8BRxmIQgwKlzydJowqAQEBAQYBA?= =?us-ascii?q?QEBAQEBIIsLhESDAoJaBY8likqGJoskTocbhhOHAoVig3seNoRtOzSGIoFAAQE?= =?us-ascii?q?B?= X-IPAS-Result: =?us-ascii?q?A0BcAwCUut9X/8THlVNcHAEBBAEBCgEBFwYMgl4zAQEBAQF?= =?us-ascii?q?1SgExhSeIDKMTiCyCAyCDFIJqAoF+FAEBAQEBAQEBAQEBXSeCMgQBFQEEghABA?= =?us-ascii?q?QEDASMEUgULCQIYCSECAg8BRxmIQgwKlzydJowqAQEBAQYBAQEBAQEBIIsLhES?= =?us-ascii?q?DAoJaBY8likqGJoskTocbhhOHAoVig3seNoRtOzSGIoFAAQEB?= X-IronPort-AV: E=Sophos;i="5.30,361,1470693600"; d="scan'208,217";a="193893187" Received: from bran.ispras.ru (HELO smtp.ispras.ru) ([83.149.199.196]) by mail3-smtp-sop.national.inria.fr with ESMTP; 19 Sep 2016 12:18:20 +0200 Received: from molnar.localnet (molnar.intra.ispras.ru [10.10.2.183]) by smtp.ispras.ru (Postfix) with ESMTP id 224656129D; Mon, 19 Sep 2016 13:18:19 +0300 (MSK) From: Mikhail Mandrykin To: caml-list@inria.fr Cc: Markus Mottl Date: Mon, 19 Sep 2016 13:18:19 +0300 Message-ID: <2161155.JggR3X9ZFM@molnar> User-Agent: KMail/5.1.3 (Linux/4.4.0-36-generic; KDE/5.18.0; x86_64; ; ) In-Reply-To: References: MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="nextPart1637076.TxOIkOc6mV" Content-Transfer-Encoding: 7Bit Subject: Re: [Caml-list] Covariant GADTs This is a multi-part message in MIME format. --nextPart1637076.TxOIkOc6mV Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" 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, >=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, 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 mutabi= lity=20 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 allo= ws=20 safe mutation, otherwise it's only possible to update the field with the el= ement of=20 exactly same type that doesn't allow e.g. deleting an element at the end of= the list=20 without reallocating the corresponding record of the previous element (and = if one=20 decides to keep more precise information e.g. about the number of elements,= the=20 whole list needs to be re-allocated). With the link wrapper as above it's p= ossible to=20 define add, remove and also a get operation without and extra pattern match= ing: 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[1] ) that sho= uld=20 allow constructing and deconstructing links (Link l) without overhead. Regards, Mikhail --=20 Mikhail Mandrykin Linux Verification Center, ISPRAS web: http://linuxtesting.org e-mail: mandrykin@ispras.ru -------- [1] https://github.com/ocaml/ocaml/pull/606 --nextPart1637076.TxOIkOc6mV Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8"

Hello,

&nb= sp;

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 Mar= kus,

>

> Theref= ore, 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

> instan= ce,

&nb= sp;

As far as I= know quite common approach in this case is introduction of one-constructo= r wrapper types to hide the existential variable and allow mutability e.g.<= /p>

&nb= sp;

type ('el, = _) t =3D

| Empt= y : ('el, [ `empty ]) t

| Elt = : {

mu= table prev : 'el link;

el= : 'el;

mu= table next : 'el link;

} -&= gt; ('el, [ `elt ]) t

and 'el lin= k =3D Link : ('el, _) t -> 'el link;;

&nb= sp;

So the link= type wraps the type parameter of the next element and thus allows safe mut= ation, 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 o= f the list without reallocating the corresponding record of the previous el= ement (and if one decides to keep more precise information e.g. about the n= umber 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 operati= on without and extra pattern matching:

&nb= sp;

let add : t= ype a. _ -> (_, a) t -> (_, [`elt]) t =3D fun el ->

function<= /p>

| Empty -= > Elt { el; prev =3D Link Empty; next =3D Link Empty }

| Elt _ a= s n -> Elt { el; prev =3D Link Empty; next =3D Link n };;

&nb= sp;

let remove = : type a. ('el, a) t -> 'el link =3D

function<= /p>

| Empty -= > Link Empty

| Elt { p= rev =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;;<= /p>

&nb= sp;

let get : (= _, [`elt]) t -> _ =3D function Elt { el; _ } -> el

&nb= sp;

Also note t= he GPR#606(https://github.com/ocaml/o= caml/pull/606 ) that should allow constructing and deconstructin= g links (Link l) without overhead.

&nb= sp;

Regards, Mi= khail

&nb= sp;

&nb= sp;

&nb= sp;

--

Mikhail Man= drykin

Linux Verif= ication Center, ISPRAS

web: http:/= /linuxtesting.org

e-mail: man= drykin@ispras.ru

= --nextPart1637076.TxOIkOc6mV--