Document Type
Report
Date
1982
Keywords
retract model
Language
English
Disciplines
Computer Sciences
Description/Abstract
There has been great interest in recent years in designing programming languages which permit functions which may accept types as parameters (polymorphic functions) and types with type parameters (type generators). Unfortunately the semantics of such functions and types has not been as well understood as their practical use in software design. In [McCracken 1979], a denotational semantics was given for a simple programming language with these features. The semantics used closures, which are a special case of the more familiar retractions, over the Scott universal domain, Pw to represent types. It was then possible to interpret polymorphic functions as continuous functions from types to objects in Pw and the type generators as continuous functions from types to types. However, the model depends heavily on the fact that Pw and the types over it are all complete lattices, while in many cases it seems that the less restrictive complete partial orders are more natural for programming language semantics. An attempt to construct a model using retracts over complete lattices was made in [Donahue 1979], but it has been shown that the construction is not valid [McCracken 1980]. Structures that may solve this problem have been suggested by Scott [Scott 1980]. In this paper, we use Scott’s suggestion of finitary retracts over a finitary complete partial order. We show that Scott’s conjecture that these structures will provide a model for the polymorphic functions is true. In addition, we show that this also provides a model for the type generators and that recursive types can be interpreted in the model. In this paper we first define a prototype language as a typed λ-calculus extended with polymorphic functions and type generators. Next we present the finitary cpo‘s and the various functions and operators necessary in the semantics. And finally, we show how to use the cpo’s to give a model for the language.
Recommended Citation
McCracken, Nancy, "A finitary retract model for the polymorphic lambda-calculus" (1982). Electrical Engineering and Computer Science - Technical Reports. 1.
https://surface.syr.edu/eecs_techreports/1
Source
lo
