Type-based selection of label and constructors.

Alain Frisch

Most languages provide some way to manipulate tuples of values with a proper label for each field. They are called structures in C, records in OCaml; objects as found in most mainstream OO languages extend this same notion.

This post introduces some recent improvements to how records are supported in OCaml. This is currently available in the record-disambiguation branch of OCaml, on which Jacques Garrigue has been working recently (with some major contributions from Leo P. White, and with a lively discussion with Gabriel Scherer and myself).

Some references:

Type-checking field projection: the “last record in scope” strategy

Let’s consider this example in C:

struct foo { int x; int y; };
struct bar { char* y; char* x; };

int f(struct foo r) {
  return r.x;
}

Both structures foo and bar define a field label x. How does the C compiler know that the field projection r.x extracts the first field of a foo structure and not the second field of a bar structure? Well, simply because its type-checker tells it that the expression t has type struct foo. This information is propagated from the function interface, which gives explicitly the type of r.

Let’s do the same in OCaml:

type foo = { x: int; y: int }
type bar = { y: string; x: string }

let f (r : foo) : int = r.x

With OCaml 4.00, this does not type-check. The OCaml type checker ignores the explicit type information about r to decide what “.x” means. Instead it applies a standard lookup strategy: the last record type definition (in the current scope) which defines a label x is picked. In the example above, type-checking obviously fails because this strategy decides that the field projection in on type bar, which is incompatible with the type inferred for r.

This behavior of OCaml is directly related to the core type-checking strategy of OCaml, based on type inference with unification. When OCaml sees an expression like (fun r -> r.x), in general, it might not know the type for r. To keep things simple, the original design decision was to apply the “last record in scope” strategy. So the field projection .x would actually fix the type for r (and if a type happened to be already known, those two types would be unified, maybe leading to an error). This is not very nice, because it makes the type-checking depends on the order between type declarations. Also, the open statement can bring external declarations in the current scope, and thus potentially pollute it. Consider the case where a third-party library, which you open in your code, decide in a next version to add some new record type; this could very well shadow your own definitions and yield a weird error message.

The record-disambiguation branch tries to deprecate, or at least downgrade, this lookup strategy. In particular, it adds a new warning (number 41) which reports ambiguous cases (where the “last record in scope” strategy plays).

Dealing with shadowed label names

In addition to making code fragile, the “last record in scope” strategy simply makes it impossible to refer to a record field whose label has been shadowed. See this previous post for a discussion of existing work-arounds and why none of them is satisfactory. This post also described a hack we added at LexiFi to our version of OCaml to refer explicitly to a label by referring to its type explicitly. Indeed, we considered that having nicer names and cleaner APIs without extra noise (arbitrary choices of synonyms to avoid collision, prefixes, extra module structure) deserved some little extra investment at the language level.

The record-disambiguation branch provides a better solution: it provides a lookup strategy based on type information, exactly as in mainstream languages without advanced type inference. If the type of r is known (through propagation of types), you can write r.x without having to worry that the label x might have been (or will be) re-used in another record type declaration in the current scope (through a local declaration or an open statement). The legacy lookup strategy is used as a fallback if no type information is available. With this branch of OCaml, the example above type-checks.

I won’t describe here what “type propagation” means exactly, but: (i) you can assume that standard type information flow as found in mainstream language is respected; for instance a type flows from an annotated function parameters to its use sites; (ii) the same type propagation is already used for other language features such as GADTs, optional arguments, polymorphic methods; (iii) users probably get an intuitive understanding of how propagation works, roughly, and they can always add more explicit type annotation if needed (extreme situation: (r : foo).x); (iv) all that is done by preserving principality properties of the type-checker, as long as the -principal compiler flag is enabled.

Records declared in other modules

Now let’s consider the following piece of code:

module Foo = struct
  type t = { x: int; y: int }
end

let f (r : Foo.t) = r.x

Here, when the type-checker encounters r.x, it knows that r has type Foo.t. With the new type-based lookup strategy, this is enough to accept the projection on x because in the current scope, we know that Foo.t is a record type with a label x. This might be surprising because we OCaml users used to live in a world where labels were scoped by the module in which they were declared (and as long as this module is not opened, we had to use an explicit module qualifier on the label name, as in r.Foo.x). But if you think about it, this is exactly what would happen in “classical” languages; for instance in C++, you can use the dot notation to extract the value of an object field without having to write down which class the field name belongs to (this is implicitly derived from the type of the object). In a sense, the type-based lookup strategy considers that labels are scoped by their declaring type: if the type of a record is known and the declaration of this type is visible (not abstract) in the current scope, this is enough to allow accessing the record labels without any module qualification.

Allowing type information to access implicitly a non-local label is a real departure from the previous approach, although it remains compatible, obviously. Some people don’t like that this more powerful algorithm allows developers to write less explicit code. There are also deeper philosophical reasons about labels really being scoped by the module they are defined in. Most of the intense discussion about this branch was about whether those implicit non-local accesses should be rejected. But all the participants have agreed that this is a matter of programming style, and a new warning (number 40) has thus been incorporated to report such cases. When the warning is triggered, there are two ways to get rid of it: either open the module in which the label is defined or add an explicit module prefix in front of the label. The first solution does not really bring much: the concrete rationale for the warning (forgetting about philosophy) is that the extension makes the code less explicit, but adding an “open” statement, even a local one, does not really make the field access more explicit on its own. So I assume that people who will turn the warning on will tend to keep explicit prefixes on non-local label.

Overview of the branch

I’ve described three improvements brought to records in the branch:

  • A new warning to report cases where a piece of code relies on the “last record in scope” strategy.

  • A new resolution logic which allows the type-checker to use known type information to process a record field access even though the label has been shadowed by another declaration.

  • This new mechanism can also be used to avoid explicit module qualification for non-local record types (this can be disabled by turning a warning into an error if you really don’t like it). The branch does a few more things:

  • The new resolution logic is also available for building records. This relies on the fact that the type-checker propagates type information not only in a forward way, but also in an top-down way (i.e. it propagates an “expected type” to sub-expressions): for instance, in our running example, you can write ({ x = 1; y = 1 } : foo) or foo {x = 1; y = 1} if you have declared a function foo of type foo -> foo.

  • Same for record patterns, now relying on the fact that the type of the matched expression is propagated to patterns (this has been introduced recently to support GADTs).

  • All that is available for resolving sum type constructors as well. It is now possible to have two ASTs sharing common constructors and map from one to the other without writing module prefixes everywhere!

  • Back to records, the fallback “last record in scope” strategy has been improved a little bit for record expressions and patterns. Instead of looking up each label independently, they are all considered together and the selected type is the last record in scope which has all these labels (and maybe more, for record patterns or record “update” expression { r with … }). Even when type information is not explicitly available, simply looking at the whole set of labels can now be used to disambiguate between record types. This is purely syntactic information, which not does not change the spirit of the “last record in scope” strategy, just make it more clever. (This works especially well if you rely on record patterns instead of field projections.)

LexiFi was so eager to benefit from these changes (for our internal developers but also for our dear customers) that we already incorporated the branch to our local version of OCaml and got rid of our previous hack (type prefixing, which had luckily not been advertised to our customers). We consider that the branch closes a long-standing annoyance with basic features of the language (records, sum types), which leads to noisy code, and more importantly, to noisy type definitions. Moreover, it was difficult to explain (and justify) the previous behavior to experienced developers without prior knowledge of OCaml. So we are eager to see the branch incorporated to the next official version of OCaml. Thanks to Jacques, Leo, Gabriel for the hard work and the interesting discussion around these new features!

© 2000-2024 LexiFi - All Rights Reserved.

Legal | Manage Cookies