Type Pattern-Matching for Existential Types

Fergus Henderson fjh@cs.mu.oz.au
Wed, 31 Jan 2001 19:48:45 +1100


On 30-Jan-2001, Johan Nordlander <nordland@cse.ogi.edu> wrote:
> 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. 

That's a good argument for dynamic type casts not being available by
default.  However, there are certainly times when the designer of an
interface wants some degree of abstraction, but does not want to
prohibit dynamic type class casts.  The language should permit the
designer to express that intention, e.g. using the `Typeable' type
class constraint.

> 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!".

Yes.  But there are times when something like that is indeed what you
want to say.  The language should permit you to say it.

The specific language that you have chosen has some connotations
which imply that this would be undesirable.  But saying "this data
structure is abstract, but you are permitted to downcast it" is
really not a bad thing to say.  There's different levels of secrecy,
and not everything needs to be completely secret; for some things it's
much better to allow downcasting, so long as you are explicit about it.

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

OK, perhaps we are in agreement after all.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.