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

[Adam Megacz]

On 2011-10-24 00:18:45 -0700, Heinrich Apfelmus said:
> Actually, polymorphism is not implicit in System F,

Of course; take a look at the explicit type-application {|t|} in the 
second link I posted.


On 2011-10-24 00:18:45 -0700, Heinrich Apfelmus said:
> 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
> 

I certainly agree that the program you've written won't work -- but 
unfortunately that's not the same thing as proving it can't be written!


> 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.

Indeed, this is precisely the sense in which I believe it is "missing".

Thanks for your comments!

  - a