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