On Jan24, Antoine Latter wrote: > Can "Fix" be made to work with higher-kinded types? If so, would the > following work:
Yes, it can. For a particular A (e.g., Int), List A is a recursive type Fix X. 1 + (A * X). List :: type -> type is a family of recursive types: if you give it a type, it gives you a recursive type. So we can represent that by \ a -> Fix X. 1 + (a * X). [As an aside, note that (\ a -> A) is the type-constructor-level abstraction (i.e., the introduction form for the *kind* K1 -> K2). This is different from the polymorhpic type (\forall a.A), which has kind type, and is introduced and eliminated by *term*-level type abstraction and application. So I'd say that list itself is parametrized, not polymorphic. On the other hand, cons :: \forall a . a -> list a -> list a is a polymorphic function that instantiates the parametrized type list with its type parameter.] Now, as Edsko observed, families of recursive types aren't good enough for non-uniform datatypes like perfect trees, lists indexed by their length, etc. One ingredient that GADTs give you is *recursive families of types*. In contrast to families of recursive types, recursive families are a simultaneous recursive definition of all of the elements of the family; this is important because it permits one instance of the family to be defined in terms of another. In syntax, you get a new type Fix (C1, C2) where C1 :: (type -> type) -> (type -> type) and C2 :: type The idea is that this takes the fixed point of C1 and applies it to C2. The roll and unroll do what you suggest below. [This can be generalized to the fixed point of a constructor-level function of kind (K -> type) -> K -> type as well, and then C2::K. I.e., there's no reason the argument has to be a type.] See Flexible Type Analysis Karl Crary and Stephanie Weirich ICFP 99 for an example of a type theory with this type. Make sense? -Dan > 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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe