3 ms·

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

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

ajkjk 2y ago
I think you've misunderstood me. If the predicate types are enumerable then they're not predicate types, they're enumerated types. And if the enumeration turns out to be infinite then you get the algebra of infinite cardinals, not the algebra of numbers, which looks very different. But it still explains why they obey algebra.
- kccqzy 2y ago
  I don't understand you. Everything you can do on a computer is enumerable. So every type is enumerable. Then predicate types don't exist. Infinite cardinals are not very useful when it comes to computers because there's only one infinite cardinal that's relevant: aleph-zero. All other infinite cardinals are beyond what computers can handle.
  - ajkjk 2y ago
    I'm not talking about the notion of enumerable sets. I'm talking about whether a type explicit enumerates its members (like A = B | C or A = [] | [A]) or whether it is a contract which does not know how many members it has (like a class Foo, or a predicate like "lists of Foos" or just "even integers". You can do algebra on the former, including sometimes divergent-series style algebra like writing 1/(1-X) = 1 + X + X^2 + ...; you can't do algebra on the latter. It doesn't matter that you could in principle enumerate the, say, the even integers, either finitely (since there are finite values in your chosen language) or infinitely (in the sense of having cardinality aleph-zero). It matters whether the type definition does that. If the definition of an even integer was `Even = [] | S^2(Even)` with S as the successor function, then it would fall in the first category and some algebra on the type would work (although it would be silly to do that).
    - feoren 2y ago
      > I'm talking about whether a type explicit enumerates its members (like A = B | C or A = [] | [A]) or whether it is a contract which does not know how many members it has And I'm asserting that this is an implementation detail that doesn't matter to type theory and would be unnecessary and distracting to think about. > you can't do algebra on the latter. Yes, you can. You can take sum types and cross products of the latter. You can use them as "type variables" in "type algebraic equations" That's what "doing algebra" on types means. Whether or not you can count how many members are in the result. > It doesn't matter that you could in principle enumerate the [type] ... It matters whether the type definition does that. This is the root of our disagreement. You should be able to replace the definition (implementation) of a type, e.g. a list of the even integers between 0 and 100, with an equivalent definition (implementation), e.g. "all integers x such that x is even and x is between 0 and 100", and your type theory must not care. If your type theory cares about the exact implementation details of your type, it's hard to even call it a theory at all, because it's not working at a consistent level of abstraction. "Replace implementation with equivalent implementation" must always be invisible to everything operating in higher abstraction levels. From the point of view of any reasonable type theory, enumerated types and predicate types are interchangeable. Question: take type X to be the cross product of some predicate type and some enumerated type. Is X enumerated or predicate? You've claimed they can't overlap. Which is it? A type theory that frets over this distinction is a bad type theory. Imagine trying to categorize all your functions as either "bit-fiddling": those that use bit manipulation to calculate, and "arithmetic": those that use + - * / to calculate. Who cares? You can convert one to the other. You can do both at once. It's an implementation detail of your function and you should not be worrying about it at the functional abstraction level.
      - ajkjk 2y ago
        > take type X to be the cross product of some predicate type and some enumerated type. Is X enumerated or predicate? You've claimed they can't overlap. A type like X = enum | predicate is enumerated, since it has two options that it explicitly lists, one of which happens to be a predicate. > Yes, you can. You can take sum types and cross products of the latter. You are talking about a different kind of algebra than I am, which should be pretty obvious from the context of this conversation. This was all in reply to somebody who was put off by the fact that you can do literal actual algebra on types, like L(A) = 1 + A * L(A) and then rearrange it into an infinite sum, and was saying that types ought to be obey something like set algebra instead, wherein A ∪ A = A. I am saying, the sense in which the former algebra works is due to the existence of types which enumerate their variants and therefore act like numbers (or, like, decategorify to numbers, or w/e). Anyway, I understand that I am not well-versed in type-theory, but your thickheaded refusal to see my actual point and instead dismiss me with your confused counterpoints is just rude and unnecessary. Although I might be saying something in slightly incorrect terminology or missing something subtle, I'm not missing the non-subtle things you're saying and it should really not be hard to see the sense of what I'm getting at. So... cut it out, please.

by feoren 2y ago

ajkjk 2y ago

I think you've misunderstood me. If the predicate types are enumerable then they're not predicate types, they're enumerated types. And if the enumeration turns out to be infinite then you get the algebra of infinite cardinals, not the algebra of numbers, which looks very different. But it still explains why they obey algebra.

kccqzy 2y ago
I don't understand you. Everything you can do on a computer is enumerable. So every type is enumerable. Then predicate types don't exist. Infinite cardinals are not very useful when it comes to computers because there's only one infinite cardinal that's relevant: aleph-zero. All other infinite cardinals are beyond what computers can handle.
- ajkjk 2y ago
  I'm not talking about the notion of enumerable sets. I'm talking about whether a type explicit enumerates its members (like A = B | C or A = [] | [A]) or whether it is a contract which does not know how many members it has (like a class Foo, or a predicate like "lists of Foos" or just "even integers". You can do algebra on the former, including sometimes divergent-series style algebra like writing 1/(1-X) = 1 + X + X^2 + ...; you can't do algebra on the latter. It doesn't matter that you could in principle enumerate the, say, the even integers, either finitely (since there are finite values in your chosen language) or infinitely (in the sense of having cardinality aleph-zero). It matters whether the type definition does that. If the definition of an even integer was `Even = [] | S^2(Even)` with S as the successor function, then it would fall in the first category and some algebra on the type would work (although it would be silly to do that).
  - feoren 2y ago
    > I'm talking about whether a type explicit enumerates its members (like A = B | C or A = [] | [A]) or whether it is a contract which does not know how many members it has And I'm asserting that this is an implementation detail that doesn't matter to type theory and would be unnecessary and distracting to think about. > you can't do algebra on the latter. Yes, you can. You can take sum types and cross products of the latter. You can use them as "type variables" in "type algebraic equations" That's what "doing algebra" on types means. Whether or not you can count how many members are in the result. > It doesn't matter that you could in principle enumerate the [type] ... It matters whether the type definition does that. This is the root of our disagreement. You should be able to replace the definition (implementation) of a type, e.g. a list of the even integers between 0 and 100, with an equivalent definition (implementation), e.g. "all integers x such that x is even and x is between 0 and 100", and your type theory must not care. If your type theory cares about the exact implementation details of your type, it's hard to even call it a theory at all, because it's not working at a consistent level of abstraction. "Replace implementation with equivalent implementation" must always be invisible to everything operating in higher abstraction levels. From the point of view of any reasonable type theory, enumerated types and predicate types are interchangeable. Question: take type X to be the cross product of some predicate type and some enumerated type. Is X enumerated or predicate? You've claimed they can't overlap. Which is it? A type theory that frets over this distinction is a bad type theory. Imagine trying to categorize all your functions as either "bit-fiddling": those that use bit manipulation to calculate, and "arithmetic": those that use + - * / to calculate. Who cares? You can convert one to the other. You can do both at once. It's an implementation detail of your function and you should not be worrying about it at the functional abstraction level.
    - ajkjk 2y ago
      > take type X to be the cross product of some predicate type and some enumerated type. Is X enumerated or predicate? You've claimed they can't overlap. A type like X = enum | predicate is enumerated, since it has two options that it explicitly lists, one of which happens to be a predicate. > Yes, you can. You can take sum types and cross products of the latter. You are talking about a different kind of algebra than I am, which should be pretty obvious from the context of this conversation. This was all in reply to somebody who was put off by the fact that you can do literal actual algebra on types, like L(A) = 1 + A * L(A) and then rearrange it into an infinite sum, and was saying that types ought to be obey something like set algebra instead, wherein A ∪ A = A. I am saying, the sense in which the former algebra works is due to the existence of types which enumerate their variants and therefore act like numbers (or, like, decategorify to numbers, or w/e). Anyway, I understand that I am not well-versed in type-theory, but your thickheaded refusal to see my actual point and instead dismiss me with your confused counterpoints is just rude and unnecessary. Although I might be saying something in slightly incorrect terminology or missing something subtle, I'm not missing the non-subtle things you're saying and it should really not be hard to see the sense of what I'm getting at. So... cut it out, please.