[Haskell-cafe] is Haskell missing a non-instantiating polymorphic case?
batterseapower at hotmail.com
Mon Oct 31 15:17:14 CET 2011
On 23 October 2011 06:48, Adam Megacz <megacz at cs.berkeley.edu> wrote:
> 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 wonder if you can write eta-expansion for a product type containing
an existential given your extension? If I have:
data Id a = Id a
I can currently write:
eta x = Id (case x of Id x -> x)
And I have that eta x != _|_ for all x. But if I have:
data Exists = forall a. Exists a
Then I can't write the equivalent eta-expansion:
eta x = Exists (case x of Exists x -> x)
The closest I can get is:
eta x = Exists (case x of Exists x -> unsafeCoerce x :: ())
I'm not sure if you can do this with your extension but it smells plausible.
More information about the Haskell-Cafe