Recursive definitions in type theory

Abstract

We offer a new account of recursive definitions for both types and partial functions. The computational requirements of the theory restrict recursive type definitions involving the total function-space constructor (→) to those with only positive occurrences of the defined typed. But we show that arbitrary recursive definitions with respect to the partial function-space constructor are sensible. The partial function-space constructor allows us to express reflexive types of Scott's domain theory (as needed to model the lambda calculus) and thereby reconcile parts of domain theory with constructive type theory.