[Haskell-cafe] Existential quantification problem
Brandon S. Allbery KF8NH
allbery at ece.cmu.edu
Sun Jul 13 21:03:04 EDT 2008
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
>>>> 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
>>> expression. (It can't `escape'). This is required for decidable
>>> 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
More information about the Haskell-Cafe