Unboxed types (version 2) #34

goldfirere · 2022-10-27T19:52:08Z

This is a complete update from @stedolan's proposal for unboxed types (#10), built from that proposal, and written in collaboration with the type-systems team here at Jane Street: @lpw25, @stedolan, @antalsz, and @ccasin.

We're still at the early stages of implementation (in https://github.com/ocaml-flambda/ocaml-jst), so all feedback is warmly welcomed.

Rendered version

nojb · 2022-10-27T20:09:18Z

Rendered version: https://github.com/goldfirere/ocaml-rfcs/blob/unboxed-types/rfcs/unboxed-types.md

Gbury · 2022-10-27T22:38:57Z

I have two small questions:

I'd guess that abstract types exposed in an interface must be given a layout or else, the layout is assumed to be value, to maintain backward compatibility. In such a case the following example given in the proposal:

module M : sig
  type unboxed_t
  type t = box unboxed_t
end = struct
  type t = { x : int32; y : int32 }
  type unboxed_t = #t
end

would, if I'm not mistaken, fail to typecheck because by default, unboxed_t in the signature being abstract, it would be assumed to have layout value, which it does not, since it has layout value * value. (Actually, even before that, the signature alone would appear to be quite weird since box foo does not really make much sense if foo has layout value). Is my understanding correct, or did I miss something ?

secondly, how does that work interact with the work on unboxed constructors ? E.g.,would it be completely separate, or could unboxed constructors somehow fit in this work ?

lpw25 · 2022-10-28T08:59:38Z

In such a case the following example given in the proposal [...] would, if I'm not mistaken, fail to typecheck

That's correct, this example should have:

type unboxed_t : value * value

in the signature.

how does that work interact with the work on unboxed constructors ?

See Stephen's comment on the unboxed constructors RFC. Essentially there are two optimisations proposed in that RFC: "inlining" and "disjointness" as Stephen calls them. The unboxed variants described in this RFC give you inlining, but this RFC doesn't say anything about disjointness. I think that @gasche has separately been making progress towards some implementation of disjointness.

One area where they could interact is that disjointness requires information about the representation of abstract value types in order to ensure that they are suitably disjoint. This information is also a form of kinding, although a more fine-grained one than you want for unboxing. It should cause no problems to allow a finer notion of kind on abstract types than on type variables, which would allow these two proposals to interact seamlessly.

goldfirere · 2022-10-28T12:35:38Z

Thanks @Gbury. You're right about abstract types, and you're right that my example was wrong. I've fixed it.

The unboxed constructor work is definitely related, but not the same thing, as @lpw25 points out. That said, I'm hoping to update this soon with a new section that will allow a non-allocating option type, based on the same notions of disjointness from Stephen's post, and using the layout system in this proposal to guarantee safety. In a sense, by giving us a way to classify types, this starts to lay the groundwork for unboxed constructors (if I'm understanding everything correctly).

gasche · 2022-10-28T14:04:38Z

Current status of unboxed constructors

In case it can help, here is all the information one could want on the current status of unboxed constructors:

My work with @nchataing was presented precisely in September 2021 as a comment on top of @yallop's RFC: Proposal: constructor unboxing #14 (comment) ( This is in fact a markdown file we maintain in our experimental ocaml repository: https://github.com/gasche/ocaml/blob/head_shape/HEAD_SHAPE.spec.md ) This comment / this file serve as self-contained descriptions of the work, which is directly inspired by the original RFC but also different, and as far as I know is the only variant of the idea that is being worked on.
Besides this comment which describes the specification as a language feature, we maintain another document (written around the same time) describing our implementation approach: https://github.com/gasche/ocaml/blob/head_shape/HEAD_SHAPE.impl.md , which can be taken as an introductory guide if someone wanted to look at our implementation, hosted on a head_shape branch of my ocaml fork.
I later wrote a research paper that goes into the details of the termination argument for repeated type-definition expansion during head shape computations; unfortunately the current version is in French. I am planning to translate this into an English paper (with Stephen hopefully), but haven't done it yet.
I looked at upstreaming the unboxed-constructor work recently -- at getting my experimental fork in a nice shape to start sending PRs. But currently this upstream work is waiting on #10041, which is a November 2020 PR from @stedolan that I think should be merged first before my own PRs, as I wish to build on its code. (I made this point in Expand aliases if necessary during immediacy computation (second attempt) ocaml#10041 (comment) in May 2021, and then again in early June 2020, and then (by email directly to Leo, Stephen and Antal) late June and September 1st.) I would like to move this work forward, but for now I am waiting to find someone willing to help (as either a submitter or a reviewer) on #10041.

General interaction between the two proposals

I think globally the two strands of work are complementary in a good way. (This was already said before, let's summarize again.)

In our work on unboxed constructors transform the representation of values (and thus the compilation strategy) based on type-directed representation information, an abstraction/approximation of types that we call the "head shape". We worked out how to compute the head shape of a type expression, but of course we cannot assume anything on the shape of type parameters/variables and abstract types

The work on unboxed types is, in part, about introducing explicit kinds ("layouts") in the language to classify types depending on their representation properties, and performing kind-checking and kind-inference as one would expect. This is precious to make our unboxed-constructor work more modular: if we suddenly get to specify the head shape of a type parameter, or an abstract type, the user can express more constructor-unboxing across abstraction boundaries. This assumes that there is a close connection between our abstraction of type (head shapes) and the kinds (layouts) in the unboxed-types work, and my understanding is that there could very well be. (Our head shapes are a bit more fine-grained than the unboxed layouts right now, one could extend unboxed layouts or just accept coarser-grained information across abstraction boundaries.)

Removing constructors in both proposals

Both proposals allow to "remove" some constructors from the value representation, but in disjoint ways.

In our proposal (1) of unboxed constructors, this removal is "unboxing" (turning a boxing operation into a no-op):

the arguments of the unboxed constructor always have layout value (or a sub-layout of value)
the value representation is exactly preserved by applying an unboxed constructor, those really are no-ops

In the unboxed-types proposal (2), this removal is "inlining" or "packing":

the arguments of the unboxed constructor (or packed record field) always have non-value layouts (void, bits, word, float)
the value representation is transformed (in general) when applying the inlined/transformed constructor

For example, the memory layout of an occurrence of #int32 in a larger record or variant definition (unboxed or not) depends on the rest of the definition: it may be stored in the first half of a 64bit word, or in the second half, and in general putting a value of type #int32 inside a record field may involve bit-shifting operations. This is the same when inlining/packing an unboxed record into another record (unboxed or not), or an unboxed variant inside another variant; for the unboxed variants, the tag bits change from the "alone" representation to the "inside the outer variant" representation, so compiling the unboxed constructor has to insert appropriate data transformation.

The different approach in different settings make a lot of sense and both are useful.

For non-uniform unbox values, "transforming" the value on the fly during inlining/packing (approach 2) is generally a fine design choice because this transformation is very cheap, or at least very close to the simple cost of passing the value around. Transposing this choice into setting (1) would be dubious: transforming the tag of boxed variants on the fly involves allocating a new value, which is probably not an operation we want to make completely implicit in general. (This being said, we currently accept implicit allocations when reading unboxed floats.)
Conversely, once we decide to never transform uniform values (approach 1), we have to impose the "disjointness" restriction, which adds static restrictions on when unboxing is allowed. Transforming arguments on the fly (approach 2) imposes basically no restriction on when inlining/packing is permissible, so it is more flexible.

To me this suggests that both features are useful and we could consider having both at the same time in the language.

ccasin · 2022-10-28T14:18:39Z

@gasche Regarding #10041 in particular, I'm still planning to help with this. We also updated and included it in the prototype of the first bits of this document (ocaml-flambda/ocaml-jst#48). That prototype is occupying all my time until I have it in a place where it can be reviewed internally, but I think that's only about a week away, and I'm then happy to update #10041 and make a new PR (or review yours, if you get there first).

gasche · 2022-10-28T14:21:41Z

Sounds great, thanks!

gadmm

Here is some feedback. The main questions are about possible simplifications to the design of mutable fields (or about things that I am missing).

(Note: the comments appear in the order in which I wrote them initially, not as they are meant to be read; the "files changed" tab shows them in the intended order.)

gadmm · 2022-10-28T13:01:36Z

rfcs/unboxed-types.md

+
+In general, we reserve the right to reorder components in an unboxed tuple or
+record in order to reduce padding. With demand, we could imagine introducing
+a way for programmers to request that we do not reorder. (An unboxed type that


Comes to mind, specifying a C-like memory layout, having in mind the use-case of interoperability with foreign structs (see #[repr(C)] in Rust).

Yes, I expect we'll need this.

gadmm · 2022-10-28T13:22:54Z

rfcs/unboxed-types.md

+```ocaml
+type #t = #( K1 of ty1 | K2 of ty2 | ... )
+type t = #t box
+```


How does this equation work for constructors without payload? Is there a conversion between the unboxed tag and the boxed tag/immediate? (Concretely I imagine that type ('a : any) option = None | Some 'a uses tag 0 for None and 1 for Some for the unboxed version, but tag 0 for Some and immediate 0 for None in the boxed version—if we leave aside for now the niche optimization whereby you could encode None as NULL in certain cases.)

Is there special treatment for the void layout? Concretely for the equality type:

type (_,_) eq = Refl : ('a,'a) eq

we most likely would like #eq : void (compile-time erasure for equality types) while perhaps still enjoying eq : immediate.

Hmmmm...... maybe this is suggesting that e.g. void + void + void <= immediate? I like that. We could do even better, with something like void + void + bits32 <= immediate. Or we could just say that enumerations are immediate, but I like the sublayout approach more, as it's more general. Not sure yet whether it plays too poorly with type inference, though.

How does this equation work for constructors without payload? Is there a conversion between the unboxed tag and the boxed tag/immediate? (Concretely I imagine that type ('a : any) option = None | Some 'a uses tag 0 for None and 1 for Some for the unboxed version, but tag 0 for Some and immediate 0 for None in the boxed version—if we leave aside for now the niche optimization whereby you could encode None as NULL in certain cases.)

Just for reference, in flambda2, when we locally unbox a value of some kind, and particularly a variant, we actually generate an is_int variable along with the tag and the payloads. This makes the conversion between boxed and unboxed really simple, at the price of using more variables to hold the variant. It's probably not ideal in this situation, but at least it avoids the complication of having different tags between the boxed and unboxed versions.

gadmm · 2022-10-28T13:50:47Z

rfcs/unboxed-types.md

+We could imagine a restriction in the language stopping such copies from
+happening, or requiring extra syntax to signal them. However, we hope that there
+will not be too many wide unboxed records, and copying a few fields really isn't
+so slow. So, on balance, we do not think this is necessary.


One data point is that unintended and silent deep copies were a bane of old C++, which would tend to go in favour of having a loud syntax for copying wide unboxed types.

Yes. There has been considerable discomfort around this point internally as well. But putting e.g. #<- on every mutation seems pretty unpleasant, too. I really don't know what's best.

A comparison with C++ is in fact somewhat unfair, as the silent copies in C++ could be recursive (e.g. copying a vector of vectors) so the problem is much worse there. A better comparison is with Rust, so it can be interesting to read what they say about it (e.g. rust-lang/rust#45683).

Rust has unboxed fixed-size arrays, unlike this proposal, which make it easier to make copies costly. However, I argue that this difference is not important. Indeed, fixed-size arrays are useful, and with your proposal, users can emulate them by writing them explicitly with something like t * t * ... * t, so I believe that code like this with large structs are going to be written regardless.

My sense reading that thread is that they are just about as puzzled as we are here.

In my opinion, we should not add extra annotations to the language for this. Instead, the goal we are after is this: we want to make sure the programmer knows what they are doing. I can think of at least three ways of accomplishing this goal:

Add required annotations to the language

Add a warning; we can then debate whether the warning should be on by default. And we have to figure out a way of locally suppressing the warning, likely with some kind of annotation.

Add magic to merlin to alert the user.

I'm strongly in favor of 3, if it can be made to work. That is, imagine if an expensive <- is highlighted in yellow, say. The programmer can see this and account for it. Maybe we also add an annotation to suppress the highlighting? Not sure there. It would be very cool if an editor with merlin enabled rendered #<- as <- with a little # over it, reducing visual clutter. Actually, maybe this is the same as (2), but with special treatment in merlin.

To be clear, my "if it can be made to work" is a hedge against the possibility that people don't actually use merlin. My OCaml experience is very skewed: I'm in an environment where everybody uses merlin, because it's all set up for them. I'm not sure it's as pervasive outside Jane Street's walls.

It sounds to me like you are advocating for a lint, like in this Rust thread.

I do not have a definite opinion or an alternative solution to propose, but tooling is less mature in OCaml and has fewer contributors, and if the problem is deemed worthy of language design considerations then one should be careful about not relegating the problem to future/incomplete/third-party support.

gadmm · 2022-10-28T14:09:38Z

rfcs/unboxed-types.md

+  foo ();
+  t.(.pt.x) <- 7;
+  foo ()
+```


Here I find it clearer to see the assignment as a shorthand (as you mention, and with the relaxation to the tearing restriction I proposed) for:

t.pt <- #{ t.pt with x = 7 };

plus some optimizations to the resulting code (maybe we do not need the shorthand in a first time). Without your shorthand notation, it is apparent that there is no aliasing between pt.x and t.pt.x (syntactically it works just like in current OCaml).

Now when trying to see this as a direct mutation of the field x, perhaps this also misses a loud syntax for an operation that breaks aliasing from this angle (the copy let pt = t.pt). With functional update syntax this could look something like let pt = #{ t.pt }). But I find it clearer to avoid the shorthand notation and the loud syntax altogether.

In our internal design debates, we eventually settled on a medium-volume notation: t.(.pt.x) <- 7, where the parentheses and extra dot are the extra volume. Originally, it was just t.pt.x <- 7, but that indeed seemed too confusing. Yet I sense from your comments that you think the design is not quite loud enough. Perhaps you're right.

To clarify, there are two points in my comment that can be discussed separately:

Maybe one can skip the artificially-loud notation altogether, by writing something like t.pt <- #{ t.pt with x = 7 } instead of t.(.pt.x) <- 7 if it is made possible (after relaxing the tearing restriction: this is discussed in another comment). The compiler should be smart enough to compile it the same. Then all possible confusions about aliasing disappear. The notation is still loud, but not in way that has to be introduced artificially. (In my current understanding of this proposal, this is my preference compared to the next point.)

If nevertheless something like t.pt.x <- 7 is kept, I pointed out that the confusing part (to me at least) is that the notation let pt = t.pt suggests an aliasing of the x fields that does not exist, so perhaps the latter operation is what deserves to be louder/clearer (e.g. let pt = #{ t.pt }).