[Haskell-cafe] is Haskell missing a non-instantiating polymorphic case?

[Heinrich Apfelmus]

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