Ah! Good to know :) TypeScript seems like a neat language, and I've got a JavaScript project coming up so I intend to look into it more deeply soon.
Yeah, in my example, `R` is the row variable itself, and it represents all those other, irrelevant values in the record, while I gave it the name `_` in the type itself, since rows themselves don't have field labels, but rather represent sets of labels. In ML, the labels of the fields are part of the type, but the labels of the rows are not part of the type. Then, `..a` is a type variable representing the type of the row (it gets a distinct name because you can imagine a function which takes two separate records with two separate rows[0], or even a function which takes two records but constrains them to the same type with a single row[1]), and is akin to a type variable used for parametric polymorphism, such as `'a`, and, in Standard ML with eqtypes, `''a`.
To the best of my knowledge, the term "row" comes from The Definition of Standard ML, where the grammar given for the core language includes productions called "TyRow", "PatRow", and "ExpRow", which correspond to the syntax of record types, patterns, and expressions, respectively, but only the part in between the `{` and `}`:
(The `At` prefix means "atomic", and has a specific meaning in the definition.)
So, then, a row variable is one which literally holds a sequence of label×type or label×value pairs. It sometimes even feels like it's a metavariable which holds a branch of the syntax tree the way a variable in a macro does, which might be another reason why row polymorphism feels so cool ;)
Sorry if I'm boring you at this point, I just find this stuff really fascinating and fun :)
———
[0]: Any two records of any two record types, as long as they each have both an `x : real` and a `y : real`, with intentional information loss:
f : {x : real, y : real, ..a} -> {x : real, y : real, ..b} -> {x : real, y : real}
(* f {x = 1.0, y = 1.2, z = 1.3} {x = 1.0, y = 2.0, w = 42}; *)
(* ^ typechecks okay!
* row type `..a` can be different from row type `..b`,
* no problem
*)
[1]: Any two records which both have the same type, which can be any record type that at least has an `x : real` and a `y : real`:
f : {x : real, y : real, ..a} -> {x : real, y : real, ..a} -> {x : real, y : real, ..a}
(* f {x = 1.0, y = 1.2, z = 1.3} {x = 1.0, y = 2.0, z = 0.0}; *)
(* ^ typechecks okay! *)
(* f {x = 1.0, y = 1.2, z = 1.3} {x = 1.0, y = 2.0, w = 42}; *)
(* ^ type error!
* the second record has a different type than the first,
* but the type of `f` demands that they be the same type,
* since the single row `..a` must match itself
*)
A largely unrelated question: do you know why most ML dialects have this weird scoping rule for record members, where they share the same scope as the record itself (and so another record cannot easily reuse the same field name)? It seems awfully inconvenient, and it feels like it could be trivially resolved by allowing reuse with an explicit disambiguation syntax. Or am I missing something?
Which dialects? Both Standard ML and OCaml can handle multiple record types with homonymous fields just fine:
$ poly
Poly/ML 5.5.2 Release
> type point2 = {x : real, y : real};
type point2 = {x: real, y: real}
> type point3 = {x : real, y : real, z : real};
type point3 = {x: real, y: real, z: real}
> let val pt = {x = 1.0, y = 2.0} in #x pt end;
val it = 1.0: real
> let val pt = {x = 3.0, y = 4.0, z = 5.0} in #x pt end;
val it = 3.0: real
>
$ ocaml
OCaml version 4.03.0
# type point2 = {x : float; y : float};;
type point2 = { x : float; y : float; }
# type point3 = {x : float; y : float; z : float};;
type point3 = { x : float; y : float; z : float; }
# let pt = {x = 1.0; y = 2.0} in pt.x;;
- : float = 1.
# let pt = {x = 3.0; y = 4.0; z = 5.0} in pt.x;;
- : float = 3.
#
The only nuance with record labels in ML, as far as I can remember, is that the type of projection operations can be ambiguous if the exact type of the record is unknown (e.g., in `(fn pt => #x pt)`, the type of `pt` cannot be inferred since it could be `point2`, `point3`, `{x : int}`, `{x : real}`, ...; but this can be disambiguated with a type annotation: `(fn (pt : point3) => #x pt)`).
Perhaps I've misunderstood the question. If so, can you give me an example?
This is weird. Last time I really did anything with ML was ages ago, and I distinctly remember fighting with the fields... I wish I could remember the context, though.
Anyway, good to know that it's definitely not OCaml!
Yeah, in my example, `R` is the row variable itself, and it represents all those other, irrelevant values in the record, while I gave it the name `_` in the type itself, since rows themselves don't have field labels, but rather represent sets of labels. In ML, the labels of the fields are part of the type, but the labels of the rows are not part of the type. Then, `..a` is a type variable representing the type of the row (it gets a distinct name because you can imagine a function which takes two separate records with two separate rows[0], or even a function which takes two records but constrains them to the same type with a single row[1]), and is akin to a type variable used for parametric polymorphism, such as `'a`, and, in Standard ML with eqtypes, `''a`.
To the best of my knowledge, the term "row" comes from The Definition of Standard ML, where the grammar given for the core language includes productions called "TyRow", "PatRow", and "ExpRow", which correspond to the syntax of record types, patterns, and expressions, respectively, but only the part in between the `{` and `}`:
(The `At` prefix means "atomic", and has a specific meaning in the definition.)So, then, a row variable is one which literally holds a sequence of label×type or label×value pairs. It sometimes even feels like it's a metavariable which holds a branch of the syntax tree the way a variable in a macro does, which might be another reason why row polymorphism feels so cool ;)
Sorry if I'm boring you at this point, I just find this stuff really fascinating and fun :)
———
[0]: Any two records of any two record types, as long as they each have both an `x : real` and a `y : real`, with intentional information loss:
[1]: Any two records which both have the same type, which can be any record type that at least has an `x : real` and a `y : real`: