3 ms·

> Thank you for the clarification! No problem! The difference between the two was something I personally struggled with at first, so now I feel like I've got

> Thank you for the clarification! No problem! The difference between the two was something I personally struggled with at first, so now I feel like I've got a pretty good grasp on it. Funny how that works ;) I don't see anything here in the TypeScript docs that looks like row polymorphism. Without a row variable somewhere in the type (even if it's inferred), I'm not sure it could be considered row polymorphism. However, they could be doing something fancy with their notion of type compatibility that avoids information loss without introducing row variables (which, I think, would similarly imply a lack of subsumption[0], and might not be sound, but the docs admit the system is unsound in places). It's also possible that every record type in TS carries an implicit row variable. The important part is the (lack of) information loss, and good way to tell would be to construct a test case like the one I wrote above and see if you wind up losing your `z` field (information loss => subsumption => "by-the-book" subtyping). This all reminds me that I've been meaning to spend some time with TypeScript :) [0]: I've known type theorists who claim that without subsumption, there is no subtyping. I disagree because I think the fundamental/important part of subtyping is the subtyping relation itself.

int_19h 10y ago
I actually didn't fully understand your example originally (I missed the part where ".." now has a name!). I grok it now, and yeah, TS doesn't have it - there's simply no type-safe way to write a function like that (of course, TS being a strict superset of JS, you can still write it, it just won't typecheck). It appears that this was discussed in the context of supporting the ES7 "spread" operator, since row variable is the obvious typed counterpart to that: https://github.com/Microsoft/TypeScript/issues/2103 https://github.com/Microsoft/TypeScript/issues/2103 but they ended up implementing just the operator, without a way to reflect it in a function signature: https://github.com/Microsoft/TypeScript/pull/11150 https://github.com/Microsoft/TypeScript/pull/11150 However: "I expect a spread type or something similar to be available in future versions of TypeScript."
- groovy2shoes 10y ago
  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 *)

int_19h 10y ago

I actually didn't fully understand your example originally (I missed the part where ".." now has a name!). I grok it now, and yeah, TS doesn't have it - there's simply no type-safe way to write a function like that (of course, TS being a strict superset of JS, you can still write it, it just won't typecheck). It appears that this was discussed in the context of supporting the ES7 "spread" operator, since row variable is the obvious typed counterpart to that: https://github.com/Microsoft/TypeScript/issues/2103 https://github.com/Microsoft/TypeScript/issues/2103 but they ended up implementing just the operator, without a way to reflect it in a function signature: https://github.com/Microsoft/TypeScript/pull/11150 https://github.com/Microsoft/TypeScript/pull/11150 However: "I expect a spread type or something similar to be available in future versions of TypeScript."

groovy2shoes 10y ago
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 *)