[TYPES] Isorecursive types and type abstraction

[Stephanie Weirich]

Hi Edsko,

Yes, you can write perfect as
    /\A:*.  rec (/\P. a + P (A, A), A)

(and your original version of list as:
    List = /\A:*.  rec (/\L. 1 + (A, L A), A)
)

The reason that it is complicated is that the rec operator is creating
a recursive type with a higher kind (i.e. a type constructor of kind  
*->*)
but fold and unfold need to work with expressions that are classified by
types (with kind *). Therefore, the second argument to rec is a
parameter to the type constructor that turns it into a type.

We can simplify the rules in the paper a bit by uncurrying the  
arguments to rec:

G |- c1 : (k -> *) -> k -> *   G |- c2 : k
---------------------------------------------
G |- rec c1 c2 : *

with the typing rule for fold (unfold is the reverse):

  G |- e : c1 (rec c1) c2
--------------------------------
  G |- fold x : rec c1 c2

And if you specialize the above rule to List Int  (i.e. c1 = List  
above, c2 = Int),
you get:

  G |- x : 1 + (Int, List Int)
-----------------------------
  G |-  fold x : List Int

---Stephanie


On Jan 24, 2008, at 1:05 PM, Edsko de Vries wrote:

> Hi Stephanie,
>
>> What you need is a higher-kinded version of Fix (parameterized
>> recursive type), with the associated fold and unfold rules. You can
>> find these rules in the paper:
>>
>>    Flexible Type Analysis, Karl Crary and Stephanie Weirich, ICFP 99
>>
>>    http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.pdf
>
> Thank you for your answer. The paper looks interesting and I will  
> study
> it. Do I understand correctly that it will give me a fix operator that
> allows me to rewrite Perfect and lift the /\A over the Fix operator,
> just like for List?
>
> In a way though that circumvents the problem I'm having rather than
> solving it. That is ok, but it does mean having to introduce a more
> complicated Fix operator, and it seems to me that there should be
> simpler solution. But perhaps there isn't.
>
> Either, I appreciate the pointer. Thanks!
>
> Edsko