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

[Dan Licata]

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 <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
> >
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>