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

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