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 <[EMAIL PROTECTED]> 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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe