[Haskell-cafe] Existential quantification problem

[Brandon S. Allbery KF8NH]

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.

-- 
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH