Adventures in Category Theory – The algebra of types (2018) | Hacker News Reader

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

miklos-martin.github.io

Great article, here's the first in the series: 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.

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`

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.

I would recommend this introduction to type theory: 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.

You're missing the distinction between isomorphic and identical.

Your two types are isomorphic. They are not equal.

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.

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.

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.)

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_in...

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.

Thank you for all the replies! I didn't know type theory was a field, so I'll go look at that.

Reply on news.ycombinator.com