TY - GEN

T1 - A simple semantics for ML polymorphism

AU - Ohori, Atsushi

N1 - Funding Information:
in part by grants NSF IRISG- and by OK1 Electric Industry
Publisher Copyright:
© 1989 ACM.

PY - 1989/11/1

Y1 - 1989/11/1

N2 - We give a framework for denotational semantics for the polymorphic "core" of the programming language ML. This framework requires no more semantic material than what is needed for modeling the simple type discipline. In our view, terms of ML are pairs consisting of a raw (untyped) lambda term and a type-scheme that ML's type inference system can derive for the raw term. We interpret a type-scheme as a set of simple types. Then, given any model M of the simply typed lambda calculus, the meaning of an ML term will be a set of pairs, each consisting of a simple type r and an element of M of type T. Hence, there is no need to interpret all raw terms, as was done in Milner's original semantic framework. In comparison to Mitchell and Harper's analysis, we avoid having to provide a very large type universe in which generic type-schemes are interpreted. Also, we show how to give meaning to ML terms rather than to derivations in the ML type inference system (which can be infinitely many for a single ML term). We give an axiomatization for the equational theory that corresponds to our semantic framework and prove the analogs of the completeness theorems that Friedman proved for the simply typed lambda calculus. The framework can be extended to languages with constants, type constructors and recursive types (via regular trees). For the extended language, we prove a theorem that allows the transfer of certain full abstraction results from languages based on the typed lambda calculus to ML-like languages.

AB - We give a framework for denotational semantics for the polymorphic "core" of the programming language ML. This framework requires no more semantic material than what is needed for modeling the simple type discipline. In our view, terms of ML are pairs consisting of a raw (untyped) lambda term and a type-scheme that ML's type inference system can derive for the raw term. We interpret a type-scheme as a set of simple types. Then, given any model M of the simply typed lambda calculus, the meaning of an ML term will be a set of pairs, each consisting of a simple type r and an element of M of type T. Hence, there is no need to interpret all raw terms, as was done in Milner's original semantic framework. In comparison to Mitchell and Harper's analysis, we avoid having to provide a very large type universe in which generic type-schemes are interpreted. Also, we show how to give meaning to ML terms rather than to derivations in the ML type inference system (which can be infinitely many for a single ML term). We give an axiomatization for the equational theory that corresponds to our semantic framework and prove the analogs of the completeness theorems that Friedman proved for the simply typed lambda calculus. The framework can be extended to languages with constants, type constructors and recursive types (via regular trees). For the extended language, we prove a theorem that allows the transfer of certain full abstraction results from languages based on the typed lambda calculus to ML-like languages.

UR - http://www.scopus.com/inward/record.url?scp=84976830729&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84976830729&partnerID=8YFLogxK

U2 - 10.1145/99370.99393

DO - 10.1145/99370.99393

M3 - Conference contribution

AN - SCOPUS:84976830729

T3 - Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture, FPCA 1989

SP - 281

EP - 292

BT - Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture, FPCA 1989

PB - Association for Computing Machinery, Inc

T2 - 4th International Conference on Functional Programming Languages and Computer Architecture, FPCA 1989

Y2 - 11 September 1989 through 13 September 1989

ER -