3 ms·

I really don't like this view (but looks like I'm a small minority). Types shouldn't have an algebra similar to numbers, they should have an algebra similar to

I really don't like this view (but looks like I'm a small minority). Types shouldn't have an algebra similar to numbers, they should have an algebra similar to sets. While for numbers A + A + A = 3A, on sets A ∪ A ∪ A = A. Types are all about predicate satisfaction, and predicates don't change their value because they can be proven in more than one way. In practice, defining type sums as tagged sums leads to your algebra, and also leads to a lot of confusion between structure and denomination that would be completely avoided if sums and tags were independent operations.

paholg 2y ago
The difference is mostly a matter of perspective, isn't it? In Rust, if I have ``` enum Foo { A(u32), B(u32), C(u32), } ``` Then the number of representable states is deduced my an "algebra of numbers", but the size is deduced by an "algebra of sets". For example, the size of Foo is just 8 (4 bytes for u32, and 4 for the tag + alignment).
- marcosdumay 2y ago
  Given the types: I = A + B; J = C; X = A; Y = B + C Is I + J the same type as X + Y? If your types are tagged, they aren't. Because that's what tags do.
  - paholg 2y ago
    Okay? I don't know what point you're making.
  - bombela 2y ago
    My answer would be: No they are not the same type. Yes they have the same amount of bits representing them. They might have different RAM usage because of alignment.
  - xigoi 2y ago
    > Is I + J the same type as X + Y? They are not the same, but they are isomorphic. Just like with (A×B)×C versus A×(B×C).
ajkjk 2y ago
Here's a thought I have had cached in my head from a long time ago. Ignore me if this is obvious or dumb; I don't know anything about type theory really. There are basically two varieties of types: predicate types and enumerated types. Predicate types are functions that return true for objects that have their type. Enumerated types in some way list all the values the type can have. So "Boolean" is an enumerated type, but "even integer" is a predicate type (you test if it's even. Nevermind that you could enumerate the even integers within your language, you wouldn't). (I'm pretty sure these varieties are dual in the category-theoretic sense of reversing arrows, but I don't know much about that either.) So what happens is that the cardinalities of enumerated types obey arithmetic, but the cardinalities of predicate types do not. Predicate types only have a notion of "cardinality" anyway when you restrict the possible values to some finite universe. The intersection of two predicate types (x -> f(x) && g(x)) may be of the same cardinality as each of the predicates (if they are equal) or it might be the same cardinality as one of them (if f(x) implies g(x) then {x | f(x)} = {x | f(x) && g(x)}) or it might be some new value entirely. All of the cases where algebra works on types is cases where they're being used as enumerated types. The usual definition of a list in functional languages ([] a = [] | a : [a] or w/e) enumerates the possibilities, hence it obeys algebra. Were it described as a predicate, on the other hand, it would not (necessarily) obey algebra.
- feoren 2y ago
  I don't think a distinction between "predicate types" and "enumerated types" is particularly useful. As you pointed out, you can enumerate all even integers. All enumerated types can be represented as predicate types instead, with the predicate "does this belong to the enumerated set?". All countably infinite predicate types can be enumerated. So focusing on the difference seems like a red herring to me. > All of the cases where algebra works on types is cases where they're being used as enumerated types. No, algebra works perfectly fine "predicate types" as well, because all the predicate types we care about (constructible / countably infinite) are enumerable too. > Predicate types only have a notion of "cardinality" anyway when you restrict the possible values to some finite universe. No, there are infinite cardinalities.
  - 2y ago
nine_k 2y ago
It depends on what operations you pick. I like ML-style operations on types because they make set-theoretic sense. C = A + B means that type C is a union of A and B, aka a "sum type", so its cardinality is the sum of cardinalities of A and B. In Typescript or Python terms, C = A | B, which I read that an element of type C can be either an element of A or an element of B. C = A * B means that C is a Cartesian product of A and B, and its cardinality is the product of those of A and B. In Python terms, C = tuple[A, B]. Hence something like Point = {x: number, y: number, z: number} is not "3 * number", but number^3, because it's a point in the R^3 space.
- marcosdumay 2y ago
  > C is a union of A and B, aka a "sum type", so its cardinality is the sum of cardinalities of A and B That's exactly what's wrong. The cardinality is len(A ∪ B) = len(A) + len(B) - len(A ∩ B). Also, the Cartesian product is a tagged operation. It literally creates a result where you access the elements by index.
  - nine_k 2y ago
    We reasonably assume that A ∩ B = ∅ in all practical cases, such as `int | None` or `string | number `, etc. Yes, a Cartesian product is tagged (each axis is), but it does not affect the fact that len(A * B) = len(A) * len(B), hence it's logical to use multiplication to denote "record types".
    - marcosdumay 2y ago
      That's not a good assumption, and even the original example is Bool + Bool; len(Bool ∪ Bool) = 2 * len(Bool) is trivially false. About the Cartesian product, the tags create that rule. Untagged multiplication again has fewer elements.
ndriscoll 2y ago
The "correct" (in the categorical sense) sum operation for sets is disjoint (tagged) union, not union. So A + A + A = A ∐ A ∐ A, which is isomorphic to 3*A = (3,A) (i.e. each element of A ∐ A ∐ A carries the information of a tag from 3 and an element of A). All is well.
syrak 2y ago
IMO your view, if not common, is kinda intuitive from the point of view of someone trained in set theory/classical logic (i.e., most people before they find an interest in type theory; I myself was here a few years ago). If it feels like you're in a minority, it's because most others who might have the same opinion haven't reached the point where they could articulate it; many just give up way earlier on understanding type theory. It certainly makes sense to a set theorist that union and intersection are more primitive than sums and products. From that perspective, type theory seems like a roundabout and unnecessary way of doing things. The challenge is to imagine type theory as a radically different foundation to logic (because that's what it is), with sums and products as primitives instead, for one superficial difference. It's hard to explain in words. I personally didn't get it without years of first-hand experience with proof assistants based on type theory. Constructivism and category theory are other possible gateways into the right mindset. There is one key difference which I think highlights the charm and simplicity of type theory without delving in technical details too much. The syntax of set theory is in two layers: there are sets, and there are propositions (about elements of those sets). In contrast, there is only one such "layer" in (dependent) type theory: types. Types play the role of both sets and propositions if you want to encode set theory in type theory. The point is that types can be much more than either of those things, and that idea is inherently difficult to convey to someone whose only conception of logic is sets and propositions.
kccqzy 2y ago
You are not wrong but you are indeed a minority. If you read research papers you will definitely find papers that use union in the way you describe (when it comes to subtyping), and then use a different notation for record extension (basically the kind of discriminated union operator). It's essential to differentiate between them using different notations. For the former, for example the Animal class and the Cat class are unioned into the Animal superclass. For the latter, you have an Animal object and a Cat object that's separate.

paholg 2y ago

The difference is mostly a matter of perspective, isn't it? In Rust, if I have ``` enum Foo { A(u32), B(u32), C(u32), } ``` Then the number of representable states is deduced my an "algebra of numbers", but the size is deduced by an "algebra of sets". For example, the size of Foo is just 8 (4 bytes for u32, and 4 for the tag + alignment).

marcosdumay 2y ago
Given the types: I = A + B; J = C; X = A; Y = B + C Is I + J the same type as X + Y? If your types are tagged, they aren't. Because that's what tags do.
- paholg 2y ago
  Okay? I don't know what point you're making.
- bombela 2y ago
  My answer would be: No they are not the same type. Yes they have the same amount of bits representing them. They might have different RAM usage because of alignment.
- xigoi 2y ago
  > Is I + J the same type as X + Y? They are not the same, but they are isomorphic. Just like with (A×B)×C versus A×(B×C).

ajkjk 2y ago

Here's a thought I have had cached in my head from a long time ago. Ignore me if this is obvious or dumb; I don't know anything about type theory really. There are basically two varieties of types: predicate types and enumerated types. Predicate types are functions that return true for objects that have their type. Enumerated types in some way list all the values the type can have. So "Boolean" is an enumerated type, but "even integer" is a predicate type (you test if it's even. Nevermind that you could enumerate the even integers within your language, you wouldn't). (I'm pretty sure these varieties are dual in the category-theoretic sense of reversing arrows, but I don't know much about that either.) So what happens is that the cardinalities of enumerated types obey arithmetic, but the cardinalities of predicate types do not. Predicate types only have a notion of "cardinality" anyway when you restrict the possible values to some finite universe. The intersection of two predicate types (x -> f(x) && g(x)) may be of the same cardinality as each of the predicates (if they are equal) or it might be the same cardinality as one of them (if f(x) implies g(x) then {x | f(x)} = {x | f(x) && g(x)}) or it might be some new value entirely. All of the cases where algebra works on types is cases where they're being used as enumerated types. The usual definition of a list in functional languages ([] a = [] | a : [a] or w/e) enumerates the possibilities, hence it obeys algebra. Were it described as a predicate, on the other hand, it would not (necessarily) obey algebra.

feoren 2y ago
I don't think a distinction between "predicate types" and "enumerated types" is particularly useful. As you pointed out, you can enumerate all even integers. All enumerated types can be represented as predicate types instead, with the predicate "does this belong to the enumerated set?". All countably infinite predicate types can be enumerated. So focusing on the difference seems like a red herring to me. > All of the cases where algebra works on types is cases where they're being used as enumerated types. No, algebra works perfectly fine "predicate types" as well, because all the predicate types we care about (constructible / countably infinite) are enumerable too. > Predicate types only have a notion of "cardinality" anyway when you restrict the possible values to some finite universe. No, there are infinite cardinalities.
- 2y ago

nine_k 2y ago

It depends on what operations you pick. I like ML-style operations on types because they make set-theoretic sense. C = A + B means that type C is a union of A and B, aka a "sum type", so its cardinality is the sum of cardinalities of A and B. In Typescript or Python terms, C = A | B, which I read that an element of type C can be either an element of A or an element of B. C = A * B means that C is a Cartesian product of A and B, and its cardinality is the product of those of A and B. In Python terms, C = tuple[A, B]. Hence something like Point = {x: number, y: number, z: number} is not "3 * number", but number^3, because it's a point in the R^3 space.

marcosdumay 2y ago
> C is a union of A and B, aka a "sum type", so its cardinality is the sum of cardinalities of A and B That's exactly what's wrong. The cardinality is len(A ∪ B) = len(A) + len(B) - len(A ∩ B). Also, the Cartesian product is a tagged operation. It literally creates a result where you access the elements by index.
- nine_k 2y ago
  We reasonably assume that A ∩ B = ∅ in all practical cases, such as `int | None` or `string | number `, etc. Yes, a Cartesian product is tagged (each axis is), but it does not affect the fact that len(A * B) = len(A) * len(B), hence it's logical to use multiplication to denote "record types".
  - marcosdumay 2y ago
    That's not a good assumption, and even the original example is Bool + Bool; len(Bool ∪ Bool) = 2 * len(Bool) is trivially false. About the Cartesian product, the tags create that rule. Untagged multiplication again has fewer elements.

ndriscoll 2y ago

The "correct" (in the categorical sense) sum operation for sets is disjoint (tagged) union, not union. So A + A + A = A ∐ A ∐ A, which is isomorphic to 3*A = (3,A) (i.e. each element of A ∐ A ∐ A carries the information of a tag from 3 and an element of A). All is well.

syrak 2y ago

IMO your view, if not common, is kinda intuitive from the point of view of someone trained in set theory/classical logic (i.e., most people before they find an interest in type theory; I myself was here a few years ago). If it feels like you're in a minority, it's because most others who might have the same opinion haven't reached the point where they could articulate it; many just give up way earlier on understanding type theory. It certainly makes sense to a set theorist that union and intersection are more primitive than sums and products. From that perspective, type theory seems like a roundabout and unnecessary way of doing things. The challenge is to imagine type theory as a radically different foundation to logic (because that's what it is), with sums and products as primitives instead, for one superficial difference. It's hard to explain in words. I personally didn't get it without years of first-hand experience with proof assistants based on type theory. Constructivism and category theory are other possible gateways into the right mindset. There is one key difference which I think highlights the charm and simplicity of type theory without delving in technical details too much. The syntax of set theory is in two layers: there are sets, and there are propositions (about elements of those sets). In contrast, there is only one such "layer" in (dependent) type theory: types. Types play the role of both sets and propositions if you want to encode set theory in type theory. The point is that types can be much more than either of those things, and that idea is inherently difficult to convey to someone whose only conception of logic is sets and propositions.

kccqzy 2y ago

You are not wrong but you are indeed a minority. If you read research papers you will definitely find papers that use union in the way you describe (when it comes to subtyping), and then use a different notation for record extension (basically the kind of discriminated union operator). It's essential to differentiate between them using different notations. For the former, for example the Animal class and the Cat class are unioned into the Animal superclass. For the latter, you have an Animal object and a Cat object that's separate.