The title might be a bit more provocative than necessary.
I'm starting to suspect that there are very useful aspects of the
parametricity of System F(C) which can't be taken advantage of by
Haskell in its current state. To put it briefly, case-matching on a
value of type (forall n . T n) forces one to instantiate the "n", even
though the branch taken within the case cannot depend on "n"
(parametricity).
I came up with the simplest example I could and posted it to
StackOverflow, but there haven't been any successes (despite some
excellent attempts!):
http://stackoverflow.com/questions/7720108/
This might sound like an obscure problem, but it actually starts to get
in the way of the very useful Washburn+Weirich "Boxes Go Bananas" and
related PHOAS representation. I've written up a short example of the
problems that happen here:
The link above also includes a very rough sketch of a proposal for a
"pcase" construct that doesn't instantiate its argument.
Is it possible to do what I'm attempting without adding "pcase" to the
language? Would "pcase" break the soundness of the type system (I
don't think so) or complicate type inference (probably)?
I'd be interested in any comments/thoughts/help people can offer.
Thanks!
- a
PS, I suspect that this is somehow related to the issue that Guillemette and
Monnier mention in section 5.1 of their paper on type-preserving closure
conversion, although I wasn't able to find the code online in order to be
sure.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
