is Haskell missing a non-instantiating polymorphic case?
The title might be a bit more provocative than necessary. 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/ This might sound like an obscure problem, but it actually starts to get in the way of the very useful Washburn+Weirich "Boxes Go Bananas" and related PHOAS representation. I've written up a short example of the problems that happen here: The link above also includes a very rough sketch of a proposal for a "pcase" construct that doesn't instantiate its argument. Is it possible to do what I'm attempting without adding "pcase" to the language? Would "pcase" break the soundness of the type system (I don't think so) or complicate type inference (probably)? I'd be interested in any comments/thoughts/help people can offer. Thanks! - a PS, I suspect that this is somehow related to the issue that Guillemette and Monnier mention in section 5.1 of their paper on type-preserving closure conversion, although I wasn't able to find the code online in order to be sure.
Hrm, it seems that I hit "send" instead of "save draft" when shutting down my computer last night. On 2011-10-22 22:48:55 -0700, Adam Megacz said:
I've written up a short example of the problems that happen here:
Here is the link which was missing from that posting: http://www.megacz.com/thoughts/polymorphic-case.html
From: Adam Megacz
Hrm, it seems that I hit "send" instead of "save draft" when shutting down my computer last night.
On 2011-10-22 22:48:55 -0700, Adam Megacz said:
I've written up a short example of the problems that happen here:
Here is the link which was missing from that posting:
It seems that StackOverflow post left out important details. I think I've solved that one, but the problem there looks harder. It sounds like the entire point of this is syntax representation? If so, have you seen Conor McBride's recent post http://www.e-pig.org/epilogue/?p=773 on troubles they ran into with a higher order term representation, and a way to write first-order free name/bound index terms with a syntax like la $ \f -> la $ \x -> f (f x) Brandon
On 2011-10-23 17:02:47 -0700, Brandon Moore said:
It sounds like the entire point of this is syntax representation?
Not really...... the entire point of this is parametricity. :) There are a lot of examples involving syntax and binding because ruling out exotic terms is one of the things that parametricity is really useful for.
If so, have you seen Conor McBride's recent post http://www.e-pig.org/epilogue/?p=773
Yes, a while back; it's very cool but basically orthogonal: the data types in that blog post aren't indexed by the object-language-term's type (nor should they be -- he's writing a typechecker, after all!). - a
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!):
Actually, polymorphism is not implicit in System F, you have to use a big Λ to bind type parameters. For instance, the identity function is written id :: ∀a.(a -> a) id = Λa.λ(x::a).x The first argument is the type and the second argument is the actual argument. 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 -- http://apfelmus.nfshost.com
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
On 23 October 2011 06:48, Adam Megacz
The title might be a bit more provocative than necessary.
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 wonder if you can write eta-expansion for a product type containing an existential given your extension? If I have: data Id a = Id a I can currently write: eta x = Id (case x of Id x -> x) And I have that eta x != _|_ for all x. But if I have: data Exists = forall a. Exists a Then I can't write the equivalent eta-expansion: eta x = Exists (case x of Exists x -> x) The closest I can get is: eta x = Exists (case x of Exists x -> unsafeCoerce x :: ()) I'm not sure if you can do this with your extension but it smells plausible. Max
participants (4)
-
Adam Megacz -
Brandon Moore -
Heinrich Apfelmus -
Max Bolingbroke