5 ms·

Adventures in Category Theory – The algebra of types (2018)

Zababa 5y ago
> If our objects are sets (as they are in the category of types and functions) And from the previous article: > What I do love about category theory is that it is not some framework, or design pattern, or best practice that somebody came up with empirically because it helped them solve their problem, but it has strong mathematical foundations. It always adds up, things click smoothly, and it is just so satisfying and fun to experience this. I was thinking about that in the context of nominal and structural typing. From my (limited) understanding, set theory is equivalent to structural typing. That would mean the following: type point = { x: int; y: int } type my_point = { x: int; y: int } let example (p: point) = p.x + p.y let po: point = { x = 5; y = 6 } let my_po: my_point = { x = 1; y = 2 } example po // => 11 example my_po // => type error should typecheck, as point and my_point are exactly the same from a "set" point of view. But they don't. It's like naming the record made them different types even if they are structurally the same. So this is something I don't understand. I feel like I'm missing something, but I don't know what.
- chriswarbo 5y ago
  One major difference between types and sets (certainly between type theory and set theory) is that set membership is a proposition, e.g. all of the following are perfectly reasonable expressions, which ask whether or not a value exists in a set: po ∈ point // Valid statement, which happens to be true po ∈ my_point // Valid statement, which happens to be false my_po ∈ point // Valid statement, which happens to be false my_po ∈ my_point // Valid statement, which happens to be true However, type membership is not a question; it's part of a definition. We may choose to add "annotations" to some expressions, but they only act as sanity checks; they are logically/computationally irrelevant: po : point // Valid expression, since the annotation passes the type checker; equivalent to `po` po : my_point // Invalid expression, since the annotation doesn't pass the type checker my_po : point // Invalid expression, since the annotation doesn't pass the type checker my_po : my_point // Valid expression, since the annotation passes the type checker; equivalent to `my_po`
  - Koshkin 5y ago
    Another way of stating this is to say that sets are “extensional” and types are “intensional,” which means that a set is defined by imposing conditions (constraints) on the membership or by simply listing the objects, while a type is defined by describing its “meaning,” e.g. by specifying operations on objects.
- 4ad 5y ago
  I would recommend this introduction to type theory: https://arxiv.org/abs/1601.05035 https://arxiv.org/abs/1601.05035. While it's about HoTT, it starts with a very clear general-audience explanation on why and how type theory is different from set theory.
- contravariant 5y ago
  You're missing the distinction between isomorphic and identical. Your two types are isomorphic. They are not equal.
  - Koshkin 5y ago
    Isomorphism means having the same “interface.” Unless you specify, for each structure, a different set of operations (functions), what’s left is their, well, structures, which in this case are identical.
    - contravariant 5y ago
      Admittedly it's up to the language whether those two types should be considered identical or not, but there's nothing wrong with considering them unequal.
      - Koshkin 5y ago
        Yes, as long as there is a particular intent behind each structure even if their “form” is the same. Simply giving different names (to the structures themselves and, especially, to their respective fields) might hint to that. (The field names, in particular, should be considered part of the “interface,” actually.)
    - nextaccountic 5y ago
      The problem with isomorphism is that there are many ways two types can be considered isomorphic. For example, { x: int, y: int } and { a: int, b: int } are isomorphic, but in two different ways: one that assigns x to a and y to b, and another that assigns x to b and y to a. The case where each type has identical field names ({ x: int, y: int } and { x: int, y: int }) induces an structural equality that is the isomorphism that you expect, but there's also another that swaps x and y. (I think that "structural equality" is what you want, after all) Structural typing (and even better, row typing) is nice for specifying ad-hoc APIs but they don't scale much. In the general case, when you have two types that refer to the same thing but were written by two entirely different teams, it will be very rare for them to be structurally identical even in field names. In those cases it's better to (also) specify a general facility for converting between types, like Rust's From and Into traits, and a facility to auto-derive them in simple cases https://doc.rust-lang.org/rust-by-example/conversion/from_into.html https://doc.rust-lang.org/rust-by-example/conversion/from_in...
- Koshkin 5y ago
  The structure is not all that defines a type, you also need to include in its definition (explicitly or implicitly) a set of operations (functions) which may well be different for the structures that otherwise “look” the same.
- Zababa 5y ago
  Thank you for all the replies! I didn't know type theory was a field, so I'll go look at that.
brainwipe 5y ago
Great article, here's the first in the series: https://miklos-martin.github.io/learn/fp/category-theory/2018/01/29/adventures-in-category-theory-introduction.html https://miklos-martin.github.io/learn/fp/category-theory/201...

> If our objects are sets (as they are in the category of types and functions) And from the previous article: > What I do love about category theory is that it is not some framework, or design pattern, or best practice that somebody came up with empirically because it helped them solve their problem, but it has strong mathematical foundations. It always adds up, things click smoothly, and it is just so satisfying and fun to experience this. I was thinking about that in the context of nominal and structural typing. From my (limited) understanding, set theory is equivalent to structural typing. That would mean the following: type point = { x: int; y: int } type my_point = { x: int; y: int } let example (p: point) = p.x + p.y let po: point = { x = 5; y = 6 } let my_po: my_point = { x = 1; y = 2 } example po // => 11 example my_po // => type error should typecheck, as point and my_point are exactly the same from a "set" point of view. But they don't. It's like naming the record made them different types even if they are structurally the same. So this is something I don't understand. I feel like I'm missing something, but I don't know what.

chriswarbo 5y ago
One major difference between types and sets (certainly between type theory and set theory) is that set membership is a proposition, e.g. all of the following are perfectly reasonable expressions, which ask whether or not a value exists in a set: po ∈ point // Valid statement, which happens to be true po ∈ my_point // Valid statement, which happens to be false my_po ∈ point // Valid statement, which happens to be false my_po ∈ my_point // Valid statement, which happens to be true However, type membership is not a question; it's part of a definition. We may choose to add "annotations" to some expressions, but they only act as sanity checks; they are logically/computationally irrelevant: po : point // Valid expression, since the annotation passes the type checker; equivalent to `po` po : my_point // Invalid expression, since the annotation doesn't pass the type checker my_po : point // Invalid expression, since the annotation doesn't pass the type checker my_po : my_point // Valid expression, since the annotation passes the type checker; equivalent to `my_po`
- Koshkin 5y ago
  Another way of stating this is to say that sets are “extensional” and types are “intensional,” which means that a set is defined by imposing conditions (constraints) on the membership or by simply listing the objects, while a type is defined by describing its “meaning,” e.g. by specifying operations on objects.
4ad 5y ago
I would recommend this introduction to type theory: https://arxiv.org/abs/1601.05035 https://arxiv.org/abs/1601.05035. While it's about HoTT, it starts with a very clear general-audience explanation on why and how type theory is different from set theory.
contravariant 5y ago
You're missing the distinction between isomorphic and identical. Your two types are isomorphic. They are not equal.
- Koshkin 5y ago
  Isomorphism means having the same “interface.” Unless you specify, for each structure, a different set of operations (functions), what’s left is their, well, structures, which in this case are identical.
  - contravariant 5y ago
    Admittedly it's up to the language whether those two types should be considered identical or not, but there's nothing wrong with considering them unequal.
    - Koshkin 5y ago
      Yes, as long as there is a particular intent behind each structure even if their “form” is the same. Simply giving different names (to the structures themselves and, especially, to their respective fields) might hint to that. (The field names, in particular, should be considered part of the “interface,” actually.)
  - nextaccountic 5y ago
    The problem with isomorphism is that there are many ways two types can be considered isomorphic. For example, { x: int, y: int } and { a: int, b: int } are isomorphic, but in two different ways: one that assigns x to a and y to b, and another that assigns x to b and y to a. The case where each type has identical field names ({ x: int, y: int } and { x: int, y: int }) induces an structural equality that is the isomorphism that you expect, but there's also another that swaps x and y. (I think that "structural equality" is what you want, after all) Structural typing (and even better, row typing) is nice for specifying ad-hoc APIs but they don't scale much. In the general case, when you have two types that refer to the same thing but were written by two entirely different teams, it will be very rare for them to be structurally identical even in field names. In those cases it's better to (also) specify a general facility for converting between types, like Rust's From and Into traits, and a facility to auto-derive them in simple cases https://doc.rust-lang.org/rust-by-example/conversion/from_into.html https://doc.rust-lang.org/rust-by-example/conversion/from_in...
Koshkin 5y ago
The structure is not all that defines a type, you also need to include in its definition (explicitly or implicitly) a set of operations (functions) which may well be different for the structures that otherwise “look” the same.
Zababa 5y ago
Thank you for all the replies! I didn't know type theory was a field, so I'll go look at that.

brainwipe 5y ago

Great article, here's the first in the series: https://miklos-martin.github.io/learn/fp/category-theory/2018/01/29/adventures-in-category-theory-introduction.html https://miklos-martin.github.io/learn/fp/category-theory/201...