is Haskell missing a non-instantiating polymorphic case?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

is Haskell missing a non-instantiating polymorphic case?

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



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is Haskell missing a non-instantiating polymorphic case? (missing link added)

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:

  http://www.megacz.com/thoughts/polymorphic-case.html



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is Haskell missing a non-instantiating polymorphic case? (missing link added)

Brandon Moore-2
> From: Adam Megacz <[hidden email]>

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

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is Haskell missing a non-instantiating polymorphic case? (missing link added)

Adam Megacz

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



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is Haskell missing a non-instantiating polymorphic case?

Heinrich Apfelmus
In reply to this post by Adam Megacz
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!):
>
> http://stackoverflow.com/questions/7720108/

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


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: is Haskell missing a non-instantiating polymorphic case?

Max Bolingbroke-2
In reply to this post by Adam Megacz
On 23 October 2011 06:48, Adam Megacz <[hidden email]> wrote:
> 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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe