Type inference with simple subtypes
- 1 July 1991
- journal article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 1 (3) , 245-285
- https://doi.org/10.1017/s0956796800000113
Abstract
Subtyping appears in a variety of programming languages, in the form of the ‘automatic coercion’ of integers to reals, Pascal subranges, and subtypes arising from class hierarchies in languages with inheritance. A general framework based on untyped lambda calculus provides a simple semantic model of subtyping and is used to demonstrate that an extension of Curry's type inference rules are semantically complete. An algorithm G for computing the most general typing associated with any given expression, and a restricted, optimized algorithm GA using only atomic subtyping hypotheses are developed. Both algorithms may be extended to insert type conversion functions at compile time or allow polymorphic function declarations as in ML.Keywords
This publication has 19 references indexed in Scilit:
- A theory of type polymorphism in programmingPublished by Elsevier ,2003
- Polymorphic type inference and containmentInformation and Computation, 1988
- A semantics of multiple inheritanceInformation and Computation, 1988
- The completeness theorem for typing λ-termsTheoretical Computer Science, 1983
- A filter lambda model and the completeness of type assignmentThe Journal of Symbolic Logic, 1983
- On the semantics of polymorphismActa Informatica, 1983
- Polymorphic type inferencePublished by Association for Computing Machinery (ACM) ,1983
- What is a model of the lambda calculus?Information and Control, 1982
- Data Types as LatticesSIAM Journal on Computing, 1976
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965