Type Pattern-Matching for Existential Types

[C.Reinke]

> > > data Any = forall a. Any a
> > >
> > > get :: Any -> Maybe Char
> > > get (Any (c::Char)) = Just c -- bad
> > > get _ = Nothing
..
> 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.

This discussion reminds me of an old paper by MacQueen:

  David MacQueen. Using dependent types to express modular structure.
  In Proc. 13th ACM SIGPLAN-SIGACT Symposium on Principles of
  Programming Languages, pages 277--286, January 1986.

He discusses some of the disadvantages of using plain existential
quantification for modular programming purposes and proposes an
alternative based on dependent sums, represented as pairing the witness
type with the expression in which it is used, instead of existentials,
where there is no witness for the existentially quantified type.

See CiteSeer for some of the follow-on work that references MacQueen's
paper:

  http://citeseer.nj.nec.com/context/32982/0

Some of that work tried to find a balance between having no witness
types and carrying witness types around at runtime. In this context,
Claudio Russo's work might be of interest, as he proposes to avoid the
problems of existentials without going into (value-)dependent types:

  http://www.dcs.ed.ac.uk/home/cvr/

Claus