On 23 October 2011 06:48, Adam Megacz meg...@cs.berkeley.edu 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
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
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
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:
From: Adam Megacz meg...@cs.berkeley.edu
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
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
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)
