Report Number: CS-TN-95-18
Institution: Stanford University, Department of Computer Science
Title: Effective models of polymorphism, subtyping and recursion
Author: Mitchell, John
Author: Viswanathan, Ramesh
Date: March 1995
Abstract: We develop 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 Godel numbers for computable functions. This is consistent with trends away from natural numbers in the field of abstract recursion theory.
http://i.stanford.edu/pub/cstr/reports/cs/tn/95/18/CS-TN-95-18.pdf