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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
