Unboxed types (version 2)

[goldfirere]

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]

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

[Gbury]

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]

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]

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]

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: https://github.com/ocaml/RFCs/pull/14#issuecomment-920643103 ( 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 https://github.com/ocaml/ocaml/pull/10041#issuecomment-847710537 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<N>, word, float<N>)

• 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]

@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 (https://github.com/ocaml-flambda/ocaml-jst/pull/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]

Sounds great, thanks!

[SkySkimmer]

It seems a bit confusing that in type t = #{ mutable foo : whatever; ... } the mutable only matters for t box, but I don't have an alternative proposal. Maybe mutating unboxed records could be a default fatal warning instead of always forbidden?

Also do I understand correctly that type t = #{ bla : whatever } and type t = { bla : whatever } [@@unboxed] are equivalent?

[SkySkimmer]

I assume there is some kind of check on type recursion to forbid things like type t = #{ x : t; y : int } Is the check described somewhere?

[goldfirere]

Maybe mutating unboxed records could be a default fatal warning instead of always forbidden?

Maybe. It's hard to see how this could ever be a good idea, though. It wouldn't be hard to give a very informative error message in this case, pointing out that mutation of unboxed types is bizarre.

Also do I understand correctly that type t = #{ bla : whatever } and type t = { bla : whatever } [@@unboxed] are equivalent?

No, unfortunately. They behave the same at runtime, but there are subtle differences at compile time. For example, the former is constructed with #{ bla = ... } while the latter is constructed with { bla = ... }. Essentially, the latter is meant to be completely invisible to programmers, while the former isn't.

I assume there is some kind of check on type recursion to forbid things like type t = #{ x : t; y : int } Is the check described somewhere?

There's no detailed description of this, but the check is simple in essence: that t simply doesn't have a (finite) layout. So whatever code computes the layout will have to detect this case.

Thanks for the questions!

[gasche]

Re. layout computation and invalid recursive references: we have the same issue in our computation of "head shapes" for unboxed type constructors. There are "malign" cycles that clearly must be rejected

type t = Foo of t [@unboxed] | Bar

type t = #{ x : t; y : bool }

and also "benign" cycles that look odd (the types have no value inhabitants), but could in fact be accepted

type f = Foo of t [@unboxed]

type t = #{ x : t }  

One difficulty pointed out by @stedolan is that we want to use a criterion that works well with type abstraction, and in particular this may require accepting the benign cycles. (Our first impulse was to reject all cycles, because benign cycles are not programs you want to save from rejection very hard, and it is easier to implement the reject-all criterion.) If we have

type t = Foo of abs [@unboxed]
type t = #{ x : abs }

where abs is an abstract type, do we want to accept or reject those examples? For unboxed type constructors we clearly want to accept this example. But then the abstraction may be revelead later to be a recursive occurrence, abs is in fact t, and so you end up with a benign cycle. So benign cycles should be accepted, or you break substituability.

[gasche]

This being said, the comparison may not go all the way, because if we look at the case of "potentially-malign cycle hidden under an abstraction",

type t = Foo of abs [@unboxed] | Bar
type t = #{ x : abs; y : bool }

then it is clear that we will reject the unboxed-construct example (an abstract type has a "full" head shape, that conflicts with the shape of the Bar constructor ), while it is less obvious to me that the unboxed-record will be rejected. It looks less intuitive to explain to users that it should be rejected because abs may later be revealed to be a recursive occurrence of t. Maybe you instead want to have a system where the validity of unboxed types is re-checked when substitutions happen (for example when applying a functor), and give up on substituability anyway.

[gasche]

(The issue where we discussed this, in particular Stephen's excellent observation, is https://github.com/ocaml/ocaml/issues/10485 .)

[SkySkimmer]

it is less obvious to me that the unboxed-record will be rejected

Wouldn't abs have a layout which prevents instantiating it with t? So it's rejected when we try to instantiate the cycle, not when we define t.

[goldfirere]

Wouldn't abs have a layout which prevents instantiating it with t? So it's rejected when we try to instantiate the cycle, not when we define t.

Exactly so. If we have

type t = #{ x : abs; y : bool }

then t : (layout of abs) * immediate. When abs is declared, its layout must be given (or it defaults to value, the layout of ordinary types). So, no matter what layout abs is given, saying type abs = t later won't be possible, as we don't have recursive layouts.

[vouillon]

Would it make sense to eventually have unboxed arrays? Currently, to traverse an automata, we need to dereference two pointers in a sequential manner to go from one state to the next:

type state =
   { final : bool;
     next : state array }

let rec loop s i st =
  let st' = st.next.(Char.code s.[i]) in
  if st'.final then st' else loop s (i + 1) st'

Saving one pointer dereferencing would make this code twice as fast.

I have experimented with manual unboxing in RE (using Obj.magic...) and this can indeed make regular expression matching twice as fast.

[gadmm]

I'm afraid I don't understand your opening paragraph: when you say "How is this different here?", what is "this"? It seems you're suggesting that some aspect of the design is off (please do criticize and brainstorm!), but I'm not exactly sure what it is.

In the meantime, I will react to the counter-proposal:

• If writability is the default, is it still possible to abstract over an unboxed type with an existential variable? It would seem not -- there would have to be some way to say that a certain product is not writable.

• This effectively limits the availability of unboxed types, either preventing the abstract export of some types or placing performance-sapping burdens on the implementation of a type.

• I agree that boxing is one workaround. Yet within some teams within Jane Street, it's an unacceptable one: they need to write code that works without latency-inducing garbage collection. Indeed, the internal feedback I've gotten on this proposal already had two people essentially requesting [@non_atomic] (which perhaps they missed).

Let me try to break my comment down into independent points.

You need a "writable" predicate due to wide existentials (and unboxed variants as a special case). Indeed tearing can cause memory unsafety in this case. Beyond that, you worry more generally about tearing being able to break assumptions about abstract types (tearing a concrete type is OK, an abstract type is not). You introduce a writability restriction to avoid tearing abstract types, and then offer facilities to work around this restriction.

However, a similar hazard already exists with abstract data types without unboxed types. For instance, Stack.push updates the contents and the length separately, which gives rise to values that break the invariant of Stack.t in the case of a race. This is similar to tearing. However, this race does not cause memory unsafety per se. This is regarded as OK. (Only code that use "unsafe" OCaml features, or C code that assumes the invariant, can promote a broken invariant into a memory unsafety, and has to be looked at carefully.) It is also assumed by the Stack module implementation that the caller is responsible for avoiding such races, and this is seen as fine for data types that do not claim thread-safety.

1. Why would breaking abstract type invariants be a greater issue with unboxed types? Can it cause something worse than what races in OCaml can already cause (memory unsafety, or something else)?
2. If the consequences of tearing, with the exception of existentials and wide unboxed variants, are similar to what can already be caused by races in OCaml, then we can explore relaxations of your design that drop the design goal: Even in the presence of data races, a programmer can never observe an intermediate state of a single assignment. Can you think of such alternative designs?
3. One such relaxation I propose is that everything behaves as if annotated with [@writable] (except of course existentials and variants). One goal is to be able to write t.pt <- #{ t.pt with x = 7 } as an alternative to t.(.pt.x) <- 7 as syntax that avoid confusions about aliasing as argued with the three examples in review comments. This also makes the attribute [@writable] superfluous in passing and so it leads to a simpler proposal.

Perhaps at each step I might be missing something simple.

As for [@non_atomic], IIUC it can introduce a form of memory unsafety in case of a race. This is different from other such escape hatches in OCaml, because it is memory-unsafe all by itself in a way that cannot be encapsulated (IIUC), whereas the tricky unsafety coming from the likes of unsafe_get only arises in combination with other code and can be encapsulated. In addition, the use-case is not the one from this PR but a satellite one (avoiding allocations to prevent the GC from triggering inside latency-sensitive code). This looks like a hard pill to swallow; I wonder about two alternatives. One is whether something like the local annotation you have been working on at JS might be used to guarantee the absence of races (as a poor man's lifetime type system) and be required in order to unlock these dangerous assignments (thus much less expressively). Another is whether it is easy to maintain [@non_atomic] in your own compiler branch until some better solution for increasing the crucial expressiveness of GC-free OCaml is figured out (unboxed types surely cannot be the only and one-size-fits-all solution; I have been proposing a different solution to this problem myself).

[goldfirere]

@vouillon

Would it make sense to eventually have unboxed arrays?

Yes, this is in our general plan, but we have not yet written up a design. It is definitely something we're hoping to attack.

[goldfirere]

@gadmm

One aspect of my approach to all of this that is surely leaking through is that I don't consider type safety to be all that interesting a criterion. (Blasphemous, I know.) That is, what I care about is whether my program behaves correctly at runtime. More accurately, I care that my programs have predictable semantics. Whether a tearing is potentially type-unsafe (as in an existential) or potentially invariant-breaking (as in an abstract type) doesn't seem to matter: any problem of this sort can be catastrophic to my program's behavior. And I argue that tearing an abstract type is just as type-unsafe as tearing an existential, because the abstract type's invariants might be relied upon in order to make a call to e.g. Obj.magic safe -- or it might be passed to C code, etc. For me, it all boils down to make me think that treating existentials differently than other records is a distinction without a difference. I know this is not the majority opinion around here, and that's why the proposal does indeed treat these differently, but in all honesty, my heart isn't in it. :)

More concretely:

• Yes, you're right in some sense that unboxed types aren't worse than other features around the possibility for misbehavior around races. The real difference is that the programmer might have to think about an interruptiion in the middle of one assignment instead of between two neighboring ones, but that's not really all that interesting a difference.
• It still seems that your counter-proposal prohibits the possibility of abstracting over existential unboxed types, which are not writeable.
• We are indeed working on a grand plan to avoid data races in general that might subsume this aspect of the design here.
• Yes, we can have [@non_atomic] on our fork of the compiler only; that won't be hard to maintain. But it does limit the possibilities in our open-source libraries such as Base and Core, meaning that external users don't get to take advantage of our features. I'd prefer not to do this.

[gadmm]

@goldfirere I do not think that your first point is controversial, though I would say things differently. Type-safety should encompass abstract types and their invariants; in this sense the OCaml memory model make programs memory-safe without making them type-safe in the presence of races. (Claiming that OCaml 5 ensures type safety in the presence of races, at the cost of changing the meaning of every abstract data type in existence in OCaml 4, to me is not a useful way of seeing things—and I feel like you are trying to say something similar.)

So, OCaml has already chosen a way to deal with such issues, and in particular it is already the case that programmers of an abstract type have the responsibility of avoiding memory-unsafety around unsafe operations (reserved to people who can prove safety)—this is not a new aspect. I am guessing that one purpose of doing things your way might be as a general safeguard mechanism—make the default safer, and the risky configuration opt-in. I find that this is a good goal, and I would like to clarify that to me there is already such a mechanism: the unboxed version of an abstract type is not exported in the interface of the module by default, and the programmer of the abstract type already has to do something explicit in order to make the new races appear.

To say it differently, boiling it down to the technical differences:

1. Non-writability as default (this proposal):
   • An abstract type type unboxed_t : int64 * int64 * int64 can contain an existential, by default these are non-writable and cannot be the type of a mutable record field if > 2 words.
   • But you can write e.g. type unboxed_t : int64 * int64 * int64 [@writable] for when you want to have mutable fields of unboxed type bigger than a word (the compiler rejects this if it contains an existential type).
   • If you use [@writable] then you must be careful not to open the door to memory unsafety via unsafe operations.
2. Writability as default:
   • An abstract type type unboxed_t : int64 * int64 * int64 can be the type of a mutable field of unboxed type; this cannot contain a multi-word existential.
   • But you could have e.g. type atomic unboxed_t : int64 * int64 * int64 (atomic is technically correct terminology, never mind the confusion with Atomic.t at this point). This can contain multi-word existentials, and the compiler will e.g. prevent defining mutable fields of those.
   • The atomic qualifier can also be a tool to encapsulate unsafe operations, and thus lets you export such an abstract type in unboxed form in more situations.

So in practice it is like having the opposite from your [@writable] (I do not think it should be an attribute, but this is an orthogonal issue). This looks like a superficial difference, yet:

• With the no-tear principle (the intermediate steps of single assignments must never be observed), you give both the author of an abstract type and its user an overlapping duty of avoiding data races. Concretely, when the user of a module sees an abstract unboxed type, they might legitimately want to use it writably, aware that they must strive to avoid data races (like they already have to do with all non-thread-safe abstract types, after all). If the type is not annotated as writable, they will not know if this is by default or really needed for memory-safety (on the chance that the module makes C calls, or uses unsafe operations, or hide existentials). In this scenario, the overlapping of duties might translate as the user filing an issue with the author to please add [@writable] if you do not mind and the author agreeing. A way to resolve this overlap of duty would be to recommend a "best practice" of always adding [@writable] if possible... thus defeating the design. Or you decide to make it a rule that the programmer of an abstract type who wants to use [@writable] has to always uphold the no-tear principle. But in this case the no-tear principle is not at all a guarantee of your proposal, but an additional rule that you impose on programmers that considerably complicates programming with unboxed types—such a requirement is not even required for non-unboxed mutable data structures because it would be impractical or costly, and the situation is similar. Even if the data structure is not meant to be thread-safe, their programmers will have to reason about possible races even when they do not use unsafe operations. So I reject this principle.
• We can ask: “could a first version be with writability as default (2.) but without this atomic & unboxed-abstract-existentials?—they could be introduced later if experience showed it necessary.” It is indeed possible, and a more elegant design, to force boxing the atomic-but-bigger-than-a-word sub-part of the data. I do not say that atomic is not useful, nor that it should not be present at the start, rather that this could be discussed separately, understood that it is an extension, with its own experience reports to defend its necessity, to understand the cost/benefit ratio. (The converse, having no restriction on existentials but no writability either, would also be possible and elegant, but less useful.)

(Thanks for your careful replies, this forced me to read the proposal better and I came out of it with a better understanding. I am now satisfied by how we have explored this aspect; I think the two above points in bold summarize my remark.)

Please do not hesitate to point out if there are points of the proposal which I might have misunderstood, I still do not claim to have it fully in my head.

The next important point to discuss is the weird syntax t.(.center.x) <- ... and try to find something better (I now think this is a distinct concern).

[goldfirere]

Aha -- I think I now understand the crux of the issue: defaulting. Defaulting is always hard. My syntax suggests unwriteable as the default, while users can opt-in to writeable. I have no evidence this is the better design. Indeed, another possibility is to have no default, requiring e.g. * for writeable products and & for unwriteable ones. I'm also fine with having writeable as the default and then some way to state something is unwriteable. Is this the part you're most concerned with?

Agreed about the poor t.(.center.x) <- ... syntax; happy for concrete suggestions there.

[gadmm]

Another aspect that is worth clarifying in the meanwhile (implicit in my text)—the no-tear principle (the intermediate steps of single assignments must never be observed): is it something you throw away when you introduce [@writable], or a principle that you want to add to the language and ask programmers to uphold?

[goldfirere]

Another good point: that principle is poorly stated, in that the design does not uphold the principle as stated -- precisely because of [@writable]. So perhaps this would be more accurate (though somehow less satisfying):

• Even in the presence of data races, a programmer can never observe an intermediate state of a single assignment, unless either of these two exceptions applies: the definition of the field assigned to includes [@writable] or the assignment includes [@non_atomic].

This captures @gadmm's worry about joint responsibility. Either the type author or the type user can cause an exception to the rule. I think that this is the right design (though I'm quite up for debating concrete syntax and defaults!) because it is the most expressive. A library author can declare that they don't care about tearing (because they protect against the possibility somehow) or a library user can declare that they don't (because they use external synchronization techniques). Both of these scenarios happen in practice, so it should be possible to accommodate both.

[gadmm]

But then this principle is no longer what programmers need to hear to understand the unboxed design. If we agreed leave this principle aside, I agree that it is (finally) a matter of defaults:

Either the type author or the type user can cause an exception to the rule. I think that this is the right design (though I'm quite up for debating concrete syntax and defaults!) because it is the most expressive. A library author can declare that they don't care about tearing (because they protect against the possibility somehow)

But precisely we do not want to ask type authors in general to care about or protect themselves against tearing (except for unsafe operations).

In addition to existential and unsafe operations, you seem to envision making a type non-writable as part of a wider arrangement for enforcing some thread-safety guarantee in some situation. I agree that this is a good reason to use it (example: unboxing mutexes). But again those thread-safe-yet-unboxed data structures are the exception rather than the rule.

or a library user can declare that they don't (because they use external synchronization techniques). Both of these scenarios happen in practice, so it should be possible to accommodate both.

Our deconstruction and rephrasing efforts made me eventually understand this point better. For programmers of an abstract type t2 re-using an abstract unboxed atomic type t1, it makes sense to me to have some [@unsafe-assert-atomic-assignment] to allow assignment of atomic types when the programmer is in position of encapsulating this unsafety (here via some external synchronization technique).

[goldfirere]

But precisely we do not want to ask type authors in general to care about or protect themselves against tearing (except for unsafe operations).

I agree! This is why I thought non-writable should be the default, so library authors who don't think about it are protected from the possibility of tearing. Only those authors who opt in will care. Library users who use [@non_atomic] will be playing with fire and are responsible for wearing the appropriate gloves. (I'm happy to make [@non_atomic] sound scarier, like [@unsafe_non_atomic] or even worse.)

[gadmm]

But do you understand why with the same starting point I conclude in favour of having the opposite default, or is there still something I should clarify?

[gadmm]

Syntax for mutable unboxed record update

As discussed above, I understand that with t.(.center.x) <- ..., you mean something like t.center <- #{ x = ... }. Let's explore precisely this syntax, with the idea that you have a partial record where you have holes wherever undefined.

Let's see how it goes in the original text:

---

type point = { x : #int32; y : #int32 }
type t = { radius : #int32; mutable center : #point }

[...]

Fields within a mutable unboxed record within a boxed record.

[...]

We thus introduce a new syntax for updates of individual fields of a mutable unboxed record: We write e.g. t.center <- #{ x = ... } where the R-value does not have all fields defined. Undefined fields are guaranteed not to be touched by the assignment.

Nested partial unboxed records are allowed, which can be used to update a sub-sub-field: t.unboxed_field <- #{ x1 = #{ x2 = ... } } (more verbose, but no need to explain or remember a rule for paths).

[...]

Further discussion: mutability within unboxed records

[...]

type point = { x : int; y : int }
type t = { mutable pt : #point }
let () =
  let a : t = { pt = #{ x = 5; y = 6 } } in
  let pt = a.pt in
  let foo () = print_int pt.x in
  foo ();
  a.pt <- #{ x = 7 };
  foo ()

Here it is clear that you do not mutate a.pt.x, you mutate a.pt, so no confusion possible.

type t2 = { x : #int32; y : #int32 }
type t1 = { mutable z : #t2; other : int }
fun (a1 : t1) ->
  let other_a1 : t1 = {a1 with other = 5} in
  a1.z <- #{ x = #10l };
  other_t1.z.x = a1.z.x

Again no confusion happens: you mutate a1.z, not a1.z.x, so you do not touch the previous copy.

[End of RFC text]

---

Slightly-more-than-informal description

Partial unboxed records can be allowed following a simple syntactic criterion. You define recursively a notion of partial R-value (PR-value) where:

• A partial unboxed record is a PR-value
• A PR-value is only allowed on the right-hand-side of <-, or as a defining field of a PR-value.

A single assignment of a PR-value is elaborated by the compiler as a sequence of assignments of the form (in your syntax)

t.(.x.a) <- e1;
t.(.x.b.c1) <- e2;
t.(.x.b.c2) <- e3;
...

As an implementation detail, this has to rely on re-using type-directed disambiguation to detect partial records. I am not familiar with this part of the compiler, so I will refrain from making comments about how easy to implement it is supposed to be. (I am ok with a reply along the lines: “that looks complicated to implement!”)

(My guiding intuition was that partial fields have a sub-layout where the location of the holes are replaced with primitive kind undefined. But this leads to some kind of first-class treatment of partial unboxed records, and I do not want that.)

FAQ

• Is this notion of PR-values not restricted and artificial? You already have something restricted and artificial in OCaml's notion of L-values. It also has to be compared on these aspects to the notation t.(.x.a.b) <- ....
• What about partial boxed record assignments? The value-layout specialization of a PR-value assignment is either a plain assignment, or no assignment at all. So this notion of PR-value does not result in an addition to the base language.
• Is there not a risk that adding a field to a record results in assignments turning into partial assignments instead of failing on locations that have not been correctly updated? This is true, this is why you actually need an explicit distinction in the syntax, e.g. t.center <- #{ x = ...; _ }.
• Is this not too many characters to type? We are looking for a loud syntax in the first place, and it also gets more economical when updating several fields at once, and when using record field punning.

[goldfirere]

But do you understand why with the same starting point I conclude in favour of having the opposite default, or is there still something I should clarify?

I'm afraid to say I don't. The starting point of "library authors should not need to care about the possibility of tearing" would seem to lead directly to "don't allow tearing by default", whereas I understand you are advocating for allowing (non-existential) tearing by default.

syntax suggestions

This alternative scheme indeed seems (to me) more complicated than what I proposed. Syntax debates are challenging, because they often come down to taste. I expect this all to get refined over the course of time, as we roll out these features within Jane Street and then engage in further discussions with the broader OCaml community. In all honesty, I don't think engaging in this debate now will yield much fruit. Instead, let's wait to see this all in practice, recalling that it is easy within Jane Street to choose one syntax and then change it later. Let's take advantage of this to learn from experience.

closure capture

Hm. Interesting. I think you're suggesting that we needn't copy an unboxed value in a closure capture if the closure is local (as a great many are). I think that's a good idea. I will check in with my colleagues about this one.

[lthls]

Hm. Interesting. I think you're suggesting that we needn't copy an unboxed value in a closure capture if the closure is local (as a great many are). I think that's a good idea. I will check in with my colleagues about this one.

If @gadmm is referring to functions annotated with the [@local] annotation, then there's no issue because there's no closure at all (the [@local] optimisation transforms functions into static exceptions). But it's very different from Jane Street's local allocations, which behave like regular allocations as far as unboxed types are concerned.

I think there's room for discussing how closure capture works for non-value layouts though. The normal, straight-forward way is to capture variables, so fun () -> p.x captures p and its whole layout. But if we translate variables of non-simple layouts into multiple variables of simple layouts early enough, then we could consider that p is actually a collection of variables p:foo (tentative syntax), and replace all occurrences of p.x by the unboxed tuple of all its components (a single p:x if x has a simple layout). Then the closure only needs to store p:x. My preference is for the straight-forward implementation. It's much simpler to specify and implement, and one can still optimise it in later passes of the native compiler. But if the performance of the bytecode becomes important enough, we may have to use the trickier implementation.

[gadmm]

@lthls I was indeed thinking about Stephen and Leo's local_ presented at the OCaml workshop, which is similar to Scala's second-class values. But [@local] is a good example where it already makes sense to allow mutations.