[Haskell-cafe] OT: Isorecursive types and type abstraction

[Antoine Latter]

Can "Fix" be made to work with higher-kinded types?  If so, would the
following work:

Perfect = /\ A . Fix (L :: * -> *) . (A + L (A,A))

Keep in mind I have no idea what the "Perfect" data structure is
supposed to look like.

-Antoine

On Jan 24, 2008 9:52 AM, Edsko de Vries <devriese at cs.tcd.ie> wrote:
> Hi,
>
> This is rather off-topic but the audience of this list may be the right
> one; if there is a more appropriate venue for this question, please let
> me know.
>
> 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.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>