Type Pattern-Matching for Existential Types

Johan Nordlander nordland@cse.ogi.edu
Tue, 30 Jan 2001 23:11:19 -0800

Lennart Augustsson wrote:
> Ashley Yakeley wrote:
> > data Any = forall a. Any a
> >
> > get :: Any -> Maybe Char
> > get (Any (c::Char)) = Just c -- bad
> > get _ = Nothing
> > --
> >
> > ...but as it stands, this is not legal Haskell, according to Hugs:
> >
> > ERROR "test.hs" (line 4): Type error in application
> > *** Expression     : Any c
> > *** Term           : c
> > *** Type           : Char
> > *** Does not match : _0
> > *** Because        : cannot instantiate Skolem constant
> >
> > This, of course, is because the '::' syntax is for static typing. It
> > can't be used as a dynamic pattern-test.
> >
> > Question: how big of a change would it be to add this kind of pattern
> > matching? Is this a small issue, or does it have large and horrible
> > implications?
> It has large and horrible implications.  To do dynamic type tests you need
> to carry around the types at runtime.  This is not something that Haskell
> does (at least you don't have to).
>     -- Lennart

It can also be questioned from a software engineering standpoint.  Much
of the purpose with existential types is to provide information hiding;
that is, the user of an existentially quantified type is not supposed to
know its concrete representation.  The merits of an information hiding
dicipline is probably no news to anybody on this list.

However, this whole idea gets forfeited if it's possible to look behind
the abstraction barrier by pattern-matching on the representation. 
Allowing that is a little like saying "this document is secret, but if
you're able to guess its contents, I'll gladly confirm it to you!".  The
same argument also applies to information hiding achieved by coercing a
record to a supertype.

This doesn't mean that I can't see the benefit of dynamic type checking
for certain problems.  But it should be brought in mind that such a
feature is a separate issue, not to be confused with existential types
or subtyping.  And as Lennart says, it's a feature with large (and
horrible!) implications to the implementation of a language.

-- Johan