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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
