Type Theory and Recursion Extended Abstract
Gordon D. Plotkin · ERA · 2003
At first sight, type theory and recursion are compatible: there are many models of the typed lambda calculus with a recursion operator at all types. However the situation changes as soon as one considers sums. By a theorem of Huwig and Poign´e, any cartesian closed category with binary sums and such a general recursion operator is trivial. Domain theory provides the category of cpos and continuous functions. It is cartesian closed and has a general recursion operator — the least fixed-point operator. It (necessarily) does not have binary sums, but the closely associated category of cpos and strict continuous functions does. has derivable in System F finite products and sums, second-order existential quantification and initial and final algebras (of definable covariant functors). It is both interesting — and necessary for the development of the semantics of programming languages — to consider the interaction of polymorphism and recursion. However as the parametric models have categorical sums, a now familiar difficulty arises. We consider instead a second-order intuitionistic linear type theory whose primitive type constructions are linear and intuitionistic function types and second-order quantification.