3 ms·

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

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

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

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.