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

Adam Megacz megacz at cs.berkeley.edu
Sun Oct 30 01:33:10 CEST 2011

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

More information about the Haskell-Cafe mailing list