On 23 October 2011 06:48, Adam Megacz <meg...@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. Max _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe