[Haskell-cafe] Re: Existentials and type var escaping

[Ben Rudiak-Gould]

Roberto Zunino wrote:
> foo, as defined above does not work (lazy patterns not allowed), and in
> 
> foo y = E (case y of E x -> x)
> 
> a variable escapes. I also tried with CPS with no success.
> 
> Is foo definable at all? I'm starting to think that it is not, and that
> there must be a very good reason for that...

It's not definable, and there is a good reason. Existential boxes in 
principle contain an extra field storing their hidden type, and the type 
language is strongly normalizing. If you make the type argument explicit, 
you have

   foo (E <t> x) = E <t> x
   foo _|_ = E ??? _|_

The ??? can't be a divergent type term, because there aren't any; it must be 
a type, but no suitable type is available (foo has no type argument). You 
can't even use some default dummy type like (), even though _|_ does have 
that type, because you'd have to solve the halting problem to tell when it's 
safe to default.

I'm less clear on how important it is that type terms don't diverge. I think 
it may be possible to write cast :: a -> b if this restriction is removed, 
but I don't actually know how to do it.

-- Ben