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 EB25B7FF41 for ; Mon, 19 Sep 2016 16:53:57 +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=3AVBpXhBJVYt15QcPpYtmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgUK/vxwZ3uMQTl6Ol3ixeRBMOAuqsC27ad7fmoGTRZp83e4DZaKN0EfiRGoP?= =?us-ascii?q?tVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blIt?= =?us-ascii?q?dazdU7TfhMWv1u2054abI0AR3GL8MvtOK0CTpB/Sq9JepIx+NqJ5nh7AuHhVYK?= =?us-ascii?q?JTwn90IXqcmh/94oG7+5s1oApKvPd00s9DUaz7e+wdRLpUFiUlMmZ9sMjisxXZ?= =?us-ascii?q?XAiO4FMdSX0MmwEOGRWTv0KyZYv4riav7rk14yKdJ8CjCOlsATk=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0B6BQBq+99X/8THlVNdHAEBBAEBCgEBF?= =?us-ascii?q?wEFAQsBgl0zAQEBAQF1SgExhSeIDKMUiCyCAyCDFIJqAoIGFAEBAQEBAQEBAQE?= =?us-ascii?q?BXSeCMgQBFQEEghABAQEDASMEUgULCQIYCRcBCQICDwFHBhOIQgwKlVydJow1A?= =?us-ascii?q?QEBAQYBAQEBAQEBIIsLhESDAoJaBY8likqGJoskTocbhhOHAoVig3seNoJ/G4F?= =?us-ascii?q?TOzSGQoFAAQEB?= X-IPAS-Result: =?us-ascii?q?A0B6BQBq+99X/8THlVNdHAEBBAEBCgEBFwEFAQsBgl0zAQE?= =?us-ascii?q?BAQF1SgExhSeIDKMUiCyCAyCDFIJqAoIGFAEBAQEBAQEBAQEBXSeCMgQBFQEEg?= =?us-ascii?q?hABAQEDASMEUgULCQIYCRcBCQICDwFHBhOIQgwKlVydJow1AQEBAQYBAQEBAQE?= =?us-ascii?q?BIIsLhESDAoJaBY8likqGJoskTocbhhOHAoVig3seNoJ/G4FTOzSGQoFAAQEB?= X-IronPort-AV: E=Sophos;i="5.30,362,1470693600"; d="scan'208,217";a="237401143" 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 16:53:56 +0200 Received: from molnar.localnet (molnar.intra.ispras.ru [10.10.2.183]) by smtp.ispras.ru (Postfix) with ESMTP id 52C446129D; Mon, 19 Sep 2016 17:53:56 +0300 (MSK) From: Mikhail Mandrykin To: Markus Mottl Cc: OCaml List Date: Mon, 19 Sep 2016 17:53:56 +0300 Message-ID: <2324346.DfHVUap7Qc@molnar> User-Agent: KMail/5.1.3 (Linux/4.4.0-36-generic; KDE/5.18.0; x86_64; ; ) In-Reply-To: References: <2161155.JggR3X9ZFM@molnar> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="nextPart2183531.9deqRkLVfm" Content-Transfer-Encoding: 7Bit Subject: Re: [Caml-list] Covariant GADTs This is a multi-part message in MIME format. --nextPart2183531.9deqRkLVfm Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" 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[1])= is to=20 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 exi= stential=20 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 argum= ent. This is triggered with a [@@unboxed] attribute on the type definition. (Damien Doligez) Regards, Mikhail >=20 > Regards, > Markus >=20 > On Mon, Sep 19, 2016 at 6:18 AM, Mikhail Mandrykin = =20 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 M= SK you wrote: > >> Hi Markus, > >>=20 > >>=20 > >>=20 > >> Therefore, these fields are neither readable nor writable directly. A > >>=20 > >> direct manifestation of the problem is that, as you observed, you cann= ot > >>=20 > >> assign new values to either prev or next without use of `Obj.magic`. F= or > >>=20 > >> instance, > >=20 > > 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. > >=20 > >=20 > >=20 > > type ('el, _) t =3D > >=20 > > | Empty : ('el, [ `empty ]) t > > |=20 > > | Elt : { > >=20 > > mutable prev : 'el link; > >=20 > > el : 'el; > >=20 > > mutable next : 'el link; > >=20 > > } -> ('el, [ `elt ]) t > >=20 > > and 'el link =3D Link : ('el, _) t -> 'el link;; > >=20 > >=20 > >=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 > > 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 matching: > >=20 > >=20 > >=20 > > let add : type a. _ -> (_, a) t -> (_, [`elt]) t =3D fun el -> > >=20 > > function > >=20 > > | Empty -> Elt { el; prev =3D Link Empty; next =3D Link Empty } > > |=20 > > | Elt _ as n -> Elt { el; prev =3D Link Empty; next =3D Link n };; > >=20 > > let remove : type a. ('el, a) t -> 'el link =3D > >=20 > > function > >=20 > > | Empty -> Link Empty > > |=20 > > | Elt { prev =3D Link p as prev; next =3D Link n as next} -> > >=20 > > (match p with Empty -> () | Elt p -> p.next <- next); > >=20 > > (match n with Empty -> () | Elt n -> n.prev <- prev); > >=20= --nextPart2183531.9deqRkLVfm Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8"

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 Mo= ttl wrote:

> Thanks= , Mikhail, that's the correct way to solve this problem from a

> typing= perspective. Sadly, this encoding using a separate GADT

> contai= ning a "Link" tag defeats the purpose of the idea, which was to

> save i= ndirections and the associated memory overhead. I wish it was

> possib= le to introduce existentially quantified variables within

> record= s without having to go through another GADT.

&nb= sp;

In fact the= purpose of GPR#606 (https://github.co= m/ocaml/ocaml/pull/606) is to avoid the indirection e.g.

type t = =3D A of string [@@unboxed]

let x =3D= A "toto"

assert (O= bj.repr x =3D=3D Obj.repr (match x with A s -> s))

It is also = said in the comment that:

&nb= sp;

This is us= eful (for example):

&nb= sp;

--...

-- when u= sing a single-constructor, single-field GADT to introduce an existential ty= pe

&nb= sp;

This is mer= ged 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 argument.

This is= triggered with a [@@unboxed] attribute on the type definition.

(Damien= Doligez)

&nb= sp;

Regards, Mi= khail

&nb= sp;

>

> Regard= s,

> Markus=

>

> On Mon= , Sep 19, 2016 at 6:18 AM, Mikhail Mandrykin <mandrykin@ispras.ru> wr= ote:

> > H= ello,

> > <= /p>

> > O= n =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:

> >&g= t; Hi Markus,

> >&g= t;

> >&g= t;

> >&g= t;

> >&g= t; Therefore, these fields are neither readable nor writable directly. A

> >&g= t;

> >&g= t; direct manifestation of the problem is that, as you observed, you cannot=

> >&g= t;

> >&g= t; assign new values to either prev or next without use of `Obj.magic`. For=

> >&g= t;

> >&g= t; instance,

> > <= /p>

> > A= s 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

> > m= utability e.g.

> > <= /p>

> > <= /p>

> > <= /p>

> > t= ype ('el, _) t =3D

> > <= /p>

> > |= Empty : ('el, [ `empty ]) t

> > |=

> > |= Elt : {

> > <= /p>

> > m= utable prev : 'el link;

> > <= /p>

> > e= l : 'el;

> > <= /p>

> > m= utable next : 'el link;

> > <= /p>

> > }= -> ('el, [ `elt ]) t

> > <= /p>

> > a= nd 'el link =3D Link : ('el, _) t -> 'el link;;

> > <= /p>

> > <= /p>

> > <= /p>

> > S= o the link type wraps the type parameter of the next element and thus

> > a= llows safe mutation, otherwise it's only possible to update the field

> > w= ith

> > t= he element of exactly same type that doesn't allow e.g. deleting an

> > e= lement at the end of the list without reallocating the corresponding

> > r= ecord of the previous element (and if one decides to keep more precise

> > i= nformation e.g. about the number of elements, the whole list needs to be

> > r= e-allocated). With the link wrapper as above it's possible to define

> > a= dd, remove and also a get operation without and extra pattern matching:

> > <= /p>

> > <= /p>

> > <= /p>

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

> > <= /p>

> > f= unction

> > <= /p>

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

> > |=

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

> > <= /p>

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

> > <= /p>

> > f= unction

> > <= /p>

> > |= Empty -> Link Empty

> > |=

> > |= Elt { prev =3D Link p as prev; next =3D Link n as next} ->

> > <= /p>

> > (= match p with Empty -> () | Elt p -> p.next <- next);

> > <= /p>

> > (= match n with Empty -> () | Elt n -> n.prev <- prev);

> > <= /p>

> > n= ext;;

> > <= /p>

> > <= /p>

> > <= /p>

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

> > <= /p>

> > <= /p>

> > <= /p>

> > A= lso note the GPR#606(https://github.com/ocaml/ocaml/pull/606 ) that

> > s= hould

> > a= llow constructing and deconstructing links (Link l) without overhead.

> > <= /p>

> > <= /p>

> > <= /p>

> > R= egards, Mikhail

> > <= /p>

> > <= /p>

> > <= /p>

> > <= /p>

> > <= /p>

> > <= /p>

> > <= /p>

> > -= -

> > <= /p>

> > M= ikhail Mandrykin

> > <= /p>

> > L= inux Verification Center, ISPRAS

> > <= /p>

> > w= eb: http://linuxtesting.org

> > <= /p>

> > e= -mail: mandrykin@ispras.ru

&nb= sp;

&nb= sp;

--

Mikhail Man= drykin

Linux Verif= ication Center, ISPRAS

web: http:/= /linuxtesting.org

e-mail: man= drykin@ispras.ru

= --nextPart2183531.9deqRkLVfm--