4 ms·

>types are constructive. Thus, the cardinality of any given type is at most countably infinite, and thus axiom of choice is undeniably valid for types. Sequenc

>types are constructive. Thus, the cardinality of any given type is at most countably infinite, and thus axiom of choice is undeniably valid for types. Sequences of rational numbers are the usual way of constructing reals, and f(n): N -> Q is a both a sequence of rational numbers and a valid type in almost any language. Does that type include every sequence of rationals or only those that could be produced by a program in that programming language? I guess there is a third option, that it would represent all computable sequences, but is the computability of a sequence decidable? The question of whether or not the function will ever return if asked for the nth value certainly isn't.

colanderman 5y ago
I think most languages (implicitly) define `->` to include all such functions, not just those which could be defined by the language itself. Otherwise it would not be possible to describe the type of builtin or foreign-language library functions, which often exist explicitly to circumvent language restrictions. Even constructive logic languages (e.g. Coq) adhere to this definition I believe, else it would be impossible to introduce axioms.
gowld 5y ago
Andrej Bauer is a great resource twitter.com/andrejbauer/status/1212737159217762304 http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/ http://math.andrej.com/2008/02/06/representations-of-uncompu... > constructive mathematics does not assume that all reals are computable or constructive. It is agnostic about which reals there are. Basically, in a computer, the "set of all reals" is irrelevant, only the set of computable reals matters. (And you can represent many reals without infinite sequenecs, even some exotic ones. You don't need "infinite precision rational approximation", you just need enough precision to disambiguate from all other reals in your program.)
jerf 5y ago
It can be helpful in the computer-science (as considered as studying real machines, not infinite machines) context to very explicitly consider types as literally what they will be in the computer's memory. For instance, an "int64" in languages that support that type is not "an integer" which may be of unbounded size. It is specifically 2*64 values, and no others. Things like strings can be imagined as a family of types, one for each size, or as a new sort of thing that can be variable length, but still has a strongly-characterizable upper limit. It is also valid to consider mathematical types, of course. My point here is not to confuse the two, though. You will make a big mess of things if you are switching back and forth between types that can be represented in real machines and math types without realizing it. Mathematical types turn out to be tricky ways of viewing real programs, because they're much simpler to work with [1] but will bite you when you least expect it if you're not careful when real machine limits affect you. [1]: One of the things that a lot of people find counterintuitive is why it's simpler to have things like "infinite tapes" and other infinities in the math. The reason is, in a real machine when you reach for another byte in RAM, you have two cases to consider: 1. it's there and 2. it's not. If you have "infinite" RAM, you only have one case. Trying to do real proofs on real machines is a this never ending proliferation of cases to worry about that the infinities make go away. Personally I think of almost every "infinite" that shows up in computer science as the English word "unbounded" instead. It's not that there's literally infinite cells, it's just, you'll never reach for another one and be told it's not there, but at any given point, consumption of whatever resource is finite.
- colanderman 5y ago
  Not quite literally, I would argue -- in almost all modern languages, `int64` doesn't mean just "all 64-bit bit patterns", it means more specifically: "a 64-bit bit pattern in a context in which the program text interprets as an integer value". I.e., although any given `float` bit pattern (member of the set GF(2)^64) is also an `int64` bit pattern (member of the same set), a value of type `float` is not a value of type `int64`. Alternatively -- the type `int64` is comprised of 2^64 discrete values, distinct from the 2^64 discrete values comprising `float`, which happen to have 64-bit representations which overlap.
  - jerf 5y ago
    I would certainly call that another useful and valid perspective. Again, the real thing is to make sure you don't accidentally flipflop between them without realizing it, because that leads to confusion. The mathematical definition isn't too hard, the definition I laid out isn't too hard, the definition you give isn't too hard, but the amount of confusion you can get from unknowingly switching between them is almost unbounded.
tshaddox 5y ago
Is your question similar to the question "there's a string type in almost any language, but does that include a string representation of the 100 states of the 100-state 2-symbol busy beaver winner?"

colanderman 5y ago

I think most languages (implicitly) define `->` to include all such functions, not just those which could be defined by the language itself. Otherwise it would not be possible to describe the type of builtin or foreign-language library functions, which often exist explicitly to circumvent language restrictions. Even constructive logic languages (e.g. Coq) adhere to this definition I believe, else it would be impossible to introduce axioms.

gowld 5y ago

Andrej Bauer is a great resource twitter.com/andrejbauer/status/1212737159217762304 http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/ http://math.andrej.com/2008/02/06/representations-of-uncompu... > constructive mathematics does not assume that all reals are computable or constructive. It is agnostic about which reals there are. Basically, in a computer, the "set of all reals" is irrelevant, only the set of computable reals matters. (And you can represent many reals without infinite sequenecs, even some exotic ones. You don't need "infinite precision rational approximation", you just need enough precision to disambiguate from all other reals in your program.)

jerf 5y ago

It can be helpful in the computer-science (as considered as studying real machines, not infinite machines) context to very explicitly consider types as literally what they will be in the computer's memory. For instance, an "int64" in languages that support that type is not "an integer" which may be of unbounded size. It is specifically 2*64 values, and no others. Things like strings can be imagined as a family of types, one for each size, or as a new sort of thing that can be variable length, but still has a strongly-characterizable upper limit. It is also valid to consider mathematical types, of course. My point here is not to confuse the two, though. You will make a big mess of things if you are switching back and forth between types that can be represented in real machines and math types without realizing it. Mathematical types turn out to be tricky ways of viewing real programs, because they're much simpler to work with [1] but will bite you when you least expect it if you're not careful when real machine limits affect you. [1]: One of the things that a lot of people find counterintuitive is why it's simpler to have things like "infinite tapes" and other infinities in the math. The reason is, in a real machine when you reach for another byte in RAM, you have two cases to consider: 1. it's there and 2. it's not. If you have "infinite" RAM, you only have one case. Trying to do real proofs on real machines is a this never ending proliferation of cases to worry about that the infinities make go away. Personally I think of almost every "infinite" that shows up in computer science as the English word "unbounded" instead. It's not that there's literally infinite cells, it's just, you'll never reach for another one and be told it's not there, but at any given point, consumption of whatever resource is finite.

colanderman 5y ago
Not quite literally, I would argue -- in almost all modern languages, `int64` doesn't mean just "all 64-bit bit patterns", it means more specifically: "a 64-bit bit pattern in a context in which the program text interprets as an integer value". I.e., although any given `float` bit pattern (member of the set GF(2)^64) is also an `int64` bit pattern (member of the same set), a value of type `float` is not a value of type `int64`. Alternatively -- the type `int64` is comprised of 2^64 discrete values, distinct from the 2^64 discrete values comprising `float`, which happen to have 64-bit representations which overlap.
- jerf 5y ago
  I would certainly call that another useful and valid perspective. Again, the real thing is to make sure you don't accidentally flipflop between them without realizing it, because that leads to confusion. The mathematical definition isn't too hard, the definition I laid out isn't too hard, the definition you give isn't too hard, but the amount of confusion you can get from unknowingly switching between them is almost unbounded.

tshaddox 5y ago

Is your question similar to the question "there's a string type in almost any language, but does that include a string representation of the 100 states of the 100-state 2-symbol busy beaver winner?"