Recursive types in polymorphic lambda calculus

• To: types@cis.upenn.edu, categories@mta.ca
• Subject: Recursive types in polymorphic lambda calculus
• From: Philip Wadler <wadler@research.bell-labs.com>
• Date: Fri, 14 May 1999 15:24:32 -0400

There is a fairly standard encoding of recursive types
into polymorphic lambda calculus, given by

	rec X.F[X]  =  all X.(F[X] -> X) -> X

where F[X] is a type in which the type variable X appears only
covariantly.  Recall that every covariant type corresponds to a
covariant functor, so for every h:X->Y we have F[h]:F[X]->F[Y].
If we abbreviate T = rec X.F[X], then the key functions on this
type are given by the polymorphic lambda terms:

	fold : all X.(F[X] -> X) -> T -> X
	fold = Lam X.lam k:F[X]->X.lam t:T.t{X}(k)

	in   : F[T] -> T
	in   = lam u:F[T].Lam X.lam k:F[X]->X.k(F[fold{X}(k)](u))

	out  : T -> F[T]
	out  = fold{F[T]}(F[in])

Questions: Who first had this insight?  Where is a good place to find
this spelled out in the literature?  Please send results to me, and I
will summarize them for the list.  Cheers, -- P

• Prev: WoLLIC'99 - Call for Participation
• Next: Type soundness issues in Java
• Index(es):
  • Main
  • Thread