Type Pattern-Matching for Existential Types

[Johan Nordlander]

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