From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2VFqxE8008444 for ; Sat, 31 Mar 2012 17:52:59 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AswCANQnd0/ZSMD3iGdsb2JhbAAqEQm4fiIBAQEKCQsJEwQkggkBAQQBJwsBRgULCxgJJQ8BBCghE4gECQcpuU+LB4YVBJZyhEyNOw X-IronPort-AV: E=Sophos;i="4.75,349,1330902000"; d="scan'208";a="138492382" Received: from fmmailgate06.web.de ([217.72.192.247]) by mail4-smtp-sop.national.inria.fr with ESMTP; 31 Mar 2012 17:52:54 +0200 Received: from moweb001.kundenserver.de (moweb001.kundenserver.de [172.19.20.114]) by fmmailgate06.web.de (Postfix) with ESMTP id D03E61072884 for ; Sat, 31 Mar 2012 17:52:53 +0200 (CEST) Received: from frosties.localnet ([95.208.118.96]) by smtp.web.de (mrweb002) with ESMTPA (Nemesis) id 0MKJAE-1SCMiM2GJy-001O9b; Sat, 31 Mar 2012 17:52:48 +0200 Received: from mrvn by frosties.localnet with local (Exim 4.77) (envelope-from ) id 1SE0bd-00043y-Vh; Sat, 31 Mar 2012 17:52:46 +0200 From: Goswin von Brederlow To: Francois Bobot Cc: caml-list@inria.fr In-Reply-To: <4F75CA78.4080103@lri.fr> ("Francois Bobot"'s message of "Fri, 30 Mar 2012 10:00:08 -0500") References: <87fwcx6ejm.fsf@frosties.localnet> <4F74E647.1040603@lri.fr> <87k4229td1.fsf@frosties.localnet> <4F75CA78.4080103@lri.fr> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) Date: Sat, 31 Mar 2012 17:52:45 +0200 Message-ID: <87wr60hinm.fsf@frosties.localnet> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Provags-ID: V02:K0:z3zy3DPP0NKHiTIF5g1oR3BblKAPGD0WYwla/fmx+r0 XHB8rfBIUqUGAbz4k4hFdGMbGvNSURFfZeXYS4nm0EQVH0AO9N ROpJIzQ4jn50cVBohtXabowhCRrE+nh6oCJDNS9ZKUt+KPuaEx 27NgTb9UEHvDcWznmwgDTdDy0lKpAPwGqLbvBKuNihcRmWwt9V rnxfVGWR2LExggbW6CxHQ== Subject: Re: [Caml-list] Wish: mutable variant types, equivalence with records François Bobot writes: > On 30/03/2012 07:16, Goswin von Brederlow wrote: >> François Bobot writes: >> >>> On 24/03/2012 13:45, Wojciech Meyer wrote: >>>> Please see [1], Alain Frisch has been working recently on implementing >>>> in-line records for constructor arguments. >>>> >>>> It's more implementation/design implications than people might think. >>>> >>>> [1] http://caml.inria.fr/mantis/view.php?id=5528 >>> >>> In the thread of this proposed feature, there is a remark that inlined >>> record and normal record can become competing features. There is also >>> the burden that inlined record as proposed can be modified only in >>> pattern matching. >>> >>> But can't we consider that, for a semantic, syntax and typing perspective: >>> >>> type t = >>> | A of string >>> | B of ({msg: string; mutable foo:int} as t2) >>> | C >>> >>> is exactly the same thing than: >>> >>> type t = >>> | A of string >>> | B of t2 >>> | C >>> >>> and t2 = {msg: string; mutable foo:int} >> >> That would change existing code because B of t2 currently is a Block of >> size 1 with tag B and pointer to a record of type t2. > > I don't propose to change how is compiled the second definition. Just > that if a developer use the first definition in a module he can > consider that he define t and t2 like in the second definition. The > only exception is if you use Obj.magic: Obj.magic (B r) == Obj.magic r. > But Obj.magic is not in the semantic I assume. > >> >>> The only difference is that when you create a record of type t2 the >>> tag is directly the one of B in the first case and is the default tag >>> for record (the first tag if I remember well) in the second case. So >>> in the first case applying the constructor B is just the identity. >> >> Maybe the type of a record could be altered to, at least internally, >> include a tag value: > Every records already include a tag value, it's just always the same: > the tag of the first non-constant constructor of a sum type. No it doesn't. Not in its type. It just happens to have a tag 0 in its memory representation. Say you have type r1 = { x : int; } type Foo = Foo of int | Bar of ({ x : int; } as r2) type Foo = Foo of ({ x : int; } as r3) | Bar of int The type r1 and the internal type r2 are not the same. A record of type r2 would have a tag of 1. Same with r2 and r3, they should be different types. >> type t = A of string | B of ({msg: string; mutable foo:int} as t2) | C >> type t2 = {[B] x : int; } >> >> The inline record would be identical to the external record with tag >> value and (t2 :> t) would work even implicitly. > > I'm not sure that we should make implicit conversion (inference? > principality?). But that B r is a noop can be very interesting. The implicit parts would be in matches for example. "match x with B r ->" would basically just translate to (x :> t2) with the additional check that the tag is right. Or let bar = fun i -> {[B] x = i; } let foo : int -> t = fun i -> bar i val bar : int -> {[B] x : int; } val foo : int -> t On the other hand bar could already be interfered as type int -> t. It all depends on wether the [] syntax would be restricted to inline records in constructors or not. It probably makes sense to restrict declaring a record with tag to inline records. Otherwise it might get confusing what value the tag should actually have. One other thing: How do you declare a value of such a type? type r = { x : int; } type foo = Foo of r | Blub of int type bar = Bar of { y : int; } | Blubber of int let myfoo = Foo { x = 0; } let mybar = Bar { y = 0; } This would be confusing since the two look identical but do something quite different. Maybe the syntax should be more like this: type r = { x : int; } type foo = Foo of r | Blub of int type bar = { Bar y : int; } | Blubber of int let myfoo = Foo { x = 0; } let mybar = { Bar y = 0; } With the constructor actualy inside the record the two cases look different and it is visually clear that the "Bar" tag is part of the record while "Foo" is a constructor taking a record as argument. > If we want to play to extend this feature (perhaps too much) we can > play with conversion between sum type without cost by allowing Ap to > be also the identity: > > > type tpublic = > | A of ({... } as ta) > | B of ({... } as tb) > > type tprivate = > | Ap of ta > | Bp of tb > | Cp of ... > > > Since A,ta and Ap share the same tag the following function is the identity: Again no, at least it isn't a NOP. The current memory representation of Ap of ta is incompatible with the representation we want for A of ({... } as ta). MfG Goswin