[Haskell-cafe] Existential quantification problem

[Jonathan Cast]

On Sun, 2008-07-13 at 21:03 -0400, Brandon S. Allbery KF8NH wrote:
> On 2008 Jul 13, at 19:50, Jonathan Cast wrote:
> 
> > On Sun, 2008-07-13 at 18:28 -0500, Derek Elkins wrote:
> >> On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
> >>> On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva  
> >>> wrote:
> >>>> Hello,
> >>>>
> >>>> how do I unbox a existential quantificated data type?
> >>>
> >>> You can't.  You have to use case analysis:
> >>>
> >>>  case foo of
> >>>    L l -> <whatever you wanted to do>
> >>>
> >>> where none of the information your case analysis discovers about the
> >>> actual type of l can be made available outside of the scope of the  
> >>> case
> >>> expression.  (It can't `escape').  This is required for decidable  
> >>> static
> >>> typing, IIRC.
> >>
> >> It's not an extraneous requirement; it is part of the definition of
> >> existential types.
> >
> > I know that.  I didn't know implementing existential types was an  
> > end in itself, though.
> 
> No?  Consider ST.  Anytime you need to completely restrict access to  
> the innards of a datum, existential types are your friend.

Right.  Mea culpa.

jcc