[TYPES] Types-list post from devriese@cs.tcd.ie requires approval

[Stephanie Weirich]

Hi Edsko,

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

--Stephanie

>
> From: Edsko de Vries <devriese at cs.tcd.ie>
> Date: January 24, 2008 11:38:26 AM EST
> To: types-list at lists.seas.upenn.edu
> Subject: Isorecursive types and type abstraction
>
>
> (Originally sent to haskell-cafe; someone suggested posting it here)
>
> Hi,
>
> Most descriptions of recursive types state that iso-recursive types
> (with explicit 'fold' and 'unfold' operators) are easy to typecheck,
> and that equi-recursive types are much more difficult. My question
> regards using iso-recursive types (explicitly, not implicitly using
> algebraic data types) together with type abstraction and application.
>
> The usual typing rules for fold and unfold are
>
>          e :: Fix X. t
>   -----------------------------  Unfold
>   unfold e :: [X := Fix X. t] t
>
>       e :: [X := Fix X. t] t
>   ----------------------------- Fold
>        fold e : Fix X. t
>
> This works ok for the following type:
>
>   ListInt = Fix L. 1 + Int * L
>
> (where "1" is the unit type). If
>
>   x :: ListInt
>
> then
>
>   unfold x :: 1 + Int * ListInt
>
> using the Unfold typing rule. However, this breaks when using type
> abstraction and application. Consider the polymorphic version of list:
>
>   List = Fix L. /\A. 1 + A * L A
>
> Now if we have
>
>   x :: List Int
>
> we can no longer type
>
>   unfold x
>
> because x does not have type (Fix ..), but ((Fix ..) Int) instead. Of
> course, we can unroll List Int by first unrolling List, and then
> re-applying the unrolled type to Int to get
>
>   (/\A. 1 + A * (Fix L. /\A. 1 * L A) A) Int
>
> which can be simplified to
>
>   1 + Int * List Int
>
> but this is not usually mentioned (that I could find; in  
> particular, TAPL does not mention it) and I'm worried that there  
> are subtleties here that I'm missing--nor do I have an exact  
> definition of what this 'extended' unrolling rule should do.
>
> Any hints or pointers to relevant literature would be appreciated!
>
> Edsko
>
> PS. One way to simplify the problem is to redefine List as
>
>   List = /\A. Fix L. 1 + A * L
>
> so that List Int can easily be simplified to the right form (Fix ..);
> but that can only be done for regular datatypes. For example, the  
> nested
> type
>
>   Perfect = Fix L. /\A. A + Perfect (A, A)
>
> cannot be so rewritten because the argument to Perfect in the  
> recursive
> call is different.
>
>