3 ms·

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

by feoren 2y ago

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.

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.

by feoren 2y ago

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.