[Haskell-cafe] OT: Isorecursive types and type abstraction
drl at cs.cmu.edu
Thu Jan 24 11:49:25 EST 2008
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.]
Flexible Type Analysis
Karl Crary and Stephanie Weirich
for an example of a type theory with this type.
> 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
More information about the Haskell-Cafe