Proposal: constructor unboxing

[yallop]

[I've replicated the proposal in this comment for ease of reading.]

Constructor unboxing

Motivating example: compact rope representation

Data structures defined in OCaml are often less compact than they might be, because of boxing.

For example, here is a type for representing ropes:

type rope = Leaf of string
          | Branch of { llen: int; l:rope; r:rope }

With this definition the value Branch {llen=3; l=Leaf "abc"; r=Leaf "def"} has the following representation:

[--B|-3-|-∘-|-∘-]
         /     \
        /       \
       /         \
      [--L|-∘-]   [--L|-∘-]
           /             \
          /               \
         "abc"             "def"

In the general case each part of this representation serves a purpose. For example, in order to distinguish Leaf nodes from Branch nodes at run-time, each constructor is represented by a tagged block. However, for this particular data type the block representing Leaf nodes ([--L|-∘-]) is unnecessary; since strings are already distinguishable from other blocks, the value could in principle be represented more compactly:

[--1|--3|-∘-|-∘-]
         /     \
        /       \
       /         \
       "abc"      "def"

The basic idea

Adding an [@@unboxed] annotation to a variant definition indicates that the representation of unary constructors should not involve an additional block:

type rope = Leaf of string
          | Branch of { llen: int; l:rope; r:rope } [@@unboxed]

Only a subset of variant definitions support [@@unboxed]. In particular, it must be possible to distinguish the arguments of unary constructors from each other (and from constant constructors in the same definition) at run-time. For example, the following definition is not allowed, since the arguments of X and Y have the same representation:

type strings = X of string | Y of string [@@unboxed] (* Invalid! *)

Performance improvements

Since the unboxed variant representation uses less allocation and less indirection, it improves performance in some cases.

For example, here is a simple benchmark for the rope data type. The benchmark creates rope representations of size n, converting the ropes to strings in a final step:

  let rec build n =
    if n = 1 then leaf "a"
    else let llen = succ (Random.int (pred n)) in
         branch (build llen) (build (n - llen))
  in
    string_of_rope (build n)

Measurements show substantial improvements for the unboxed representation, especially for larger values of n:

Size	Boxed (μs)	Unboxed (μs)	Unboxed %
2^6	3.90	3.81	97.7
2^8	15.99	15.38	96.2
2^10	64.82	62.32	96.1
2^12	281.13	257.30	91.5
2^14	1560.99	1220.11	78.1
2^16	10089.72	5332.93	52.9
2^18	50027.06	35030.16	70.0

(These measurements were taken by building the unboxed representation explicitly using Obj rather than actually implementing this proposal in the OCaml compiler.)

Which types are distinguishable?

Eliminating the block associated with a constructor is safe only when:

1. the representations of distinct constructors remain distinguishable at run-time
2. no type can represent both non-float and float values (to avoid problems with the float array unboxing optimization)

This proposal currently focuses on concrete types; it may be extended to abstract type constructors and existential variables by building on the notion of separability introduced in Unboxing Mutually Recursive Type Definitions in OCaml (Colin, Lepigre, Scherer, JFLA 2019).

Consider the definition of a data type t with unary argument types t1...tn and constant constructors C1...Cn:

type t = C1 | ... | Cn | T1 of t1 | ... Tn of tn

The simplest case where constructor unboxing is clearly safe is where t1...tn all have non-immediate and distinguishable representations, and none of them is either float or t.

However, constructor unboxing is also possible if some of the t1...tn have immediate representations. For example, consider the following definition:

type u = C1 | C2 | C3 of bool | C4 of char

In OCaml C1, C2, bool and char are all represented as immediates, and a single immediate value (i.e. an int) can easily represent all of these values. We can therefore adopt the following representation:

Value	Representation
C1	0
C2	1
C3 false	2
C3 true	3
C4 c	4 + Char.code c

More generally, we can unbox the definition t if:

• the block-representations of t1...tn are all disjoint (and distinct from float and from t for non-unary constructors)

• the immediate-representations of t1...tn together with C1...Cn cover less than the immediate space.

(Here block-representation indicates the set of tags that non-immediate values of a type can have, and immediate-representation indicates the number of distinct immediate values of a given type. Covering less than the immediate space means that the sum of the immediate representations of t1...tn is less than max_int.)

How does this relate to the existing [@@unboxed] annotation?

This proposal is a conservative extension of the existing [@@unboxed] annotation (PRs #606, #2188). It has no effect on existing code, and the extended meaning of [@@unboxed] is compatible with the existing meaning.

How does this relate to the existing proposal for unboxed types?

Another open proposal involves unboxing field types into parent types --- for example, producing flat representations of int32 pairs:

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

The two proposals are distinct, but complementary. The field-unboxing proposal does not support the compact rope representation, the current proposal does not support pair unboxing, and the combination of the two proposals can support representations that are more compact than either proposal supports in isolation. In the following example, the int32 arguments are unboxed into a single block using field unboxing, and the block associated with the Pair constructor is eliminated using constructor unboxing:

type t = { x : #int32; y : #int32 }
type topt = Nopair | Pair of t [@@unboxed]

Without any support for unboxing, the value Pair {x=0l; y=0l} involves 4 blocks; with field unboxing alone it involves 2 blocks; with constructor unboxing alone it involves 3 blocks; with both field and constructor unboxing it involves 1 block.

(There are some additional connections and distinctions between the two proposals. The current proposal can be seen as a generalization of the nullable types mentioned in the field unboxing proposal. And the field unboxing proposal is more ambitious: it additionally introduces compound unboxed types and changes to the type system to combine unboxing with abstraction.)

Extension: partial unboxing

The current proposal requires all unary constructor arguments to have distinguishable representations. It might also be useful to support the case where only some of the arguments are distinguishable by allowing per-constructor unboxing specifications.

Comment: abstraction

Unboxability (for records) is a property of a single type, and is fairly straightforward to abstract.

However, separability is a relation between types, and is not so easily abstractable.

One possibility is to optionally expose the immediate-space and the tag-space of abstract types by extending the [@@immediate] attribute. For example, we might promise that a type has an immediate representation with no more than 256 distinct values:

type t [@@immediate 0..255]

We might additionally support setting the tag value associated with particular constructors explicitly to avoid clashes:

type t = { x: int; y: float} [@@tag 240]

[stedolan]

I like this proposal, and these are definitely optimisations I want to be able to express. However, I think that there are two separate optimisations being proposed here which I'll call inlining and disjointness, and I think it's worth considering the two independently, rather than conflating them with the immediate/block distinction as this proposal currently does.

Inlining and disjointness

Inlining combines the constructors of different types into a single sum representation. Given:

type ab = A | B
type cd = C | D
type u = Foo of ab | Bar of cd [@@unboxed]

this proposal inlines the definition of ab and cd into u, giving u the same representation as currently given to:

type u = Foo_A | Foo_B | Bar_C | Bar_D

Inlining amounts to reasoning about sum types modulo associativity, transforming (A + B) + (C + D) into A + B + C + D.

Disjointness represents certain constructors of different types as the identity, when this introduces no ambiguity. Given:

type ef = E of int | F of int * int | G
type t = Stuff of ef * int | Num of float [@@unboxed]

this proposal represents the Num constructor as the identity, on the basis that its values are represented using Double_tag which collides with none of the other possible values. This type is not currently expressible in OCaml, but its values are exactly the values represented by either of these two types:

type t1 = Stuff of ef * int
type t2 = float

Disjointness amounts to transforming A + B into A ∪ B, when A and B do not overlap.

This proposal

If I understand correctly, this proposal currently operates on type definitions type t = C1 of ... | C2 of ... | ... [@@unboxed] by:

• selecting all of the single-argument constructors Ci with arguments ai
• applying inlining to the immediate values of the types ai
• applying disjointness to the block values of the types ai

I don't think that this immediate = inlining, block = disjointness split is natural, and it makes two otherwise-orthogonal optimisations less useful. For instance:

• Inlining blocks A slight variant of the type u above is:

type ab' = A of int | B of int
type cd' = C of int | D of int
type u' = Foo of ab | Bar of cd [@@unboxed]

The inlining optimisation is just as applicable and just as useful as before. I would like to represent u' as though it were:

type u' = Foo_A of int | Foo_B of int | Bar_C of int | Bar_D of int

However, upon seeing block constructors, the currently proposal switches from inlining to disjointness, which fails as the types ab' and cd' are not disjoint.

(The converse, applying disjointness to immediates, does not appear to be useful. It is very difficult to construct two immediate types that are disjoint, as all immediate types tend to assign a meaning to 0).

• Multi-argument constructors The single-argument restriction is necessary for disjointness but irrelevant for inlining. For instance, we could still inline the types ab and cd below:

type v = Two of ab * cd

by representing it as though it were

type v = Two_A_C | Two_A_D | Two_B_C | Two_B_D

(This amounts to reasoning about distributivity of products over sums, as well as associativity of sums)

• Partial unboxing As mentioned in the proposal itself, it would be useful to be able to specify particular constructors to unbox. In particular, this allows unboxing of the type strings mentioned above, by unboxing either (but not both) of the arguments.

So, with this in mind, might it not make more sense to have separate annotations for inlining (per-field) and disjointness (per-constructor), rather than a single per-type [@@unboxed] annotation? In particular, I suspect the #t syntax from #10 could be reused for inlining, as it's essentially the same (or dual) optimisation.

Abstraction

The distinction between inlining and disjointness reappears when considering abstraction. Inlining requires no notion of "separability" - whether something can be inlined depends only on its layout, and is exactly as hard as inlining records in the manner proposed in #10. (Well, I imagine the implementation will be more work, as there's the pattern-matching compiler to worry about)

Separability arises only for disjointness optimisations. While a precise analysis of disjointness does require a binary relation between types (which as mentioned above is annoying to abstract), a simple approximation seems to get most of the value of this relation.

We can introduce a new layout (i.e. kind) describing those types whose block values do not lie in the tag space used for datatype constructors. This layout includes types string, float, int32 and so on. The disjointness criterion than then allow at most one constructor with such a type to be represented as the identity.

This is a very coarse approximation. However, it suffices to accept all of the motivating examples in this proposal. (Finer approximations are also possible. For instance, having separate layouts for string and float tags would allow both a string and a float constructor to be simultaneously unboxed via disjointness)

[gasche]

The way I think of it, constructors type foo = ... | Bar of bar denote an embedding of bar into foo that gives distinguishability (from other constructors) -- initiality / an elimination principle / the ability to pattern-match. The syntactic piece of data Bar(...) may be realized in various way in low-level representations; the default to create a new block with a constructor tag chosen for distinguishability from other constructors of t, but any other embedding is acceptable as long as distinguishability is preserved.

Single-constructor unboxing uses exactly identity (of low-level representations) as the embedding functions. This is also what's going on with what Stephen calls "disjointness", but not with "unboxing": with unboxing, the values are changed by the embedding: in the example of Jeremy where booleans are inlined, false, true become 2, 3 (this shifting is the computational content of the embedding).

Embeddings are restricted by the fact that they must preserve identity of mutable state: "inlining" may not be possible if the argument of the constructor to inline is a record with mutable fields.

[yallop]

Here's another example where this would be useful: Z.t values in Zarith are either immediate integers or custom blocks. Both the type itself and (consequently) much of the implementation is currently written in C; with this proposal it'd be possible to express the type definition in OCaml without changing the representation:

type t = Small of int | Large of mpz_t [@@unboxed]

[chambart]

The FFI story is not obvious here. We might want the compiler to be allowed to be as clever as possible as soon as the user ask for unboxing (or any other kind of change in representation). Maybe we should just say that the representation is not fixed in that case and this type is not fit for FFI (or can only be manipulated as an abstract type on the C side). A warning triggering whenever that kind of type can reach a C function would be nice. Such a warning would probably be neither correct nor complete but for obvious cases it could still probably help.

[chambart]

There is also another question that arise with that kind of performance related annotations. How do user discover about that kind of features ? Should there be a mode where the compiler suggest what transformation could be possible ? Something like that would require an non local analysis (you need to annotate some other mlis than the one you are looking at to know that something is possible)

[chambart]

As a last comment, the notion of separability might not be as stable as one could assume. There is some work going on to try to compile OCaml to webassembly. Such a backend has less control on the shape of values and in particular might not have tags for float or string values.

[garrigue]

A few comments coming from my partial understanding of this proposal.
My impression is that indeed there are two different problems, separability and compression of "constant" cases into a word. Separability is clear enough, eventhough its is hard to make it prescriptive. The compression part could potentially do more. In both cases, my impression is that the behavior should be either specified by the programmer explicitly (using multiple annotations), or seen as a black box (even if the algorithm is public).

[garrigue]

I'm not sure about the original specification "should not involve an additional block", and what it is supposed to reject.
For instance, for the following

type 'a or_int = Ret of 'a | Err of int [@@unboxed]

it is possible to unbox Err but clearly not Ret, so will it be accepted?

In general, should [@@unboxed] be seen as prescriptive or suggestive.
If it is prescriptive, wouldn't it be better to annotate each constructor individually, meaning that both

type strings = X of string [@@unboxed] | Y of string

and

type strings = X of string | Y of string [@@unboxed]

would be valid, but not

type strings = X of string [@@unboxed] | Y of string [@@unboxed]

Otherwise, it could be just suggestive, meaning "attempt to flatten the type as much as possible".
We might still want a warning when nothing is done.

[garrigue]

What I suggested above is already proposed here.
Actually, I find the special handling of unary constructors confusing.
All the more when you think of types such as

type t = A of {x: int}

One could also want to flatten n-ary constructors:

type variance = V of bool * bool * bool [@@unboxed]

[gasche]

Thinking more about this as well:

• I like the general idea of the proposal, and I think that being able to write type zarith = Small of int [@@unboxed] | Large of mpz_t is a killer application.
• I would prefer if the [@@unboxed] attribute was per-constructor rather than global. (This was also hinted at by @garrigue.) The meaning of each [@@unboxed] is that this constructor is represented as runtime by a no-op, because the payload is disjoint from all other values of the type.
• Reusing @stedolan's distinction between inlining and disjointness, I would concentrate on the "disjointness" part for a minimal version of the RFC, without playing with "inlining" (of a sum type into another sum type) at first.

[gasche]

• When we do inlining, I would prefer if we manually specified the representations of the constructors, instead of letting the compiler perform an implicit transformation. The unboxing step itself would preferably remain the identity, to avoid copy effects.

For example I would not be in favor of either

type cd = C | D of int
type abcd = A | B | CD[@unboxed] of cd
(* Bad: not explicit enough on representations *)

type cd = C | D of int
type abcd = A | B | (CD of cd [@unboxed function C -> 2 | D -> 0])
(* Bad: (function CD x -> x) allocates *)

but I would be happy with either of those clearly-disjoint declarations:

type cd = C | D of int
type abcd = A [@repr 1] | B [@repr 2]  | CD [@unboxed] of cd

type cd = C[@repr 3] | D of int
type abcd = A | B  | CD [@unboxed] of cd

[gasche]

@chambart : two answer two of your questions

• I propose to avoid implicit transformations where the compiler "finds a representation such as X", but instead favor explicit annotations that contain, when necessary, annotations on which representation to use. In particular, this clearly specifies a FFI story, just like [@@unboxed] does: expert users have to specify the representation of OCaml values to use these annotations (no guessing from the compiler), and they can also use the C FFI to manipulate them.

• The whole idea of attributes is that different consumers of the code could interpret them differently. js_of_ocaml or wasm_of_ocaml may not use some of the unboxing attributes, and I think that this is fine. OCaml has a high-level semantics where those attributes are ignored, and (several) low-level semantics where we think about value representation, observing allocations etc., and the latter may differ among realizations of the language.

[diremy]

* I would prefer if the `[@@unboxed]` attribute was per-constructor rather than global. (This was also hinted at by @garrigue.) The meaning of each `[@@unboxed]` is that this constructor is represented as runtime by a no-op, because the payload is disjoint from all other values of the type.

I fully agree with @garrigue and @gasche : the annotation should be per constructor so that the user knows exactly which constructors are omitted, and the compiler never chooses which of two constructors should be omitted.

[lpw25]

OCaml has a high-level semantics where those attributes are ignored

Note that this is not entirely the case because the representation needs to be taken into account when checking implementations against interfaces. I think this is still all fine -- it just means that your code needs to obey the rules of the native OCaml representation even when you are actually compiling it to JavaScript.

[alainfrisch]

The whole idea of attributes is that different consumers of the code could interpret them differently. js_of_ocaml or wasm_of_ocaml may not use some of the unboxing attributes, and I think that this is fine. OCaml has a high-level semantics where those attributes are ignored, and (several) low-level semantics where we think about value representation, observing allocations etc., and the latter may differ among realizations of the language.

Sure, but we might have a problem with js_of_ocaml if it needs to have a different interpretation of the attributes than the bytecode compiler (since, well, it is "just" a postprocessing on its output).

[gasche]

In a sense the point is that if a given compiler pass makes choices based on assumptions on runtime value representations, then only OCaml implementations that satisfy those assumptions can safely reuse this compiler pass. Adding low-level features to the surface language that are based on those assumptions means that those assumptions are now made earlier in the pipeline, and they could in general invalidate design choices of some implementations branching from the main compiler after some passes.

In general if the problem arise we always have the option of having a flag to not perform the representation change during compilationoptimization. js_of_ocaml (or wasm_of_ocaml) would then compile using this flag for the lower passes.

For this optimization for js_of_ocaml, I don't foresee a problem. If I understand correctly, js_of_ocaml stores the tag of blocks, uses JS closures for closures (and I expect we can distinguish them from arrays by introspection). It uses javascript "numbers" (float, I presume?) for both integers and floats, but I expect that numbers represent unboxed floats, and that boxed floats still carry their type around. (In any case we don't allow unboxing floats so this should be safe, but the same question could apply to say int versus Int64.t in a runtime that would not box Int64.t.)

[alainfrisch]

One should ask people who knows better about js_of_ocaml (ping @hhugo), but I believe floats are indeed unboxed. And one could imagine (if it's not already the case) that int32 would also be represented with Javascript numbers (so, cannot be distinguished from int and floats, contrary to OCaml).

It's certainly possible to tell ocamlc to not perform the representation optimization when the result is intended to be fed to js_of_ocaml, but then we lose the ability to reuse existing .cma libraries compiled for "normal" use. I'm not saying this is an argument against the optimization (which I like very much), but we need to take that into account (perhaps the conclusion is that js_of_ocaml should introduce its own file suffixes, not reuse .cmo/.cma, and explicitly requires re-compilation; a bit more like Bucklescript, I guess).

[Lupus]

perhaps the conclusion is that js_of_ocaml should introduce its own file suffixes, not reuse .cmo/.cma, and explicitly requires re-compilation

This sounds pretty inconvenient for users that have single codebase targeting both native and js (via jsoo), especially when depending on heavy packages like core-kernel. Switch rebuild takes considerable amount of time, and above suggestion will effectively double it.

[gasche]

My understanding is that the part of the build that would need to be duplicated (parsing, type-checking and bytecode compilation) takes only a fraction of the time, compared to either native-code production or jsso optimizations and javascript production. I picked a single module (tool/ocamlprof.ml from the compiler distribution), producing the .cmo takes 0.070s on my machine (0.060s from typing), producing the .cmx takes 0.120s on my machine (again 0.060s from typing), calling jsoo on the .cmo takes 0.140s. If you want a switch that installs jsoo modules for all packages, today building this module would take 0.330s (0.070s + 0.120s + 0.140s), tomorrow the .cmo-production step would be duplicated so it would take 0.400s. This is far from a doubling of compilation time.

[gasche]

Of course this could be reduced further by, say, having an intermediate output for the typedtree, so that all three builds (.cmx, .cmo, .js) could reuse it. Then the build time would go down from 0.330s today to 0.280s.

[lpw25]

My understanding is that the part of the build that would need to be duplicated (parsing, type-checking and bytecode compilation) takes only a fraction of the time, compared to either native-code production or jsso optimizations and javascript production.

I would just like to point out that this is not at all accurate on Jane Street's code base. Type checking is comfortably the largest cost in compilation.

I don't think it is particularly relevant to this discussion though, because I think that needing to use different front-end options for js_of_ocaml is both unnecessary and not really a viable suggestion. A better option is to keep the constructors and destructors of these unboxed constructors until later in the compilation pipeline so that exotic back-ends can decide whether to unbox or not based on whether the representations are actually separated on that platform.

[alainfrisch]

A better option is to keep the constructors and destructors of these unboxed constructors until later in the compilation pipeline so that exotic back-ends can decide whether to unbox or not based on whether the representations are actually separated on that platform.

js_of_ocaml currently parses .cmo files; do you mean that we should propagate explicitly the "constructors/destructors" down to the bytecode level? That doesn't sound right. Keeping the information up, to, say, the lambda level would make sense, but then one would need to dump the lambda code and have js_of_ocaml starts from there (as Bucklescript does, IIUC).

[dbuenzli]

This is a bit tangent to the discussion but regarding js_of_ocaml I wouldn't like it to add its own compilation objects. There's already quite a menagerie of compilation objects in the eco-system and starting from bytecode has the following good properties:

1. Suppose you have a pure OCaml library you install via opam. The author of that library is not interested in js_of_ocaml and doesn't support it in its build system. Yet you can just install the library and use it in your js_of_ocaml project. No need to go bother that author or fiddle to have your opam switch/packages build in a different way.
2. I don't know where Bucklescript starts but it's notoriously lagging behind OCaml versions. Starting from bytecode offers a relatively stable interface to the compiler's outputs which seemed to have enabled js_of_ocaml devs to cope with OCaml development without too much work.

I think that for js_of_ocaml to start from bytecode is a very good call both from a usability and maintenance perspective.

[jordwalke]

Regarding jsoo:
It might be the case that that most of the proposals here are compatible with jsoo, with only a smaller subset of them requiring more thought.

When compiling to JS, Strings will always have some way to be distinguished at runtime. Even if jsoo's string implementation removes the boxing around strings by default (JS engines always provide a type tag to check strings).

Even some of the proposed optimizations around partitioning an integer range (bool/char etc) across a set of variant constructors seems like it wouldn't cause problems (so long as the bytecode includes all of the information for renormalizing their values when they leave their "constructors").
The only thing that seemed like a potential problem for jsoo was any optimization that relies on floats always being reliably tagged at runtime. Right now floats are not, and it does cause some compatibility issues, though for a JS target it is a welcome tradeoff because you don't want to have to pay the price of allocating boxes around floats, on top of the price of the VM's NaNboxing at runtime (which most engines do).
Is it perhaps a good idea to avoid any optimizations that rely on the runtime representation of floats - not just for jsoo's sake, but to make it easier to later change the representation of floats in OCaml itself?

On the other hand, if all the other optimizations mentioned are compelling enough, maybe it would be worthwhile to add boxing around floats in jsoo in order to get them. It would solve some of the compatibility issues that jsoo currently has with floats (unmarshaling). For perf sensitive applications, applications could explicitly use an unboxed Js.float.

Either way, it would be nice if jsoo could take advantage of all of the optimizations that do easily apply to jsoo's compilation approach. Does it need to be all or nothing?

[jordwalke]

Regarding jsoo-specific compiler artifacts: I think this has the potential to cause compatibility, reliability, or even fragmentation issues within the ocaml ecosystem. jsoo's strength is that it is ocaml ecosystem compatible, and unless you use native C bindings, your packages more or less work well when compiled with jsoo. Importantly, packages that you depend on don't need to anticipate being compiled with jsoo, or do anything special. They don't even need test the jsoo workflow.

[gasche]

Note: currently choices based on the representation (or not) of constructors are made during the translation from Typedtree to Lambda, in particular during pattern-matching compilation. If we wanted to keep the Lambda representation-agnostic, we would need to use higher-level makeblock and switch constructs (with constructors instead of constants and tag values), which would only be lowered later (as we do for string switches currently). This is possible, but a sizeable refactoring, sensibly more work I suspect than implementing the corresponding part of the proposal.

[jhjourdan]

@gasche and me discussed about coq/coq#12733 and found that this RFC would be an elegant solution to this problem. Essentially, they would need an ability to discriminate over the closure tag in an OCaml pattern matching (Obj.tag is too slow for this application, so this is not an option here). (A small extension of) This RFC makes this possible by allowing to unbox functions in an ADT. (A subtlety is that if we allow to unbox functions, then the corresponding constructor would correspond to two tags --the closure tag and the infix tag--, but that does not seem to be really complicated to handle.)

The way the Coq folks solved this problem in the past is by changing the tag of the closure to 0 so that this special kind of closures (accumulators) had the same tag as a special ADT constructor which was easy to discriminate using a pattern matching. However, this is not compatible with the new closure representation in no naked pointers mode, hence they need a new solution.

[silene]

As far as I understand, for this proposal to be useful for Coq, the unboxed attribute would need to be per constructor. Also, this is not just an optimization in the case of Coq, as the program would instantly crash (hopefully), if the compiler decided to ignore the attribute and put an indirection. That said, ultimately, the tag attribute is much closer to the semantics Coq expects.

Currently:

type ind_foo =
  | Accu_foo of t (* this constructor is a lie, just to make sure that tag 0 is free for storing a closure *)
  | Construct_foo_0 of t * t * ...
  | Construct_foo_1 of t * t * ...
  | Int_foo_0
  | Int_foo_1

With unboxed:

type ind_foo =
  | Accu_foo of t -> t [@@unboxed] (* the actual type of the closure is infinite: t -> t -> t -> ... *)
  | Construct_foo_0 of t * t * ...
  | Construct_foo_1 of t * t * ...
  | Int_foo_0
  | Int_foo_1

With tag:

type ind_foo =
  | Accu_foo of t [@@tag 247] (* the type is still a lie, but the intent is clear *)
  | Construct_foo_0 of t * t * ...
  | Construct_foo_1 of t * t * ...
  | Int_foo_0
  | Int_foo_1

[jhjourdan]

As far as I understand, for this proposal to be useful for Coq, the unboxed attribute would need to be per constructor.

Indeed, you would need some way to do a fine-grained control of which constructor is unboxed. Perhaps this could be done by choosing well the content of the other constructors?

That said, ultimately, the tag attribute is much closer to the semantics Coq expects.

@silene : if such a tag attribute were implemented, then it is very unlikely that the closure tag will be allowed at this place, since the GC expects some particular memory layout when it sees the closure tag.

| Accu_foo of t -> t [@@unboxed] (* the actual type of the closure is infinite: t -> t -> t -> ... *)

If t -> t -> t -> ... is really your intent for the inner type of the constructor, you can still define type u = (t -> u) with -rectypes But note that this is (again) a lie since the accumulator can be used as a constructor even in the future.

[silene]

Indeed, you would need some way to do a fine-grained control of which constructor is unboxed. Perhaps this could be done by choosing well the content of the other constructors?

None of the other constructors takes a function as an argument, so I guess this is fine. In the end, the compiler can unbox any constructor it wants, as long as Accu_foo is guaranteed to be unboxed and a constructor Constructor_foo of t is guaranteed not to be. The latter could be avoided by turning t into t * t, but that would have a non-negligible memory footprint.

if such a tag attribute were implemented, then it is very unlikely that the closure tag will be allowed at this place, since the GC expects some particular memory layout when it sees the closure tag.

That is the whole point, isn't? Coq is being mentioned in this discussion precisely because OCaml's GC will soon expect some specific layout for (non-)closuresclosures, so Coq can no longer create closures with tag 0.

But if you are concerned with safety, the solution would be for the compiler to forbid the use of Accu_foo for creating values or anything other than a wildcard for pattern-matching. Note that this is perfectly fine with Coq, since the only occurrence of the constructor is in the construct match Obj.magic x with Accu_foo _ -> ... | ... -> ....

If t -> t -> t -> ... is really your intent for the inner type of the constructor,

No, I just wanted to make it clear for the readers that t -> t is an approximation of the type, since the closure representing an accumulator accepts an arbitrary large number of arguments. From the point of view of enabling unboxing, any type that looks like a function, e.g., t -> t, should be fine.

[xavierleroy]

To summarize my comment at coq/coq#12733 (comment) : perhaps a fast is_closure test suffices to get OK performance; I would need evidence that it doesn't suffice before embarking on the [@@tag 247] approach.

[jhjourdan]

if such a tag attribute were implemented, then it is very unlikely that the closure tag will be allowed at this place, since the GC expects some particular memory layout when it sees the closure tag.

That is the whole point, isn't? Coq is being mentioned in this discussion precisely because OCaml's GC will soon expect some specific layout for (non-)closuresclosures, so Coq can no longer create closures with tag 0.

But if you are concerned with safety, the solution would be for the compiler to forbid the use of Accu_foo for creating values or anything other than a wildcard for pattern-matching. Note that this is perfectly fine with Coq, since the only occurrence of the constructor is in the construct match Obj.magic x with Accu_foo _ -> ... | ... -> ....

Yes, that's the whole point of this RFC, but, in this RFC, in addition to providing more control over memory layout, we don't want to loose any safety guarantee. If the feature is unsafe or requires using Obj either to create or use values, then I don't think this is satisfying. As far as I understand your tag attribute proposal, it would require using Obj to create values which are compatible with the GC requirements.

[recoules]

Hi, I do not know if it perfectly fits in this RFC, but I think it is at least related.

I would appreciate being able to specify that a constructor argument should be "mixed/inlined" within the constructor itself.

So for instance, in the case of simple expression:

type op = Add | Mul
type t = Cst of int | Neg of t | Op of (op [@product]) * t * t

The annotation [@product] will make the cartesian product of Op and op:

type t = Cst of int | Neg of t | OpAdd of t * t | OpMul of t * t

Thus, matching on "high level" Op will simply be the or patter of every derived constructor. Extracting the value Add from OpAdd should be trivial since it would be a simple affine transformation of the tag.

I think it could also work if the mixed type contains non constant constructor but I am not sure if it would be interesting (extracting the value back will need a fresh allocation with copy). May be should it apply only on the constant constructors of the type.

[nchataing]

Hi,

We (@nchataing as intern, @gasche as advisor) implemented a variant of @yallop's constructor-unboxing specification as an experimental branch that we would now like to discuss and consider for upstreaming (you can find the original file for this specification at HEAD_SHAPE.spec.md)

Our intent was to implement the simplest possible form of unboxing in presence of several constructors, and leave more advanced aspects -- anything that could be left off -- to further work.

We support a per-constructor [@unboxed] attribute, that can be used in a variant type as long as the set of values corresponding to each constructor (boxed or unboxed) remain disjoint.

For example:

type bignum =
  | Short of int [@unboxed] (* represented directly by an integer *)
  | Long of Gmp.t           (* Block of tag 0 (first non-unboxed constructor) *)

Precise specification

We define the head of an OCaml value as follows:

• the head of an immediate value v is the pair (Imm, v)
• the head of a heap block with tag t is the pair (Block, t).

(In other words, the head tracks whether a value is immediate or a block, and for blocks only keeps the tag.)

The "head shape" of a type is a (slight over-approximation of) the set of heads of all possible values of this type.

Now consider a variant type declaration containing one or several constructors annotated with [@unboxed]:

type ('a, 'b, ...) t =
  | Const0 (* some constant constructors *)
  | Const1
  | ...
  | Const{m}
  | NonConst0 of t00 * t01 * ...
  | Nonconst1 of t10 * t11 * ...
  | ...
  | NonConst{n} of t{n}0 * t{n}1 * ...
  | Unboxed1 of u0 [@unboxed]
  | Unboxed2 of u1 [@unboxed]
  | ...
  | Unboxed{l} of u{l} [@unboxed]

(For simplicity we wrote above all constant constructors first, then all non-constant constructors then all unboxed constructors. But in fact we support arbitrary interleaving of these categories, and the representation is exactly the same as long as the ordering within constant constructors and within non-constant constructors is preserved.)

The compiled representation of this type is as follows:

• as before, constant constructors Const{k} are represented by the immediate number k
• as before, non-constant constructors Nonconst{k} of ... are represented by a heap block with tag k
• unboxed constructors Unboxed{k} of u{k} are represented directly by the value of type u{k}, without
  any boxing

This definition is rejected statically if the unboxed constructors overlap with the other values of the type, in the following precise sense:

1. We compute the "boxed head shape" BS of this type without the unboxed constructors; by definition of the head shape, this is the set {(Imm, 0), (Imm, 1), ..., (Imm, m)} ∪ {(Block, 0), (Block, 1), ,.., (Block, n)}.

2. Then we compute the "unboxed shapes" US{k} of each unboxed constructor, that is the head shape of u{k}.

3. The type is accepted if and only if the shapes BS, US0, US1, ..., US{l} are disjoint from each other. The head shape of the whole shape is then the disjoint union BS ⊎ US0 ⊎ US1 ⊎ ... ⊎ US{l}.

Unknown/abstract types are assumed to have a "top" shape with containing potentially all heads. (This should be refined when the abstract type is used to represent an FFI type with a precise shape implemented in C; supporting head shape assertions on abstract types is future work.)

Examples

(* rejected *)
type t =
  | Int of int [@unboxed] (* shape: (Imm, _) *)
  | Unit                  (* shape: (Imm, 0), conflicts with Int above *)

(* accepted *)
type t =
  | Int of int [@unboxed]  (* shape: (Imm, _) *)
  | Box of t               (* shape: (Block, 0), as the first non-constant non-unboxed constructor *)
  (* shape(t): (Imm, _) ∪ {(Block, 0)} *)

(* accepted *)
type prod = t * t
and t =
  | Int of int [@unboxed]        (* shape: (Imm, _): any immediate *)
  | String of string [@unboxed]  (* shape: (Block, Obj.string_tag)    (Obj.string_tag is 252) *)
  | Prod of prod [@unboxed]      (* shape: (Block, 0) *)
  (* shape(t): (Imm, _) ∪ {(Block, 0), (Block, Obj.string_tag)} *)


(** With abstract types *)

type abstract

(* accepted *)
type t =
  | Int of int [@unboxed] (* shape: (Imm, _) *)
  | Abs of abstract       (* shape: (Block, 0) *)
  (* shape(t): (Imm, _) ∪ {(Block, 0)} *)

(* rejected *)
type t =
  | Int of int                 (* shape: (Block, 0) *)
  | Abs of abstract [@unboxed] (* any shape, conflicts with Int *)


(** Nested unboxing *)

type t1 =
  | Int of int [@unboxed]
  | Block of unit
  (* shape(t1): (Imm, _) ∪ {(Block, 0)} *)

(* rejected *)
type t2 =
  | T1 of t1 [@unboxed] (* shape: (Imm, _) ∪ {(Block, 0)} *)
  | S of string         (* shape: (Block, 0), conflicts with T1 *)

(* accepted *)
type t3 =
  | T1 of t1 [@unboxed]    (* shape: {(Imm, _), (Block, 0)} *)
  | S of string [@unboxed] (* shape: (Block, Obj.stringₜag) *)
  (* shape(t3): (Imm, _) ∪ {(Block, 0)} ∪ {(Block, Obj.string_tag)} *)

Comparison with Yallop's proposal RFC#14

Jeremy Yallop's proposal uses a global annotation [@@unboxed] on all constructors at once, we use a per-constructor annotation [@unboxed]. (The RFC mentions this as a possible extension in "Extension: partial unboxing".) It would be easy to interpret [@@unboxed] as just "[@unboxed] on all constructors", but we have not implemented this yet.

A major difference is that the RFC#14 specification suggests renumbering constructors in some cases, where the representation of C of foo [@unboxed] is taken to be different from the representation of foo, in order to avoid conflicts with other constructors at this type. We do not support any such renumbering:

• the representation of Unboxed of foo [@unboxed] is always the representation of foo
• the representation of Boxed of foo always uses the block tag consecutive/next/succedent to the previous boxed-constructor tag in the declaration (filtering out unboxed constructors).

(Note: @stedolan calls this aspect of RFC#14 "conflating inlining and disjointness". We only deal with disjointness.)

separability

When the compiler is in flat-float-array mode, soundness relies on the property that all OCaml types are "separated": they contain either (1) only float values, or (2) no float value. New forms of unboxing must preserve this property.

We can track separatedness as part of the head-shape computation for unboxed type declaration, by adding to head-shape data a "separated" bit (see the details in HEAD_SHAPE.impl.md). We reject type declarations whose head-shape is not separated (when in flat-float-array mode).

It may be that this tracking is precise enough to entirely replace the pre-existing "separability analysis" of the type-checker. We have not implemented it yet, and have not evaluated this possibility.

Leftover question: how close to the compiler-distribution runtime should the specification be?

We define static accept/reject decisions for partially-unboxed types using "head shapes", which are defined in terms of the value-representation strategy of the main OCaml implementation. Should we have a more abstract definition, that leaves more room to other representations in alternative implementations?

We have not studied this question yet and we believe it is a pressing question. In particular, any choice that would end up being merged in the language probably MUST support the js_of_ocaml value representation. (Do you know of a reference document that describes the js_of_ocaml value representation? Pointers are welcome are we are not jsoo experts ourselves. cc @hhugo.)

Our intuition is that we could fine a "weakening" of our current specification that distinguishes less different sort of shapes -- thus rejects more definitions -- and gives good flexibility for alternative implementations. Here are some things we could do:

• We could stop making assumptions about the shape of function closures (currently: {Closure_tag, Infix_tag}), preventing the unboxing of closure-holding constructors.
• We could also weaken our assumptions about built-in containers (string/byte, arrays, double-arrays, etc.)
• We could stop distinguishing "float" from immediates (ouch!) if jsoo does this. What about Int32, Int64, should they be known as custom values?

In other words: what amount of runtime type information should we require from OCaml implementations?

At the limit, one extreme choice would be to only reason on the tag of variant constructors (constant or not), which are distinguishable from each other in any OCaml implementation, and not make any other assumption about head shapes (map all types except variants to the "top" shape). This would reject most unboxing definitions, leave maximal freedom for language implementations. Unfortunately this would also prevent the actually-interesting uses of the feature we know about, which mostly resolve around unboxing an int-carrying constructor.

This is an aspect of our design on which we need external feedback from people with a good taste for these matters. (cc @xavierleroy, @damiendoligez, @yallop, @stedolan, @lpw25, @let-def, etc.).

[hhugo]

Two things come to mind immediately

• Jsoo currently uses the same memory representation for int, nativeint, int32 and float.
• there is an option to represent strings and bytes differently. There are the same by default.

[jberdine]

An extension that might be useful to consider early as it might be related to the question of how tightly to tie the unboxability criterion to the value representation is e.g.

type t = Even of int [@unboxed] | Odd of int [@unboxed] | Box of t

or

type t = Zero | Positive of int [@unboxed] | Negative of int [@unboxed] | Box of t

These cases are similar to the normal case of unboxing an int-carrying constructor, but where a few bits, or the sign, of the carried int value are used to determine the constructor tag.

I don't know if the added complication of supporting such cases would be worthwhile, but it seems that it would involve considering more than representation of the carried values when determining the shapes. This notion might be productively unifiable with being able to support different backends with different representations.

[alainfrisch]

When the compiler is in flat-float-array mode

In this mode, wouldn't it be enough to simply reject unboxed constructors whose argument can contain floats, checking this property using the head-shape? (No need to keep track of separability in the head-shape itself.)

[alainfrisch]

Jsoo currently uses the same memory representation for int, nativeint, int32 and float.

Being able to have an unboxed disjoint sum between, say, int and float (e.g. as part of the "value representation" in the interpreter of a dynamically typed language) seems very useful (for those lucky enough to use the no-flat-float-array mode :-)). I can see several approaches:

• Ignore unboxing on individual constructors when compiling to bytecode (which covers the case of js_of_ocaml). The underlying assumption is that in general, when compiling to bytecode, performance matters less, and unboxing of constructor is justified by performance gains. One advantage of this approach is that we can still use the code base between native targets and bytecode/js_of_ocaml. One disadvantage is that the representation is no longer coherent between the two, which will require some care with both the FFI and scenarios based on the generic marshaler.

• Another approach is to keep track (in compilation artefacts) of assumptions about the backend. When the compiler detects that some required constructor unboxing would not "work" for js_of_ocaml, it would mark it in the resulting .cmo/.cmi file, and the marker will then be propagated to the bytecode executable. The js_of_ocaml compiler can then correctly fail when processing such executable.

• Or perhaps we don't need such explicit markers, and the js_of_ocaml compiler can figure out based on the actual bytecode instructions that the code tries to distinguish between, say, ints and floats, and fail accordingly. (If needed, one could keep more information in lambda/bytecode instruction to achieve that.) The check could perhaps occur after dead code elimination, so that one can even link a module which would try to do an unboxed union of ints and floats as long as the program does not use any function on that type. (Yet another variant: emit only a compile-time warning, and fail at runtime when trying to distinguish between ints and floats.)

[gasche]

@jberdine: In my mind, your examples (eg. Even of int [@unboxed] | Odd of int [@unboxed] are not acceptable because separation/disjointness is not guaranteed by the type system, but a "trusted" correctness property of the program. (If I understand correctly that your intent is for the programmer to only pass even numbers to the Even constructor, etc.)

I believe that this use-case would be better served by pattern views, replacing your Even n with parity n -> Even using Haskell view syntax, or something like n and (parity n with Even) using my still-weird with-patterns syntax. In the case where the property observed is represented by a constant constructore / immediate, like Even | Odd or Positive | Negative, this could be reasonably efficient.

Maybe I misunderstood. In any case, I would welcome "important examples" of why we would want to go in this direction.

@alainfrisch

In [flat-float-array] mode, wouldn't it be enough to simply reject unboxed constructors whose argument can contain floats, checking this property using the head-shape? (No need to keep track of separability in the head-shape itself.)

It might be a corner case but your proposal rejects type t = Foo of abstr [@unboxed] where abstr is an unknown abstract type, or type t = Foo of float [@unboxed], breaking the expected equivalence between [@@unboxed] and [@unboxed] on single-constructor types.

Being able to have an unboxed disjoint sum between, say, int and float (e.g. as part of the "value representation" in the interpreter of a dynamically typed language) seems very useful (for those lucky enough to use the no-flat-float-array mode :-)).

None of the three options you propose look terribly enticing to me. My preference would go for a variant of (2), where we store assumptions in the build artifacts, and also offer an explicit option to ignore some unboxing (to be discussed) to produce jsoo-compatible artifacts.
Taking a step back: in term of "getting things done" strategy, the easiest route may be to work with the lowest common denominator for a first PR (disallow combinations that would be ambiguous with the ocaml{c,opt} representation or jsoo), to avoid a long discussion on this point, and try to propose more ambitious approaches in a later PR.

[gadmm]

Congrats for the prototype! Regarding the opportunity to fix Coq's native_compute in no-naked-pointers mode, would the implementation of closure unboxing be simple enough to fit a "getting things done" strategy, or would Coq devs be better off pushing for an efficient is_closure test in the meanwhile as suggested by Xavier?

(For the curiosity of readers here is what I get:

        OCaml version 4.14.0+dev0-2021-06-03

# type t = Closure of (int -> int) [@unboxed] | Pair of int * int;;
type t = Closure of (int -> int) [@unboxed] | Pair of int * int
# let tag x = (Obj.tag (Obj.repr x));;
val tag : 'a -> int = <fun>
# tag (Closure (fun x -> x));;
- : int = 247
# let rec f x = x and g y = y;;
val f : 'a -> 'a = <fun>
val g : 'a -> 'a = <fun>
# tag (Closure g);;
- : int = 249
# let eta x = match x with Closure f -> Closure f | Pair (y,z) -> Pair (y,z);;
Fatal error: exception Invalid_argument("Cases.add_any: Set (_ :: _)")
make: *** [Makefile:673 : runtop] Erreur 2

The exception does not arise if I replace int -> int with int. I suspect that that dual tag of Closure requires a special treatment.
)

[gasche]

@gadmm I would prefer to discuss our prototype somewhere else, and reserve this issue to discuss the specification. We hope to open a PR soon-ish, and in the meantime opening an issue on my fork or @nchataing's would be fine. (Currently the prototype does not support unboxing function types, but it could certainly be taught that functions have tag Closure_tag or Infix_tag. The fact that it does let you proceed with a definition that it believes to be incorrect/conflicting looks like a glitch we have to fix. You may want to use the -dheadshape flag to observe head shape computations.)

[gasche]

While we are in meta-land: please note that our proposal is different from the initial proposal of @yallop. (Maybe we should open another RFC?) We would welcome feedback on whether people find the variant we propose better or worse than the (corresponding subset of) the original proposal.

[yallop]

It's good to see progress on this. Thank you for picking it up and creating an implementation, @nchataing and @gasche!

I agree that per-constructor annotations are the wisest approach for the initial change: their behaviour is straightforward and they handle the most compelling examples (e.g. the Coq accumulator issue, ropes and bignums, although that last also needs support for exposing abstract type representations in order to work optimally).

also offer an explicit option to ignore some unboxing (to be discussed) to produce jsoo-compatible artifacts.

That's my preferred solution for the js_of_ocaml issue, too.

[gasche]

Re. Coq, the specification we propose with @nchataing would accept the type ind_foo proposed by @silene above:

type ind_foo =
  | Accu_foo of t -> t [@unboxed] (* the actual type of the closure is infinite: t -> t -> t -> ... *)
  | Construct_foo_0 of t * t * ...
  | Construct_foo_1 of t * t * ...
  | Int_foo_0
  | Int_foo_1

(Minor note: per-constructor attributes take a single @, the double sign means that the attribute is attached to the whole toplevel item.)

This is assuming that we can dynamically distinguish functions from variant-constructors and immediates on all backends we decide to care about, in particular js_of_ocaml. @hhugo gave information about the numeric representation earlier (thanks!), but not about closures. Is it valid to assume that Obj.tag works on function closures with jsoo, and returns Obj.closure_tag or Obj.infix_tag?
(If the answer is "no", then "distinguishing closures" ends up in the same boat as "distinguishing float": we can do it with the standard compiler, our prototype supports this, but understanding the right design to expose this backend-dependent capability is delicate work left ahead of us.)

[gadmm]

I was wondering what has to be done for people who overwrite tags of values when the tag was non-meaningful, for instance in order to declare that an int array needs not be scanned using Obj.no_scan_tag. (This was one use-case explicitly taken care of by the introduction of Obj.with_tag when deprecating Obj.set_tag at ocaml/ocaml#1725.) The programmer can probably avoid issues locally but one concern is with breaking code at a distance (e.g. when mixing two libraries with incompatible assumptions).

I think it is enough to ask the programmer who changes non-meaningful tags to make such types abstract, to prevent unboxing. In this case the fix is just to document that the assumptions made on the representation of values according to their type are strengthened when this feature lands.

In addition, the no-scan-tag-array use-case sounds reasonable, there is the opportunity to make it official by adding it to the list of recognised tags for types whose tag is non-meaningful.

[gasche]

We discussed the jsoo-interop problem at a maintainer meeting today. My understanding of the consensus is as follows:

• native and bytecode should keep the same value representation, always
• for a first step, let's go with the conservative approach of supporting the intersection of ocamlc and jsoo's distinctions (so merge int, int32, int64, float and nativeint together).

[gasche]

@hhugo where can I read documentation about jsoo's value representation?

In particular, how are constructors represented? Are they distinguishable from numeric values?

[hhugo]

In particular, how are constructors represented? Are they distinguishable from numeric values?

constant constructor are not distinguishable from numerical value.

I'm adding some documentation:

• GPR: Doc: document memory representation ocsigen/js_of_ocaml#1153
• preview: https://github.com/ocsigen/js_of_ocaml/blob/d4fae21a14cc78742d90331b6188acd387a482eb/README.md#data-representation

[gasche]

Thanks! I'm glad I asked :-)

[alainfrisch]

@gasche : generally speaking, since js_of_ocaml starts from the ocaml bytecode, it cannot use a representation that would allow distinguishing more values than bytecode programs.

[yallop]

This POPL 2024 paper appears to be related:

We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument.

Unboxing must be statically rejected when it could introduce confusions, that is, distinct values with the same representation.

We discuss the use-case of big numbers, where unboxing allows to write code that is both efficient and safe, replacing either a safe but slow version or a fast but unsafe version.

[gasche]

Indeed, we wrote a paper based on Nicolas' internship results and some additional contributions following, including the line of thought suggested by Stephen on the relation to cpp's algorithm to avoid macro expansion non-termination.

The current draft is available at http://gallium.inria.fr/~scherer/research/constructor-unboxing/constructor-unboxing-popl-2024.pdf . Anyone is welcome to provide feedback as I have a window of a few days/weeks to make changes before the camera-ready version.

(The Acknowledgments of the paper, currently sitting on page 30, mention a few people here by name, notably @yallop for authorship of the proposal, @jhjourdan, @silene and @gadmm for their discussion of vm_compute, @stedolan, Nicolas and myself.)

(Note: we could probably have notified the community of this presentation work earlier, but POPL used an unusually strict interpretaion of double-blind this year that made this difficult. From the CFP: "authors should not take steps that would almost certainly reveal their identities to members of the Program Committee, e.g., directly contacting PC members or publicizing the work on widely-visible social media or major mailing lists used by the community." KC, Stephen and favonia were on the PC for example.)