When defining or destructuring elements of record types, the order of fields doesn’t matter:
type foo = { bar : int; baz : string }
let x : foo = { baz = "hello"; bar = 3 }
let f : foo -> int = function { baz; bar } -> bar
But when implementing a module type, it does:
module Foo : sig
type t = { baz : string; bar : int }
end = struct
type t = { bar : int; baz : string }
end
==>
Error: Signature mismatch:
Modules do not match:
sig type t = { bar : int; baz : string; } end
is not included in
sig type t = { baz : string; bar : int; } end
Type declarations do not match:
type t = { bar : int; baz : string; }
is not included in
type t = { baz : string; bar : int; }
Field baz has been moved from position 1 to 2.
Is there a principled reason for this? Or is it just that it’s easier to check equality of types if we don’t worry about the possibility of reordering the fields? The error message shows that the compiler is already able to notice that the only difference between the types is the reordering of fields.
First, I think the reason that it matters for records, and not for objects, is that objects use a hash-based method to find members (but that’s only from memory, I could be mistaken).
For records, it seems like there are two things one could do:
(1) the current method
(2) sort fields and take that normalized version of the type as the one to compile
Imagine that one did #2. Then it would be non-obvious what the runtime representation of a particular record-type was, right? Imagine a future version of OCaml which supports unicode for field-names: it would be completely non-obvious (b/c, so I understand, Unicode collation isn’t the same as the numerical ordering of Uchar) what runtime field order is.
From the beginning of caml-light, it seems like one unstated principle has been “can understand it from the perspective of C code”. And that’s pretty much true for the core language (hence, excludes objects) right?
It depends on what you mean by “principled”, but field order directly intervenes in the compilation strategy of record operations.
Concretely, if a record type is defined with a field x which is the i-th field of the record type, then an expression of the form e.x will be compiled by a lookup on the i-th field of the block obtained as a result of evaluating e. Then clearly, order must match between interface and implementation as otherwise field accesses inside and outside the module would be compiled differently.
The same holds for its dual, variant types: the order of constructors directly influences how constructor expression and pattern matching is compiled, since their order is encoded as the “tag” of the block encoding the constructor after compilation.
Hmm, ah, I see. It seems I frequently get confused because most of OCaml is so nice and abstract like a mathematical type theory, but then every so often I trip over something where concrete memory representations matter.
I’m sure there are a bunch of places where low-level performance issues leak into what some of us might call language design. Remember the right-to-left (officially, “unspecified”) evaluation order of caml-light (and, I’m guessing without trying it, the current bytecode target) ? That was done in order to minimize closure-creation on the heap grin.
It’s one of the wonders of caml-light (and ocaml) that even though it feels nice and mathematical and all, the core language can be used in a very straightforward way, no extra bells, whistles, or fancy flux capacitors needed, to program pretty close to the metal.
Back in the day, it was the reason I gave up SML/NJ for caml-light.
Apart from the already mentionned practical reason that records must be usable from C, you can also think of a more “sound” reason: records are nothing but tuples which fields are named. Therefore, field order has to be part of the type definition.
Thanks, but I would find that more convincing if it were possible to define or destructure elements of a record type positionally. Since the only way to define and destructure elements of a record type is by field names, it’s hard for me to see “records are tuples with names” as being true in any sense other than practical implementation.
it’s hard for me to see “records are tuples with names” as being true in any sense other than practical implementation.
type a
type b
type p = a * b
type r = {
a : a;
b : b;
}
For instance, with two given types a and b, p and r will have the same number of inhabitants. They allow to combine types in the same way, and thus it is not really surprising that they’re using the same representations, whatever it is.
What you say shows that they are isomorphic types. But a * b is also isomorphic to b * a, in particular having the same number of inhabitants, so that doesn’t imply the fields have to be ordered.
No, that’s not surprising. What’s surprising to me is that implementing a module type requires a record that has the same representation, as opposed to having the fields with the same names and the same types (and therefore being indistinguishable in terms of what you can do with its elements in code).
[I could be wrong, but it seems like] That shouldn’t be surprising at all: module types are contracts that sit at compilation unit boundaries: the producer and consumer of a record-type specified in a module-type at the boundary betwen two compilation units MUST necessarily agree on the representation of that record-type, right?
But I would agree, that one could insist that the two types r1 and r2 have the same representation, right?
type r1 = { a : a; b : b}
type r2 = { b : b; a : a }
The problem would then be that from the text of a record-type, to know the runtime representation, would involve some transformation – maybe as simple as sorting the fields by some collating sequence, but still, not as simple as “the first field in the record-type is found at the zero-th slot in the block”.
I just don’t naturally think in terms of how code gets compiled having an effect on the language design. This is a statement about me, not about OCaml. To me, being a mathematician, the natural level at which to think is an abstract one, where a record type, like an object type, would have a set of fields, not a list of them. I understand the point now about why the order of the fields in a record type matters, but it’s still not intuitive to me, and I don’t think any more explanation about how it’s should be intuitive because of compilation concerns and runtime representations is going to make it intuitive to me: I understand now why those concerns require it, but those concerns are not intuitive to me, and so an explanation in terms of them doesn’t make other things intuitive either. Hopefully with practice I will develop some intuition of this sort that will naturally pop up in my head when I wonder about questions like this in the future, but I think this thread has helped as much as it can in that direction.
Another key reason for this, is separate compilation. Each file of OCaml source code is a unit of compilation, and they can all be compiled and linked separately.
Suppose someone gives you a compiled bytecode implementation file foo.cmo and you need to link it to your program. The compiled bytecode is a black box. The compiler doesn’t know anything about its implementation ie what is the ordering of the fields of the record type foo. Hence you also need to provide an interface file foo.mli to be able to link your program with the bytecode file. And so, the order of the record fields declared in foo.mli needs to match the actual order of the fields used internally in foo.cmo.
The fact that order doesn’t matter for objects means that none of these arguments imply that order has to matter for records: in theory, records could be implemented however objects are. It makes sense that records are intended to be “lower level” than objects, with a more concretely determined and efficient memory representation. But it didn’t have to be that way, since code using objects can still be separately compiled.
That’s true. You could also make the argument that OCaml didn’t need to erase types at runtime and could have attached type information to every value at runtime, like say Python, which would allow introspecting and debug printing values at runtime. It was a design decision that OCaml didn’t do that. I guess it’s the same for every decision where they traded some ergonomics for efficiency.
This is only a consequence of OCaml’s separate compilation strategy though.
If you have a compiled object file, you could absolutely also have a generated interface file that other modules use to link with it (e.g. GHC does this with .hi files).
It’s just that OCaml made the decision to use user-written interface files both as high level specifications that constrain implementations and as low level interface definitions between compilation units.
This has the advantage of allowing modules to be compiled in parallel more often but it also has the side effect of forcing mli files to be precise about low level implementation details like this that then leak into the supposedly high level specification.
And it turns out that every successful programming language makes such decisions. Let’s look at Haskell: for a decade or so, it languished as a theoretical curiosity: I remember back in 1992 being told that GHC took well over a day to bootstrap itself. So Wadler et al came up with monads, and modified the compler so that it would compile code written in monadic style to efficient machine code. That was transformative for Haskell.
Every language design has decisions (usually, ton) like that.
Even in mathematics, isomorphism can be considered as distinct of identity. After all, a category is just a directed graph, but when we say that two objects are isomorphic, we don’t claim that they are represented by a unique vertices in this graph but that there is two edges between them and that those edges are interpreted as an isomorphism. It’s the same with records in OCaml : two isomorphic records have two distinct but isomorphic runtime representations.
Look at this example with first-class module, that are implemented in the same way as records in the runtime.
(* same representation than `type a = { a : int ; b : float }` *)
module type A = sig val a : int val b : float end
(* same representation than `type b = { b : float ; a : int }` *)
module type B = sig val b : float val a : int end
let foo (module M : A) = ()
let bar (module M : B) = foo (module M)
You won’t get a type checking error, but the compiler automatically applies the isomorphism for you and it can cause allocation to change the runtime representation of your module.
Edit to add : When we defined a notion in category theory, we also say that it is unique up to ismorphism, which means that there can be multiple choices but that isomorphism is an equivalence principle. From a computing point of view, the denotation must not change between two isomorphic representations (it’s an implementation detail). But from an operational point of view, I would say that it is all the art of the programmer to choose, among this infinite possible choices of isomorphic representations, the one which best fits the problem at hand (mostly for time and space complexity).