Abstract
Flexibility of programming and efficiency of program execution are two important features of a programming language. Unfortunately, however, there is an inherent conflict between these features in design and implementation of a modern statically typed programming language. Flexibility is achieved by high-degree of polymorphism, which is based on generic primitives in an abstract model of computation, while efficiency requires optimal use of low-level primitives specialized to individual data structures. The motivation of this work is to reconcile these two features by developing a mechanism for specializing polymorphic primitives based on static type information. We first present a method for coherent transformation of an ML style polymorphic language into an explicitly typed calculus. We then analyze the existing methods for compiling record calculus and unboxed calculus, extract their common structure, and develop a framework for type based specialization of polymorphism.
Partly supported by the Japanese Ministry of Education Grant-in-Aid for Scientific Research on Priority Area 275: “advanced databases”.
Preview
Unable to display preview. Download preview PDF.
References
Appel, A. W. and MacQueen, D. B. Standard ML of New Jersey. In Proceedings of the 3rd International Symposium on Programming Languages and Logic Programming. Lecture Notes in Computer Science, vol. 528, 1–13, 1991.
Breazu-Tannen, V., Coquand, T., Gunter, C., and Scedrov, A. Inheritance as explicit coercion. Inf. Comput. 93, 172–221, 1991.
Buneman, P. and Ohori, A. Polymorphism and type inference in database programming. ACM Trans. Database Syst., 21(1), 30–74, 1996.
Damas, L. and Milner, R. Principal type-schemes for functional programs. In Proceedings of the ACM Symposium on Principles of Programming Languages, 207–212, 1982.
de Bruijn, N. G. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Math., Vol. 34, pp. 381–392, 1972.
Dubois, C and Weise, P. Generic polymorphism. In Proceedings of the ACM Symposium on Principles of Programming Languages, 1995.
Girard, J.-Y. Une extension de l'interpretation de gödel á l'analyse, et son application á l'élimination des coupures dans l'analyse et théorie des types. In the 2nd Scandinavian Logic Symposium. North-Holland, Amsterdam, 1971.
Hall, C. Using Hindley-Milner type inference to optimize list representation. In Proceedings of the ACM Conference on Lisp and Functional Programming, 1994.
Hall, C., Hammond, K., Peyton Jones, S., and Wadler, P. Type class in Haskell. Tech. rep., Univ. of Glasgow, Glasgow, Scotland, 1994.
Harper, R. and Mitchell, J. C. On the type structure of Standard ML. ACM Trans. Program. Lang. Syst. 15, 2, 211–252, 1993.
Harper, R. and Morrisett, G. Compiling polymorphism using intensional type analysis. In Proceedings of the ACM Symposium on Principles of Programming Languages, 130–141, 1995.
Hudak, P. et. al. Report on programming language Haskell a non-strict, purely functional language version 1.2. SIGPLAN Notices, Vol. 27, No. 5, I992.
Jones, M. ML typing, explicit polymorphism and qualified types. In Proceedings of Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, vol. 789, pages 56–75, 1994.
Kahn, G. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 22–39. Springer Verlag, Berlin, 1987.
Leroy, X. The ZINC Experiment: an economical implementation of the ML language. Technical report, No. 117, INRIA, France, 1992.
Leroy, X. Unboxed objects and polymorphic typing. In Proceedings of the ACM Symposium on Principles of Programming Languages, 177–188, 1992.
Milner, R. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348–375, 1978.
Milner, R., Tofte, M., and Harper, R. The Definition of Standard ML. MIT Press, Cambridge, Mass, 1990.
Minamide, Y. Compilation based on a calculus for explicit type passing. In Proceedings of Fuji International Workshop on Functional and Logic Programming, 301–320,1996.
Mitchell, J. Type systems for programming languages. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. MIT Press, Cambridge, Mass., 365–458, 1990.
The Objective Caml User's Manual. INRIA Rocquencourt. B.P. 105,78153 Le Chesnay, France.
Ohori, A. A simple semantics for ML polymorphism. In Proceedings of the ACM/IFIP Conference on Functional Programming Languages and Computer Architecture, 281–292, 1989.
Ohori, A. A compilation method for ML-style polymorphic record calculi. In Proceedings of the ACM Symposium on Principles of Programming Languages, 154–165, 1992.
Ohori, A. and Takamizawa, T. A polymorphic unboxed calculus as an abstract machine for polymorphic languages. To appear in Journal of Lisp and Symbolic Computation, 1997.
Ohori, A. A polymorphic record calculus and its compilation. ACM Trans. Program. Lang. Syst., 17(6):844–895, 1995.
Peterson, J. and Jones, M. Implementing type classes. In Proceedings of the ACM Conference on Programming Language Design and Implementation, 227–236, 1993.
Peyton Jones, S.L. and Launchbury, J. Unboxed values as first class citizens in a non-strict functional language. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture, pages 636–666. Lecture Notes in Computer Science, Vol 523. Springer-Verlag, Berlin, 1991.
Rémy, D. Efficient representation of extensible records. In Proceedings of the ACM SIGPLAN Workshop on ML and Its Applications, 12–16, 1994.
Reynolds, J. Towards a theory of type structure. In the Paris Colloquium on Programming. Springer-Verlag, Berlin, 408–425, 1974.
Shao, Z., Reppy, J., and Apple, A. W. Unrolling lists. In Proceedings of the ACM Conference on Lisp and Functional Programming, 1994.
Tolmach, A. Tag-free garbage collection using explicit type parameters. In Proceedings of the ACM Conference on Lisp and Functional Programming, 1–11, 1994.
Wright, A.K. Polymorphism for imperative languages without imperative types. Technical Report TR93-200, Rice University, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ohori, A. (1997). Type system for specializing polymorphism. In: Abadi, M., Ito, T. (eds) Theoretical Aspects of Computer Software. TACS 1997. Lecture Notes in Computer Science, vol 1281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014549
Download citation
DOI: https://doi.org/10.1007/BFb0014549
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63388-4
Online ISBN: 978-3-540-69530-1
eBook Packages: Springer Book Archive