[Haskell-cafe] OT: Isorecursive types and type abstraction
Edsko de Vries
devriese at cs.tcd.ie
Thu Jan 24 10:52:59 EST 2008
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.
More information about the Haskell-Cafe
mailing list