|
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 `}`: TyRow <- Label `:` Ty [ `,` TyRow ]
PatRow <- Label `=` AtPat [ `,` PatRow ]
ExpRow <- Label `=` AtExp [ `,` ExpRow ]
(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
*)
|