Predicative type theories are powerful tools for giving foundational interpretations of programming languages. Due to their explicit inductive construction, predicative type theories have multiple mathematical models that provide precise definitions of programming language features. However, not all features have predicative interpretations, and current interpretations of objects rely on impredicative type theories, such as Girard's System F, because of the difficulty in specifying a type for objects in the presence of self-application. In this paper we show that objects have a predicative interpretation.
We show that predicativity is associated with method monotonicity, and that binary methods prevent the inductive type construction. Our interpretation differs from impredicative accounts by replacing the use of recursive types for objects with conditions for method polymorphism over the self type. We further give a propositional meaning to objects in the type theory, providing a calculus for formal verification. Our interpretation has been verified in the Nuprl predicative type theory.
This paper provides (I think) a very cool mathematical interpretation of objects as records of polymorphic functions, where I give the argument that the actual types should not be determined statically. The soundness of the interpetation can be proved, but to be useful, we need to be able to find programs having type T, where T = T -> T and the function space is partial. Such programs exist (like the function that runs forever on any argument), but the argument is non-trivial, and I've put this paper on hold while I figure out the details. In the meantime, the paper is unpublished, but the contents are accurate up to the proof theoretic argument.