Re: [Caml-list] Wish: mutable variant types, equivalence with records

[Goswin von Brederlow <goswin-v-b@web.de>]

François Bobot <bobot@lri.fr> writes:

> On 30/03/2012 07:16, Goswin von Brederlow wrote:
>> François Bobot<bobot@lri.fr>  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 [<tag>] 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