This is a following to the previous post explaining the current discussion around record field and variant constructors disambiguation. This second, more technical blog post will discuss some details of the semantics, and the last one explain some of the philosophical/aesthetic arguments that were used to support either proposal -- which may interest you if you like type system design, and come back in other discussions of OCaml design choices.

The devil is in the details

Disambiguation of scoped labels

In Jacques' initial proposal, only non-scoped labels were disambiguated using typing information: (r:t).l would get elaborated into r.l^t, but (r:t).P.l would be looked up by the naming environment P.l only, without using type information.

In the consensus proposal, the type information is used also in this case, but only candidates that do have the long identifier P.l (they are possibly several in case of label shadowing) are considered. You could also drop P altogether in this case and use only type information (if it is present, there is only one correct choice anyway), but this doesn't make much sense. Another possibility would be to disambiguate in the sub-environment under P: consider all labels of the form P.Q.l for some long prefix Q, but warn when Q is not empty, as this is only accepted by the scope-inferring strategy.

Multi-label or first-label lookup

In his own implementation at Lexifi, Alain uses a multi-label lookup scheme: in the case where you're constructing a record, you can use not only the first label to disambiguate, but all the present labels. This would make the following accepted:

type t1 = { foo : int; bar : float }
type t2 = { foo : int; baz : bool }

let mk1 foo bar = { foo; bar }
let mk2 foo baz = { foo; baz }

With the current OCaml type-system, mk1 would be rejected as foo is resolved at type t2 by the shadowing rule. Alain remarks that if take into account all the fields, it's clear that mk1 can only build a t1 because the field bar is present. This is a purely syntactic criterion (no type information involved) that improves over the statu quo.

The initial implementation of the type-based strategies had only single-label lookup (using the first label appearing in the record expression), but after some discussion multi-label lookup is now implemented and used in absence of type information.

Warn to avoid relying on shadowing

One criticism that applies equally to both proposals is that the semantics of the code now depends on the presence or absence of type information -- in particular type annotations, while OCaml programmers are used to consider that they are useful for clarity and debugging purposes only.

In the case of access to a label that is not currently in the naming environment, the situation is rather clear: either there is type information available and, by the scope-inferring strategy, the program is accepted, or there isn't and the program is rejected. In this case, there exists a unique well-typed program and type annotations only allow to find it.

The situation is more awkward in the case where you access a label through a long identifier that does exist in the naming environment (it was defined at the toplevel or imported by an open directive). For example :

module P = struct
  type t = { l1 : int }
open P
type u = { l1 : bool }

... (* some code *)

let awkward = do_something (fun r -> r.l1)

The interpretation of this example depends on whether do_something provides type information. If it does not, the shadowing rules applies and the label is understood as l1^u. If it happens to have a type of the form (P.t -> _) -> _, then the label is understood as l1^(P.t). It is a bit worrying that both interpretation could be correct, and that the choice made depends on the order of open P and type u = ....

There are two solutions to make sure this awkwardness is avoided. You could always disable type-based lookup when name-based lookup succeeds. This was Jacques initial proposition, but it is exactly the opposite of what the conflict-solving proposal suggests, which is only useful to disambiguate between several name-based lookup possibilities, so this solution hasn't been kept.

The other solution is to remove the shadowing rule from the language: in the case where a given long identifier may denote several different labels, accept to type-check the program only in presence of type information. You are back in the reasonable situation where there always exists a unique way to have the program type-check. However this solution is not conservative, as it would reject programs that are currently accepted by the OCaml compiler (and make use of label shadowing). This is not acceptable, and the consensus it to raise a warning in this case.

(If you're beginning to think that adding warnings instead of making a choice between "it's ok" or "it's wrong" is a convenient way to dump hard design decisions onto the user instead of making them on the language side, well, you might have a point.
And before you complain about warnings being hard to activate or deactivate locally, let me note that I welcome well-thought-out suggestions and implementations of such pragma-like systems for OCaml, but that you will have a hard time making everyone happy about it.)

Philosophical justifications for either proposals

Scoped, unscoped or type-scoped labels

What was your mental model of OCaml labels and variant constructors: did you think of them as scoped names at a particular module prefix, or as global names like method names and polymorphic variant tags?

I definitely had a scoped model. Jacques seems to have an unscoped model. This affects how we consider both proposal, the conflict-solving one being the most natural to me (and the other one distastefully daring in omitting module prefixes), while Jacques is at home with the scope-inferring proposal and clearly intends to disable the restricting warning for his personal developments.

In the vision Jacques explained in this post (which was at least a formal vision you can have during this discussion, I don't claim that it is the way he thinks about labels), record labels and variant constructors are global names. Record access and variant matching are doing a lookup based on these global names, just as objects and polymorphic variants, and the syntactic module prefix is just here for type-checking purposes.

In my mental object of OCaml records and constructions, the declarations

type record = { foo : int; bar : bool }
type sum = A of int | B of bool

can be understood as some well-supported form of syntactic sugar for the following presentation in term of introduction and elimination rules, introduced as primitives:

type record (* abstract type *)
val foo : record -> int
val bar : record -> bool
val record_intro : ~foo:int -> ~bar:int -> record

type sum
val A : int -> sum
val B : bool -> sum
val sum_elim : ~case_A:(int -> 'a) -> ~case_B:(int -> 'a) -> 'a

With this point of view, labels and constructors are essentially identifiers like any other, for which convenient syntactic sugar is provided: this is firmly rooted in the "scoped" view of labels. We could consider having a functional language that is lower-level than OCaml, and allows to implement those primitives of record and variant construction and destruction as derived features -- in a way that is more efficient, by the way, that what dispatch/lookup on global names allows.

Finally, a third possible view of labels is that the identity of the associated type, instead of their module prefix, is part of their full name -- they are "type-scoped". The identity of the label is l^t rather than l, with the type part being hidden from the programmer for convenience. This subsumes both points of view, and I think it is the one you need to adopt to make sense of the proposal as it will be implemented -- also the one closest to Jacques' argumentation.

Type-erasure semantics vs. type-directed elaboration

A maybe subtle point of the discussion was the request by Jacques of a "dynamic semantics that does not depend on types", also called a type-erasure or type-erasable semantics. The idea is that if you take an OCaml program exactly as it is written, you can drop all form of type information, and claim that you have obtained a program in an untyped (~ dynamically typed) language that can be executed as is. The dynamics semantics (what happens at runtime) is free of any typing consideration.

This does not hold of all programming languages. Haskell type classes, for example, are a form of static information that has an influence over the dynamic semantics of the program (which type-class dictionaries get resolved where). If you drop all static information from a Haskell program, you have lost information that is necessary to run it. (This is different from some object-oriented overloading scheme that resolve method calls o.m(...) based on the type of the object o, which can be kept until runtime. In Haskell you get return-type-based overloading which cannot be explained in this way: min :: Bounded a => a.)

Type-erasure is not a black-and-white concept: what you do in practice is to explain precisely which part of the type information plays a runtime role. You do that by defining a type-directed translation from your base language to a slightly more explicit language, that does have a type-erasure semantics -- all the information you need has now been exposed in the syntax. The smaller, simpler, most local this translation ("elaboration") step is, the closer to type-erasure you language is.

A type-erasure semantics is good for performance (you can drop typing information instead of maintaining it at runtime), but I think the most important benefit is that it acts as a design pressure that can force you to do the right thing. Forcing yourself to describe that small elaboration step explicitly is always a good idea. In particular, it is an excellent candidate of what a "show me the implicit stuff" feature should reveal in an IDE for your programming language.

Back to the point, Jacques remarked that, from the point of view of the dynamic semantics, his model of unscoped labels supports type-erasure: if your mental model of the runtime semantics of the language is to dispatch on labels as global names, you can drop all type annotation without changing the semantics of the program. Because you only do that for programs that have been type-checked, you know that you won't get a label coming from an unexpected place (at an unexpected type).

On the contrary, the conflict-solving proposal combined with scoped labels seems to break the property of having a type-erasure semantics. With only the shadowing rule, you can give a dynamic semantics of scoped labels that is type-erasing. As soon as you support type-directed disambiguation instead of shadowing, you face the choice of either:

  • using a dispatch model on ambiguous names, as we have for the unscoped semantics (but then why insist on a scoped model?)

  • or using an elaboration step to explain the translation from the overloaded r.P.l to the unambiguous r.P.l^t.

Jacques criticized this elaboration step for first breaking the type-erasability of the dynamic semantics, and secondly introducing some amount of type overloading that has so far been forcefully kept out of the OCaml language.

I believe we should recognize and accept this elaboration step, taking a mental model of type-scoped labels instead of module-scoped labels. The type-erasure semantics with unscoped label names gets type-erasure at the cost of a richer runtime model (dispatch on global names), which is conceptually more complex (and formally less efficient) than the simpler semantics after the elaboration. Besides, syntactic overloading is indeed an evil that we all hate because of the ambiguity it introduces, but the potential for ambiguity of the conflict-solving proposal is strictly inferior to the ambiguity of the scope-inferring proposal; in any case, anyone supporting either this feature accepts introducing some amount of ambiguity on label names -- which are, I think, a reasonably self-contained place to be ambiguous.

Layered system design: name resolution before or during typing?

I like to think of strongly typed languages as a layering of three set of static rules:

  1. Parsing: Syntactic rules that reject syntactically invalid program, and otherwise give you a well-formed Abstract Syntax Tree (AST)

  2. Binding: Name resolution rules that take the AST and compute where each occurrence of an identifier was bound, reject programs with unbound variable occurrences, and return you an AST enriched with definition-site/use-site information. The derivations used at these steps remembers which name are defined in the current naming environment, but not (yet) their type.

  3. Typing: rules that accept this AST with name resolution information, and returns a full typing derivation proving that the program is well-typed (or reject it)

In the current implementation of the OCaml compiler, steps 2. and 3. are interleaved, done at the same time (a previous version of the "unused variable" warning implementation actually re-implemented step 2. as a separate pass). But conceptually this separation can still be done and helps to think about the design of the language.

For example, the ocamlspotter tool of Jun Furuse, that can tell you where each name is defined, (currently) depends only on the output of the name resolution pass, without needing typing information.

When you consider a new feature, you can wonder how it affects these different steps. New syntactic sugar affects only step (1) (or can be described as an AST-to-AST rewriting step happening just after step (1)). Introducing the open keyword affects steps (1) and (2), but not step (3). Adding GADTs added new syntax (step 1) and new typing rules (step 3), but no particular identifier-resolution rule, while changes to pattern matching may affect all three layers.

How do the scope-inferring and conflict-solving proposal affect the layer of the static semantics of our programming language?

With the conflict-solving proposal, the notion of "name resolution" of a label has to be weakened: when you find an access to a long label, r.P.l, you look at the set of names exported by the (sub)module P in your naming environment, and instead of taking only the last l defined in this environment, you have to consider the set {l^t1, l^t2..., l^tn} for all types t1,..,tn in P that define the label l (note that we look only at the type and label names, not at the actual types). Then, when you run the later step (3), you may have access to type information. If you don't, you should use the shadowing rule (pick the last label in the set) and potentially raise a warning if there is more than one candidate. If you have the type of r, it must be along the t1,..,tn, and you can disambiguate the label into a unique possible candidate. Note that the "multi-label" disambiguation strategy of Alain also happens purely during step (2).

For the scope-inferring proposal, you cannot say anything meaningful about labels during step (2): if you see an access with an unqualified label r.l, l might not be present unqualified in your naming environment, but potentially happen anywhere in a submodule. You can only keep l as a global name (unscoped model), and wait until step (3) to resolve the ambiguity.

Under this (admittedly personal) point of view, the conflict-solving strategy is less complex than the scope-inferring proposal: it displays a controlled amount of syntactic ambiguity (resolving to a set of candidate names instead of one possibility), which is discharged at typing time. On the other hand, the disambiguation strategy of the scope-inferring proposal can be explained by producing a syntactically correct disambiguated AST, which is not the case the conflict-solving strategy, unless you were to add the explicit construction l^t, which was proposed in the past but not really considered in this discussion -- which was complex enough already.