On Thu, Jan 24, 2008 at 10:06:04AM -0600, Antoine Latter wrote:

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

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

Hi, Thanks for your quick reply. Unfortunately, your solution does not work. For Fix X. t to be well-defined, we must have that if 'X' has kind 'k', then 't' must also have kind 'k' (compare the type of 'fix' in Haskell: (a -> a) -> a).

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

The Haskell equivalent would be data Perfect a = Leaf a | Branch (Perfect (a, a)) and models perfect binary trees (I admit, slightly headwrecking datatype! :) Edsko

On Thu, Jan 24, 2008 at 10:46:36AM -0600, Antoine Latter wrote:

Hmm ...

How about:

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

unfold Perfect = [L := Fix L . t] t where t = /\ A . (A + L (A,A)) = /\ A . (A + (Fix L . /\ B . (B + L (B,B))) (A,A))

assuming alpha-equality. Because L and (Fix L . t) are of kind (* -> *), the substitution should be okay. Am I missing something, again?

The problem is not that Perfect as it stands cannot be unrolled; the problem is that without some hackery, I don't know how to unroll the type of a term if that type is of the form ((Fix ..) applied to some arguments rather than just (Fix ..) -- whether that is List or Perfect. The only reason I mention Perfect is that for List I can 'lift' the "/\A" over the "Fix", but I cannot do that with Perfect. Edsko

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