|
 ABSTRACT
A simple semantic model of automatic coercion is proposed. This model is used to explain four rules for inferring polymorphic types and providing automatic coercions between types. With the addition of a fifth rule, the rules become semantically complete but the set of types associated with an expression may be undecidable. An efficient type checking algorithm based on the first four rules is presented. The algorithm is guaranteed to find a type whenever a type can be deduced using the four inference rules. The type checking algorithm may be modified so that calls to type conversion functions are inserted at compile time.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
Barendregt, H.P, The Lambda Calculus: Its Syntax and Semantics. North Holland, 1981.
|
| |
2
|
Barendregt, H., Coppo, M. and Dezani-Ciancaglini, M. A Filter Lambda Model and the Completeness of Type Assignment. J. Symbolic Logic (198?). to appear.
|
| |
3
|
Curry, H.B and Feys, R. Combinatory Logic I. North-Holland, 1958.
|
 |
4
|
|
| |
5
|
|
| |
6
|
Gordon, M.J., R. Milner and C.P. Wadsworth. Lecture Notes in Computer Science. Vol. 78: Edinburgh LCF. Springer-Verlag, 1979.
|
| |
7
|
Hindley. R. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. AMS 146 (1969). pp 29-60.
|
| |
8
|
Hindley. R. The Completeness Theorem for Typing Lambda Terms. Theor. Comp. Sci. 22 (1983). pp 1-17.
|
| |
9
|
Hindley, R. Curry's Type Rules Are Complete with Respect to the F-Semantics Too. Theor. Comp. Sci. 22(1983). pp 127-133.
|
| |
10
|
|
| |
11
|
MacQueen, D. Private Communication. 1983.
|
| |
12
|
Meyer, A.R. What Is A Model of the Lambda Calculus?. Information and Control 52, 1 (1982). pp 87-122.
|
| |
13
|
Milner. R. A Theory of Type Polymorphism in Programming. JCSS 17 (1978). pp 348-375.
|
| |
14
|
|
| |
15
|
Paterson, M.S. and Wegman, M.N. Linear Unification. JCSS 16 (1978). pp 158-167.
|
| |
16
|
|
| |
17
|
|
| |
18
|
|
| |
19
|
Scott, D. Data Types as Lattices. Siam J. Comput. 5, 3 (1976). pp 522-587.
|
CITED BY 52
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
David N. Turner , Philip Wadler , Christian Mossin, Once upon a type, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.1-11, June 26-28, 1995, La Jolla, California, United States
|
|
|
John Mitchell , Sigurd Meldal , Neel Madhav, An extension of standard ML modules with subtyping and inheritance, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.270-278, January 21-23, 1991, Orlando, Florida, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States
|
|
|
Peter Canning , William Cook , Walter Hill , Walter Olthoff , John C. Mitchell, F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.273-280, September 11-13, 1989, Imperial College, London, United Kingdom
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Martin Sulzmann , Manuel M. T. Chakravarty , Simon Peyton Jones , Kevin Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
I.2