[Haskell-cafe] Existentials and type var escaping

[Isaac Dupree]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

David House wrote:
> On 31/05/07, Isaac Dupree <isaacdupree at charter.net> wrote:
>> foo undefined = undefined
> 
> That's not true. When you evaluate foo undefined, it matches the first
> (irrefutable) pattern immediately, without any deconstruction of the
> undefined argument (which is the entire point of it being a lazy
> pattern). So it becomes the right hand side, C <thunk>. Only when you
> force that <thunk> would you have to force the undefined argument, so
> foo undefined = C undefined:
> 
> *Main> foo undefined
> C *** Exception: Prelude.undefined
> 

Oh, I misinterpreted "must be non bottom" to be talking about becoming
more strict, not less, compared to id, and then misanalysed the function :/

Now for the existential case... normally an existential "escaping" is
useless, sometimes it seems to make sense.  Looking at the GHC manual
http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#existential-quantification
I think this is the relevant explanatory paragraph:

In general, you can only pattern-match on an existentially-quantified
constructor in a case expression or in the patterns of a function
definition. The reason for this restriction is really an implementation
one. Type-checking binding groups is already a nightmare without
existentials complicating the picture. Also an existential pattern
binding at the top level of a module doesn't make sense, because it's
not clear how to prevent the existentially-quantified type "escaping".
So for now, there's a simple-to-state restriction. We'll see how
annoying it is.


It seems like an existential as returned by (case y of E x -> x) is
("should" be) just "anything" -- you can put it in an existential
container, or you can "seq" it, but not much else. To seq, (case y of E
x -> (x `seq`)) should work, so the difficulty is in transferring an
existential from one place to another with weird strictness effects...
Is (data E' = forall a . E' !a) allowed?  I seem to remember some
discussion about its oddness...  Type-class contexts on the existentials
make it more complicated.


Isaac
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFGYHDzHgcxvIWYTTURAn9oAJ45VLiD6W63ByUOrfpRILprPyKGdACbB+nu
YIULFXH4KHDcbNmG/+cb5vI=
=v2Co
-----END PGP SIGNATURE-----