5 ms·

Here's a thought I have had cached in my head from a long time ago. Ignore me if this is obvious or dumb; I don't know anything about type theory really. There

by ajkjk 2y ago

Here's a thought I have had cached in my head from a long time ago. Ignore me if this is obvious or dumb; I don't know anything about type theory really. There are basically two varieties of types: predicate types and enumerated types. Predicate types are functions that return true for objects that have their type. Enumerated types in some way list all the values the type can have. So "Boolean" is an enumerated type, but "even integer" is a predicate type (you test if it's even. Nevermind that you could enumerate the even integers within your language, you wouldn't). (I'm pretty sure these varieties are dual in the category-theoretic sense of reversing arrows, but I don't know much about that either.) So what happens is that the cardinalities of enumerated types obey arithmetic, but the cardinalities of predicate types do not. Predicate types only have a notion of "cardinality" anyway when you restrict the possible values to some finite universe. The intersection of two predicate types (x -> f(x) && g(x)) may be of the same cardinality as each of the predicates (if they are equal) or it might be the same cardinality as one of them (if f(x) implies g(x) then {x | f(x)} = {x | f(x) && g(x)}) or it might be some new value entirely. All of the cases where algebra works on types is cases where they're being used as enumerated types. The usual definition of a list in functional languages ([] a = [] | a : [a] or w/e) enumerates the possibilities, hence it obeys algebra. Were it described as a predicate, on the other hand, it would not (necessarily) obey algebra.

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.
kccqzy 2y ago
When you have "predicate types" in practice you need restrictions on what kind of predicates are allowed. If you allow anything at all, that's when you get Russell's paradox. That tells us the general comprehension principle is invalid, that is, you cannot allow the construction of a set from an arbitrary predicate (or definite condition). > Predicate types only have a notion of "cardinality" anyway when you restrict the possible values to some finite universe. It is much more subtle than that. Regular set theory allows cardinalities far bigger than the least infinite cardinal, aleph-zero. But of course it's computers that we are talking about. Even then it's wrong. What if I define a predicate that's returns true for every natural number? Then it's infinite. But what if I define a complicated enough predicate that it does not halt for some numbers? Then we get back a recursively enumerable set that may or may not be infinite. In essence, when you introduce predicates, you no longer really care about cardinalities you start to care about the complexity of the predicates. For your purpose, your predicate has to be sufficiently simple that it denotes a recursive set (not a recursively enumerable set).
- ajkjk 2y ago
  As a predicate Russell's paradox translates to an infinite loop in programming, not an impossibility. And yes, you get in trouble if you define a set from an arbitrary predicate, but a type is not (necessarily) a set: a type can be a predicate without asking that it be explicitly cast as a set. You can certainly consider the "set of all lists", but you can't enumerate it, because you can have a list of any type and you don't know all the types that can be put into a list. Anyway, I feel like you missed my point. It's that, if you are wondering why types seem to obey algebra but ALSO obey the laws of set theory and the two seem compatible, that this is why: predicates obey the algebra of sets while enumerated types have cardinalities which obey algebra.

by ajkjk 2y ago

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.

kccqzy 2y ago

When you have "predicate types" in practice you need restrictions on what kind of predicates are allowed. If you allow anything at all, that's when you get Russell's paradox. That tells us the general comprehension principle is invalid, that is, you cannot allow the construction of a set from an arbitrary predicate (or definite condition). > Predicate types only have a notion of "cardinality" anyway when you restrict the possible values to some finite universe. It is much more subtle than that. Regular set theory allows cardinalities far bigger than the least infinite cardinal, aleph-zero. But of course it's computers that we are talking about. Even then it's wrong. What if I define a predicate that's returns true for every natural number? Then it's infinite. But what if I define a complicated enough predicate that it does not halt for some numbers? Then we get back a recursively enumerable set that may or may not be infinite. In essence, when you introduce predicates, you no longer really care about cardinalities you start to care about the complexity of the predicates. For your purpose, your predicate has to be sufficiently simple that it denotes a recursive set (not a recursively enumerable set).

ajkjk 2y ago
As a predicate Russell's paradox translates to an infinite loop in programming, not an impossibility. And yes, you get in trouble if you define a set from an arbitrary predicate, but a type is not (necessarily) a set: a type can be a predicate without asking that it be explicitly cast as a set. You can certainly consider the "set of all lists", but you can't enumerate it, because you can have a list of any type and you don't know all the types that can be put into a list. Anyway, I feel like you missed my point. It's that, if you are wondering why types seem to obey algebra but ALSO obey the laws of set theory and the two seem compatible, that this is why: predicates obey the algebra of sets while enumerated types have cardinalities which obey algebra.