Adam Megacz wrote:
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/
Actually, polymorphism is not implicit in System F, you have to use a
big Λ to bind type parameters. For instance, the identity function is
written
id :: ∀a.(a -> a)
id = Λa.λ(x::a).x
The first argument is the type and the second argument is the actual
argument.
With this in mind, it's clear that you can't write your example; it
would look like this:
hard :: ∀n.Maybe (f n) -> Maybe (∀n.f n)
hard f = case f n of -- n is not in scope
Nothing -> Nothing
Just x -> Just (Λn.x) -- n bound here
Of course, parametricity tells you that that the function f is actually
"constant" in a certain sense. But to my knowledge, there is no way to
make this knowledge internal to System F.
Best regards,
Heinrich Apfelmus
--
http://apfelmus.nfshost.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
