[Haskell-cafe] is Haskell missing a non-instantiating polymorphic case?
Heinrich Apfelmus
apfelmus at quantentunnel.de
Mon Oct 24 09:18:45 CEST 2011
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
More information about the Haskell-Cafe
mailing list