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.

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.

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

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

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

You started by saying:

> Enumerated types in some way list all the values the type can have

And then said:

> X = enum | predicate is enumerated, since it has two options that it explicitly lists

But you can't list its values by your own definition. You defined types as being either A or B, and accepting that definition, you can come up with types that are neither. This is my point: your model is inconsistent. Your categorizations are not useful. You should not use that model. That is not a good way of thinking about the world.

>your thickheaded refusal to see my actual point and instead dismiss me with your confused counterpoints is just rude and unnecessary.

I honestly see myself as attempting to help you here. I see you making a mistake, and I'm trying to convince you, and to a lesser extent any other readers, not to make that mistake.

This has nothing to do with you using "wrong terminology" or not understanding type theory; I've accepted your definitions, and shown that they are inconsistent with themselves. Your math doesn't work. Your model is not helpful. The fact that you cannot define tuples of (enum, predicate) as either enum or predicate by your own definition shows that your model fails. Don't use it. Move on. Dismissing you is not rude nor unnecessary. It is highly necessary that we dismiss each others' ideas when those ideas don't work.

I get that that sounds harsh. It's great to come up with interesting ideas and categorizations. It's even better to throw them away when you realize they don't work. Do that seven thousand more times. Six thousand, nine hundred and eighty seven of them will be thrown away. The 13 remaining ones will be worth it. But you'll never get there if you cling to ones that are provably wrong. This one is. From my point of view, you are the one being thickheaded here, by clinging to this one idea as if it's the only one you'll ever have. It's not. I strongly urge you to get better at killing your own ideas to make room for new ones. Accept proofs that your ideas are wrong as improvements in your knowledge.

> From my point of view, you are the one being thickheaded here, by clinging to this one idea as if it's the only one you'll ever have.

It's just that you and I haven't yet talked about my idea yet, because you're talking about something else, then failing to realize it and thinking I'm ignoring your rebuttals because I'm stubborn rather than because they're irrelevant to my point.

Anyway I will try one more time for posterity:

> But you can't list its values by your own definition.

You have misunderstood me. The X I have described enumerates its values in the sense I am talking about: it's one or the other, type A (and enum) or B (a predicate). I am talking about it being enumerated _in terms of other things_. If for some reason you had X = A | B, as a definition, and then you the cardinalities of A or B, then you would be able to say |X| = |A| + |B| (or |A| + |B| - |A ∩ B| if they overlap). This is the sense in which algebra works. That is just... obviously true, right?

The interesting parts show up if you have recursive definitions (in which case you get these infinite series) or if some of the sets have cardinalities that you don't know how to use for algebra (like a predicate over an un-enumerable set of values...) ... but in some cases algebra still works, and I don't know the details about that.

In the case of "predicate" types, it is much harder to see how arithmetic would work in the cardinalities, because I could write down something like Prime = x: integer & isPrime(x) and regardless of how you think about |Integer| in your language/setting/etc, you have a complex predicate over integers that's not going to correspond to any obvious algebra. And yet if I wrote Q = Prime | true | false you can still say that |Q| = |P| + 2 and that works fine. On the other hand if I wrote Q = Prime | Fibonacci then good luck because Prime ∩ Fibonacci is hard to do anything with.