
Ashley Yakeley wrote:
At 2001-01-30 23:11, Johan Nordlander wrote:
However, this whole idea gets forfeited if it's possible to look behind the abstraction barrier by pattern-matching on the representation.
Isn't this information-hiding more appropriately achieved by hiding the constructor?
-- data IntOrChar = MkInt Int | MkChar Char data Any = forall a. MkAny a --
Surely simply hiding MkInt, MkChar and MkAny prevents peeking?
This is the simple way of obtaining an abstract datatype that can have only one static implementation, and as such it can indeed be understood in terms of existential types. But if you want to define an abstract datatype that will allow several different implementations to be around at run-time, you'll need the full support of existential types in the language. But might also want to consider the analogy between your example, and a system which carries type information around at runtime. Indeed, labelled sums is a natural way of achieving a universe of values tagged with their type. The difference to real dynamic typing is of course that for labelled sums the set of possible choices is always closed, which is also what makes their implementation relatively simple (this still holds in O'Haskell, by the way, despite subtyping). Nevertheless, (by continuing the analogy with your proposal for type pattern-matching) you can think of type matching as as a system where the constructors can't be completely hidden, just become deassociated with any particular "existentially quantified" type. That is, MkInt and MkChar would still be allowed outside the scope of the abstract type IntOrChar, they just wouldn't be seen as constructors specifically associated with that type. Clearly that would severely limit the usefulness of the type abstraction feature. -- Johan