Effective Models of Polymorphism, Subtyping and Recursion
(extended abstract)

John Mitchell, Department of Computer Science, Stanford University, Stanford, CA 94305.
(Supported in part by NSF Grant CCR-9303099 and a grant from the TRW Foundation.

Ramesh Viswanathan, Bell Laboratories, 101 Crawfords Corner Road, Holmdel, NJ 07733. rv@research.att.com
(Supported by NSF Grant CCR-9303099.)

Abstract

We explore a class of models of polymorphism, subtyping and recursion based on a combination of traditional recursion theory and simple domain theory. A significant property of our primary model is that types are coded by natural numbers using any index of their supremum operator. This leads to a distinctive view of polymorphic functions that has many of the usual parametricity properties. It also gives a distinctive but entirely coherent interpretation of subtyping. An alternate construction points out some peculiarities of computability theory based on natural number codings. Specifically, the polymorphic fixed point is computable by a single algorithm at all types when we construct the model over untyped call-by-value lambda terms, but not when we use G\"odel numbers for computable functions. This is consistent with trends away from natural numbers in the field of abstract recursion theory. Although our development and analysis of each structure is completely elementary, both structures may be obtained as the result of interpreting standard domain constructions in effective models of constructive logic.