4 ms·

Although if you just consider 1-1 correspondence, then basically any type with a countable number of inhabitants is isomorphic to the integers (when the type is

Although if you just consider 1-1 correspondence, then basically any type with a countable number of inhabitants is isomorphic to the integers (when the type is viewed as a set of inhabitants). And that makes sense, because we can always just take the binary representation of any data type in memory. And if you just have unit type, empty type, sums and products, then you can only make types with finitely many inhabitants. Adding the integers to that makes you able to make any countable type, but potentially in a trivial way as described above. Therefore just viewing the types as sets does not give a very satisfactory basis for determining whether a type is an "algebraic data type". Maybe we could do better if we consider some more aspects related to type safety, but it's not immediately obvious to me how.

gmfawcett 5y ago
"Any type with a countable number of inhabitants is isomorphic to the integers" --> I assume you mean "countable" in the sense of "countably infinite." Clearly the finite types can't be put into correspondence with the integers. I agree that viewing the types just in terms of their cardinality isn't terribly insightful. But I do think it's helpful to realize that arrays aren't some other kind of thing that's separate from ADTs, and that you can bring the same algebraic reasoning tools to bear on arrays (and other pedestrian data types).
- Hercuros 5y ago
  My point was basically that you can implement the array abstract data type (creation, set value at index, get value at index) in a lot of ways, including by using ADTs (although it seems hard to get an O(1) implementation if you use ADTs, unless you have some clever compiler or language mechanism). But just because you can implement arrays in terms of ADTs doesn't mean that arrays ARE ADTs. Now that I think of it a bit more, it seems to be a category error to say that a "set" or an "object" or a "dictionary" is an algebraic data type. Algebraic data types are types (values) constructed out of simpler types (values) in a certain way, and that can be deconstructed in a way that mirrors the way they were created. You can implement various APIs/interfaces on top of that, including dictionaries and sets and whatnot. But my point was that you can do the same on top of just integers (assuming you have the common integer operations), and you could even package it up in a type safe way so that the fact that you used integers in the implementation does not leak out, assuming the language has some modularity/abstraction mechanism so that you can make stuff private to a module. But based on this it seems to be a stretch to say that dictionaries are REALLY just integers or bitstrings. And just like you probably wouldn't want to bring "integer reasoning" to bear on dictionaries, you probably don't want to use ADT reasoning to reason about dictionaries either. Because then you are really reasoning about the concrete implementation details and generally speaking those details are hidden from clients of the dictionary (and subject to change at any time).
  - gmfawcett 5y ago
    I think I see where you're going, and it seems completely reasonable to me. :) I like the distinction you've drawn between implementation and interface in your dictionary and abstract-array examples. I don't think that abstract interfaces make algebraic reasoning completely impossible, e.g., you could represent unknown implementation details as variables (or even functions). But it's good to be clear re: what questions you're asking, the level of abstraction you're thinking at, and whether any analogy to ADTs is useful or simply a distraction. I think a nice corollary to your second point is that the existence of an isomorphism between two collections doesn't mean they are the same thing. This is easy to see when you discuss integer reasoning. E.g., if we have a infinitely countable data type, so we have an isomorphism to Z. But that doesn't automatically make our data type a ring (not in any meaningful sense).

gmfawcett 5y ago

"Any type with a countable number of inhabitants is isomorphic to the integers" --> I assume you mean "countable" in the sense of "countably infinite." Clearly the finite types can't be put into correspondence with the integers. I agree that viewing the types just in terms of their cardinality isn't terribly insightful. But I do think it's helpful to realize that arrays aren't some other kind of thing that's separate from ADTs, and that you can bring the same algebraic reasoning tools to bear on arrays (and other pedestrian data types).

Hercuros 5y ago
My point was basically that you can implement the array abstract data type (creation, set value at index, get value at index) in a lot of ways, including by using ADTs (although it seems hard to get an O(1) implementation if you use ADTs, unless you have some clever compiler or language mechanism). But just because you can implement arrays in terms of ADTs doesn't mean that arrays ARE ADTs. Now that I think of it a bit more, it seems to be a category error to say that a "set" or an "object" or a "dictionary" is an algebraic data type. Algebraic data types are types (values) constructed out of simpler types (values) in a certain way, and that can be deconstructed in a way that mirrors the way they were created. You can implement various APIs/interfaces on top of that, including dictionaries and sets and whatnot. But my point was that you can do the same on top of just integers (assuming you have the common integer operations), and you could even package it up in a type safe way so that the fact that you used integers in the implementation does not leak out, assuming the language has some modularity/abstraction mechanism so that you can make stuff private to a module. But based on this it seems to be a stretch to say that dictionaries are REALLY just integers or bitstrings. And just like you probably wouldn't want to bring "integer reasoning" to bear on dictionaries, you probably don't want to use ADT reasoning to reason about dictionaries either. Because then you are really reasoning about the concrete implementation details and generally speaking those details are hidden from clients of the dictionary (and subject to change at any time).
- gmfawcett 5y ago
  I think I see where you're going, and it seems completely reasonable to me. :) I like the distinction you've drawn between implementation and interface in your dictionary and abstract-array examples. I don't think that abstract interfaces make algebraic reasoning completely impossible, e.g., you could represent unknown implementation details as variables (or even functions). But it's good to be clear re: what questions you're asking, the level of abstraction you're thinking at, and whether any analogy to ADTs is useful or simply a distraction. I think a nice corollary to your second point is that the existence of an isomorphism between two collections doesn't mean they are the same thing. This is easy to see when you discuss integer reasoning. E.g., if we have a infinitely countable data type, so we have an isomorphism to Z. But that doesn't automatically make our data type a ring (not in any meaningful sense).