Inductive, Projective, and Retractive Types

We give an analysis of classes of recursive types by presenting two extensions of the simply-typed lambda calculus. The first language only allows recursive types with built-in principles of well-founded induction, while the second allows more general recursive types which permit non-terminating computations. We discuss the expressive power of the languages, examine the properties of reduction-based operational semantics for them, and give examples of their use in expressing iteration over large ordinals and in simulating both call-by-name and call-by-value versions of the untyped lambda calculus. The motivations for this work come from category theoretic models.