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
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