[Haskell-cafe] Re: Existentials and type var escaping
Benjamin.Rudiak-Gould at cl.cam.ac.uk
Mon Jun 11 20:37:37 EDT 2007
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,
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.
More information about the Haskell-Cafe