2 ms·

It can be helpful in the computer-science (as considered as studying real machines, not infinite machines) context to very explicitly consider types as literall

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

by jerf 5y ago

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.