[TYPES] Isorecursive types and type abstraction

[Derek Dreyer]

Edsko,

To follow up on what Karl said, if you want to see a formalization of
a language with iso-recursive type constructors at higher kind (i.e.
of kind K, where K is not restricted to be of the form K' -> Type but
may include arbitrary arrows and also product kinds), you could take a
look at chapter 6 of my PhD thesis:

http://tti-c.org/dreyer/thesis/main.pdf

I wouldn't claim that the formalization of iso-recursive higher-kinded
constructors here is original, but there is an aspect of the
meta-theory studied here that *is* original (see below).  In any case,
it more or less follows along the lines that Karl suggested.  In
particular, you have an iso-recursive type constructor

Mu alpha:K. A,

which has kind K as long as A has kind K under the assumption that
alpha does.  Equivalence of these mu-constructors is purely structural
(no "equi-recursive" unfolding at the type level).  Then, a recursive
"type" (i.e. of kind Type) just takes the form

E{Mu alpha:K.A},

where E is an elimination (a sequence of projections and applications)
applied to a Mu-constructor, resulting in a type of kind Type.  In the
case that K = Type itself, E is the empty path.  If K = K' -> K'' ->
Type, then E is a sequence of two applications (to constructors of
kinds K' and K''), etc.  And then the "fold" and "unfold" coercions at
this recursive type just coerce between E{Mu alpha:K.A} and E{A[Mu
alpha:K.A/alpha]}, which in the chapter are written "Q" and
"expand(Q)", respectively.

What I've described above is a pretty straightforward extension to F-omega.

However, in my thesis, I also considered iso-recursive higher-kinded
constructors as an extension to a language with dependent and
*singleton* kinds a la Stone and Harper.  (This combination arose
quite naturally in modeling the type theory of a recursive module
system.)  Such an extension turns out to be surprisingly tricky,
essentially because, when singleton kinds appear to the left of an
arrow in the kind of a Mu-constructor, the unfolding of a recursive
type rooted at that constructor is not always well-kinded.  (See
Section 6.2 for an example.)  In that chapter, I showed that you could
work around this by "monster-barring" such examples (which was not
obvious how to do), but I was never totally satisfied with that
solution.

Derek

On 1/24/08, Edsko de Vries <devriese at cs.tcd.ie> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> (Originally sent to haskell-cafe; someone suggested posting it here)
>
> Hi,
>
> 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.
>