3 ms·
> 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
by ajkjk 2y ago
> 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.