article

Open access

PolyTOIL: A type-safe polymorphic object-oriented language

Authors:

Angela Schuett,

Robert van Gent,

Adrian FiechAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 25, Issue 2

Pages 225 - 290

https://doi.org/10.1145/641888.641891

Published: 01 March 2003 Publication History

Abstract

PolyTOIL is a new statically typed polymorphic object-oriented programming language that is provably typesafe. By separating the definitions of subtyping and inheritance, providing a name for the type of self, and carefully defining the type-checking rules, we have obtained a language that is very expressive while supporting modular type-checking of classes. The matching relation on types, which is related to F-bounded quantification, is used both in stating type-checking rules and expressing the bounds on type parameters for polymorphism. The design of PolyTOIL is based on a careful formal definition of type-checking rules and semantics. A proof of type safety is obtained with the aid of a subject reduction theorem.

References

[1]

Amadio, R. and Cardelli, L. 1993. Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15, 4, 575--631.

[2]

Abadi, M. and Cardelli, L. 1994a. A theory of primitive objects: Second-order systems. In Proceedings of ESOP '94, Springer-Verlag, New York, 1--24.

[3]

Abadi, M. and Cardelli, L. 1994b. A theory of primitive objects: Untyped and first-order systems. In Proceedings of Theoretical Aspects of Computer Software, Springer-Verlag, New York, 296--320.

[4]

Abadi, M. and Cardelli, L. 1995. An imperative object calculus. In TAPSOFT '95: Theory and Practice of Software Development, P.D. Mosses and M. Nielsen, Eds., Lecture Notes in Computer Science, vol. 915, Springer-Verlag, New York, 471--485.

[5]

Abadi, M. and Cardelli, L. 1996. A Theory of Objects. Springer-Verlag, New York.

[6]

Arnold, K. and Gosling, J. 1996. Java. Addison-Wesley, Reading MA.

[7]

Amadio, R. M. 1991. Recursion over realizability structures. Inf. Comput. 91, 1, 55--86.

[8]

Abadi, M. and Plotkin, G. D. 1990. A PER model of polymorphism and recursive types. In Proceedings of the Symposium on Logic in Computer Science, 355--365.

[9]

Bruce, K. B., Crabtree, J., Dimock, A., Muller, R., Murtagh, T., and van Gent, R. 1993. Safe and decidable type checking in an object-oriented language. In Proceedings of the ACM Symposium on Object-Oriented Programming: Systems, Languages, and Applications, 29--46.

[10]

Bruce, K. B., Crabtree, J., and Kanapathy, G. 1994. An operational semantics for TOOPLE: A statically-typed object-oriented programming language. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, Eds., Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, vol. 802, Springer-Verlag, New York, 603--626.

[11]

Bruce, K. B., Fiech, A., and Petersen, L. 1997. Subtyping is not a good "match" for object-oriented languages. In Proceedings of ECOOP '97, Lecture Notes in Computer Science, vol. 1241, Springer-Verlag, New York, 104--127.

[12]

Bracha, G. and Griswold. D. 1993. Strongtalk: Typechecking Smalltalk in a production environment. In Proceedings of the ACM Symposium on Object-Oriented Programming: Systems, Languages, and Applications, 215--230.

[13]

Bruce, K. B. and Longo, G. 1990. A modest model of records, inheritance and bounded quantification. Inf. Comput. 87, 1/2, 196--240.

[14]

Bruce, K. B. and Mitchell, J. C. 1992. PER models of subtyping, recursive types and higher-order polymorphism. In Proceedings of the ACM Symposium on Principles of Programming Languages, 316--327.

[15]

Bruce, K. B. 1993. Safe type checking in a statically typed object-oriented programming language. In Proceedings of ACM Symposium on Principles of Programming Languages, 285--298.

[16]

Bruce, K. B. 1994. A paradigmatic object-oriented programming language: Design, static typing and semantics. J. Funct. Program. 4, 2, 127--206. An earlier version of this paper appeared in the 1993 POPL Proceedings.

[17]

Bruce, K. B. 2002. Foundations of Object-Oriented Languages: Types and Semantics. MIT Press, Cambridge, MA.

[18]

Bruce, K. B. and van Gent, R. 1993. TOIL: A new type-safe object-oriented imperative language. Tech. Rep. Williams College.

[19]

Cardelli, L. 1988. A semantics of multiple inheritance. Inf. Comput. 76, 138--164. (Special issue devoted to the Symposium on Semantics of Data Types (Sophia-Antipolis France, 1984).

[20]

Cardone, F. 1989. Relational semantics for recursive types and bounded quantification. In ICALP, Lecture Notes in Computer Science, vol. 372, Springer-Verlag, New York, 164--178.

[21]

Canning, P., Cook, W. R., Hill, W., Mitchell, J. C., and Olthoff, W. 1989. F-bounded quantification for object-oriented programming. In Funct. Prog. Comput. Arch. 273--280.

[22]

Cook, W. R., Hill, W. L., and Canning, P. S. 1990. Inheritance is not subtyping. In Proceedings of the Seventeenth ACM Symposium on Principles of Programming Languages (January), 125--135.

[23]

Cook, W. R. 1989. A proposal for making Eiffel type-safe. In Proceedings of the European Conference on Object-Oriented Programming, 57--72.

[24]

Cardelli, L. and Wegner, P. 1985. On understanding types, data abstraction, and polymorphism. Comput. Surv. 17, 4, 471--522.

[25]

Day, M., Gruber, R., Liskov, B., and Meyers, A. C. 1995. Subtypes vs. where clauses: Constraining parametric polymorphism. In Proceedings of the ACM Symposium on Object-Oriented Programming: Systems, Languages, and Applications, 156--168.

[26]

Ellis, M. A. and Stroustrop, B. 1990. The Annotated C++ Reference Manual. Addison-Wesley, Reading, MA.

[27]

Eifrig, J., Smith, S., Trifonov, V., and Zwarico, A. 1994. Application of OOP type theory: State, decidability, integration. In Proceedings of OOPSLA '94, 16--30.

[28]

Fisher, K., Honsell, F., and Mitchell, J. C. 1993. A lambda calculus of objects and method specialization. Nordic J. Comput. 1, 3--37. An earlier version of this paper appeared in Proceedings of the Eighth IEEE Symposium on Logic in Computer Science, 1993, 26--38.

[29]

Fisher, K. and Mitchell, J. C. 1998. On the relationship between classes, objects, and data abstraction. TAPOS 4, 3--32.

[30]

Gawecki, A. and Matthes, F. 1996. Integrating subtyping, matching and type quantification: A practical perspective. In Proceedings of ECOOP '96, Lecture Notes in Computer Science, vol. 1098, Springer-Verlag, New York, 26--47.

[31]

Goldberg, A. and Robson, D. 1983. Smalltalk--80: The Language and Its Implementation. Addison-Wesley, Reading, MA.

[32]

Gunter, C. A. 1992. Semantics of Programming Languages: Structures and Techniques. MIT Press, Cambridge, MA.

[33]

Igarashi, A., Pierce, B., and Wadler, P. 1999. Featherweight Java: A minimal core calculus for Java and GJ. In OOPSLA Proceedings (October). Full version to appear in ACM Trans. Program. Lang. Syst. 2001.

[34]

Katiyar, D., Luckham, D., and Mitchell, J. 1994. A type system for prototyping languages. In Proceedings of the 21st ACM Symposium on Principles of Programming Languages, 138--150.

[35]

Meyer, B. 1992. Eiffel: The Language. Prentice-Hall, Englewood Cliffs, NJ.

[36]

Meyer, B. 1995. Static typing and other mysteries of life. Tech. Rep., Interactive Software Engineering, Inc. Text of invited address to OOPSLA '95.

[37]

Mitchell, J. C. 1990. Toward a typed foundation for method specialization and inheritance. In Proceedings of the Seventeenth ACM Symposium on Principles of Programming Languages (January), 109--124.

[38]

Madsen, O., Magnusson, B., and Moller-Pedersen, B. 1990. Strong typing of object-oriented languages revisited. In OOPSLA-ECOOP '90 Proceedings, 140--150. ACM SIGPLAN Not. 25, 10, (Oct.).

[39]

Pierce, B. C. 1993. Mutable objects. Tech. Rep., University of Edinburgh.

[40]

Pierce, B. C. 1994. Bounded quantification is undecidable. Inf. Comput. 112, 1, (July), 131--165. Reprinted in Theoretical Aspects of Object-Oriented Programming, Gunter and Mitchell, Eds., MIT Press, Cambridge, MA, 427--459. Summary in POPL '92.

[41]

Pierce, B. C. and Turner, D. N. 1993. Object-oriented programming without recursive types. In Proceedings of the Twentieth ACM Symposium Principles of Programming Languages, 299--312.

[42]

Pierce, B. C. and Turner, D. N. 1994. Simple type-theoretic foundations for object-oriented programming. J. Funct. Program. 4, 207--247. An earlier version appeared in Proceedings of of POPL '93, 299--312.

[43]

Reynolds, J. C. 1980. Using category theory to design implicit conversions and generic operators. In Semantics-Directed Compiler Generation, N. D. Jones, Ed., Lecture Notes in Computer Science, vol. 94, Springer-Verlag, New York, 211--2580.

[44]

Schaffert, C., Cooper, T., Bullis, B., Kilian, M., and Wilpolt, C. 1986. An introduction to Trellis/Owl. In OOPSLA '86 Proceedings, 9--16. ACM SIGPLAN Not. 21, 11, (Nov.).

[45]

Tesler, L. 1985. Object Pascal report. Tech. Rep. 1, Apple Computer.

[46]

van Gent, R. 1993. TOIL: An imperative type-safe object-oriented language. Williams College Senior Honors Thesis.

Cited By

Zhang YMyers A(2017)Familia: unifying interfaces, type classes, and family polymorphismProceedings of the ACM on Programming Languages10.1145/31338941:OOPSLA(1-31)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133894
Vanwormhoudt GCaron OCarré B(2017)Aspectual templates in UMLSoftware and Systems Modeling (SoSyM)10.1007/s10270-015-0463-316:2(469-497)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1007/s10270-015-0463-3
Ryu S(2016)ThisType for Object-Oriented LanguagesACM Transactions on Programming Languages and Systems10.1145/288839238:3(1-66)Online publication date: 8-Apr-2016
https://dl.acm.org/doi/10.1145/2888392
Show More Cited By

Index Terms

PolyTOIL: A type-safe polymorphic object-oriented language
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
    2. General programming languages
      1. Language features
        Classes and objects
        Constraints
        Inheritance
        Polymorphism
      2. Language types
        Object oriented languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Object oriented constructs
    2. Program semantics
      1. Operational semantics

Recommendations

PolyTOIL: A Type-Safe Polymorphic Object-Oriented Language
ECOOP '95: Proceedings of the 9th European Conference on Object-Oriented Programming

PolyTOIL is a new statically-typed polymorphic object-oriented programming language which is provably type-safe. By separating the definitions of subtyping and inheritance, providing a name for the type of self, and carefully defining the type-checking ...
Type-safe convariant specialization with generalized matching
FOOL VII

Matching is a relation between object types originally designed to support type-safe subclassing with binary methods. In this paper we generalize it to deal with general covariance by allowing field and method parameter types to change covariantly in ...
On subtyping and matching

A relation between recursive object types, called matching, has been proposed as a generalization of subtyping. Unlike subtyping, matching does not support subsumption, but it does support inheritance of binary methods. We argue that matching is a good ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 25, Issue 2

March 2003

132 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/641888

Issue’s Table of Contents

Copyright © 2003 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 2003

Published in TOPLAS Volume 25, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
1,105
Total Downloads

Downloads (Last 12 months)100
Downloads (Last 6 weeks)18

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhang YMyers A(2017)Familia: unifying interfaces, type classes, and family polymorphismProceedings of the ACM on Programming Languages10.1145/31338941:OOPSLA(1-31)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133894
Vanwormhoudt GCaron OCarré B(2017)Aspectual templates in UMLSoftware and Systems Modeling (SoSyM)10.1007/s10270-015-0463-316:2(469-497)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1007/s10270-015-0463-3
Ryu S(2016)ThisType for Object-Oriented LanguagesACM Transactions on Programming Languages and Systems10.1145/288839238:3(1-66)Online publication date: 8-Apr-2016
https://dl.acm.org/doi/10.1145/2888392
Bryant BJézéquel JLämmel RMernik MSchindler MSteinmann FTolvanen JVallecillo AVölter M(2014)Globalized Domain Specific Language EngineeringRevised Papers of the International Dagstuhl Seminar on Globalizing Domain-Specific Languages - Volume 940010.1007/978-3-319-26172-0_4(43-69)Online publication date: 5-Oct-2014
https://dl.acm.org/doi/10.1007/978-3-319-26172-0_4
Na HRyu S(2014)A New Formalization of Subtyping to Match Subclasses to SubtypesFunctional and Logic Programming10.1007/978-3-319-07151-0_15(238-252)Online publication date: 2014
https://doi.org/10.1007/978-3-319-07151-0_15
Sun WCombemale BDerrien SFrance R(2013)Using model types to support contract-aware model substitutabilityProceedings of the 9th European conference on Modelling Foundations and Applications10.1007/978-3-642-39013-5_9(118-133)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39013-5_9
Na HRyu SChoe KPierce B(2012)Exact type parameterization and ThisType supportProceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation10.1145/2103786.2103790(13-24)Online publication date: 28-Jan-2012
https://dl.acm.org/doi/10.1145/2103786.2103790
Guy CCombemale BDerrien SSteel JJézéquel J(2012)On model subtypingProceedings of the 8th European conference on Modelling Foundations and Applications10.1007/978-3-642-31491-9_30(400-415)Online publication date: 2-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31491-9_30
Wehr SThiemann P(2011)JavaGIACM Transactions on Programming Languages and Systems10.1145/1985342.198534333:4(1-83)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1145/1985342.1985343
Oliveira B(2009)Modular Visitor ComponentsProceedings of the 23rd European Conference on ECOOP 2009 --- Object-Oriented Programming10.1007/978-3-642-03013-0_13(269-293)Online publication date: 30-Jul-2009
https://dl.acm.org/doi/10.1007/978-3-642-03013-0_13
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents