[Prev][Next][Index][Thread]
Recursive types in polymorphic lambda calculus
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