[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 

     id :: ∀a.(a -> a)
     id = Λa.λ(x::a).x

The first argument is the type and the second argument is the actual 

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


More information about the Haskell-Cafe mailing list