Konstantin Läufer
Martin Odersky
Abstract
Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to variables, passed as function parameters, or returned as function results. Several higher-order functional languages feature strong and static type systems, parametric polymorphism, algebraic data types, and explicit type variables. Most of them rely on Hindley-Milner type inference instead of requiring explicit type declarations for identifiers. Although some of these languages support abstract data types, it appears that none of them directly provides light-weight abstract data types whose implementations are first-class values. We show how to add significant expressive power to statically typed functional languages with explicit type variables by incorporating first-class abstract types as an extension of algebraic data types. Furthermore, we extend record types to allow abstract components. The components of such abstract records are selected using the dot notation. Following Mitchell and Plotkin, we formalize abstract types in terms of existentially quantified types. We give a syntactically sound and complete type inference algorithm and prove that our type system is semantically sound with respect to standard denotational semantics.
- BURSTALL, R., MACQUEEN, D., AND SANNELLA, D. 1980. Hope: An experimental applicative language. In Stanford LISP Conference 1980, 136-143. Google Scholar
- CARDELLI, L. AND LEROY, X. 1990. Abstract types and the dot notation. In Proceedings of the IFIP Working Conference on Programming Concepts and Methods (Sea of Galilee, Israel). IFIP, 466-49t.Google Scholar
- CARDELLI, L. AND WEANER, P. 1985. On understanding types, data abstraction and polymorphism. ACM Comput. Surv. 17, 4 (Dec.), 471-522. Google Scholar
- CLEMENT, D., DESPEYROUX, g., DESPEYROUX, T., AND KAHN, C--. 1986. A simple applicative language: Mini-ML. In Proceedings of the ACM Conference on Lisp and Functional Programruing. ACM, New York, 13-27. Google Scholar
- DAMAS, L. 1985. Type assignment in programming languages. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.Google Scholar
- DAMAS, L. AND MILNER, R. 1982. Principal type schemes for functional programs. In Proceedings of the 9th ACM Symposium on Principles of Programming Languages, (Jan.). ACM, New York, 207-212. Google Scholar
- HARPER, R. 1990. Introduction to Standard ML. Tech. Rep., School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Pa.Google Scholar
- HARPER, R. AND LILLIBRIDGE, M.A. 1994. A type-theoretic approach to higher-order modules with sharing. In Proceedings of the 21th ACM Symposium on Principles of Programming Languages. ACM, New York, 123-137. Google Scholar
- HUDAK, P., PEYTON-JONES, S., WADLER, P., EDS. 1992. Report on the programming language Haskell: A non-strict, purely functional language Version 1.2. ACM SIGPLAN Not. 27, 5 (May). Google Scholar
- LAUFER, K. 1992. Polymorphie type inference and ab~rac~ data type8. Ph.D. thesis, New York Univ., New York. Available as Tech. Rep. 622, Dec. 1992, from New York Univ., Dept. of Computer Science. Google Scholar
- LAUFER, K. AND ODERSKY, M. 1991. Type classes are signatures of abstract types. In Proceedings of the Phoenix Seminar and Workshop on Declarative Programming (Nov.). Google Scholar
- LEROY, X. 1994. Manifest types, modules, and separate compilation. In Proceedings of the 21th ACM Symposium on Principles of Programming Languages. (Jan.). ACM, New York, 109-123. Google Scholar
- LEROY, X. AND MAUNY, M. 1992. The Carol Light System, Release 0.5, Documentation and User's Manual. Sept. Distributed with the Carol Light system.Google Scholar
- LEROY, X. AND MAUNY, M. 1991. Dynamics in ML. In Proceedings ACM Functional Programruing Languages and Computer Architecture. ACM, New York, 406-426. Google Scholar
- MACQUEEN, D. 1986. Using dependent types to express modular structure. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages. ACM, New York, 277-286. Google Scholar
- MACQUEEN, D., PLOTKIN, G., AND SETHI, R. 1986. An ideal model for recursive polymorphic types. Inf. Control 71, 95-130. Google Scholar
- MEYER, A. AND REINHOLD, M. 1986. Type is not a type. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages. (Jan.). ACM, New York, 287-295. Google Scholar
- MILNER, R., TOFTE, M., AND HARPER, R. 1990. The Definition of Standard ML. MIT Press, Cambridge, Mass. Google Scholar
- MITCHELL, J. AND HARPER, R. 1988. The essence of ML. In Proceedings of the ACM Symposium on Principles of Programming Languages (Jan.). ACM, New York. Google Scholar
- MITCHELL, J. AND PLOTKIN, G. 1988. Abstract types have existential type. ACM Trans. Program. Lang, Syst. 10, 3,470-502. Google Scholar
- MITCHELL, J., MELDAL, S., AND MADHAV, N. 1991. An extension of Standard ML modules with subtyping and inheritance. In Proceedings of the 18th ACM Symposium on Principles of Programming Languages (Jan.). ACM, New York. Google Scholar
- ODERSKY, M. 1991. Objects and subtyping in a functional perspective. Tech. Rep. RC 16423, IBM, T. J. Watson Research Center, Yorktown Heights, N.Y.Google Scholar
- PERRY, N. 1990. The implementation of practical functional programming languages. Ph.D. thesis, Imperial College, London, U.K.Google Scholar
- PIERCE, B. AND TURNER, D. 1993. Simple type-theoretic foundations for object-oriented programming. J. Functional Program. (April). To be published.Google Scholar
- PLOTKIN, G. 1983. Domains. Course notes. TeX-ed edition.Google Scholar
- TURNER, D. 1985. Miranda: A non-strict functional language with polymorphic types. In Proceedings of Functional Programming Languages and Computer Architecture (Nancy, France). Lecture Notes in Computer Science, vol. 201, Springer-Verlag, New York, 1-16. Google Scholar
- WADLER, P. AND BLOTT, S. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM Symposium on Principles of Programming Languages (Jan.). ACM, New York, 60-76. Google Scholar
- WINSKEL, G. 1993. The Formal Semantics of Programming Languages. MIT Press, Cambridge, Mass. Google Scholar
Index Terms
- Polymorphic type inference and abstract data types
Recommendations
Type inference for unboxed types and first class mutability
PLOS '06: Proceedings of the 3rd workshop on Programming languages and operating systems: linguistic support for modern operating systemsSystems programs rely on fine-grain control of data representation and use of state to achieve performance, conformance to hard-ware specification, and temporal predictability. The robustness and checkability of these programs could be greatly improved ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Comments