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