Abstract
We present a type inference algorithm for a Haskell-like language based on order-sorted unification. The language features polymorphism, overloading, type classes and multiple inheritance. Class and instance declarations give rise to an order-sorted algebra of types. Type inference essentially reduces to the Hindley/Milner algorithm where unification takes place in this order-sorted algebra of types. The theory of order-sorted unification provides simple sufficient conditions which ensure the existence of principal types. The semantics of the language is given by a translation into ordinary λ-calculus. We prove the correctness of our type inference algorithm with respect to this semantics.
Research supported by ESPRIT BRA 3245, Logical Frameworks.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
D. Clément, J. Despeyroux, T. Despeyroux, and G. Kahn. A simple applicative language: Mini-ML. In Proc. ACM Conf. Lisp and Functional Programming, pages 13–27, 1986.
M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and λ-calculus semantics. In R. Hindley and J. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalisms. Academic Press, 1980.
L. Damas and R. Milner. Principal type schemes for functional programs. In Proc. 9th ACM Symp. Principles of Programming Languages, pages 207–212, 1982.
K. Futatsugi, J. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proc. 12th ACM Symp. Principles of Programming Languages, pages 52–66, 1985.
F. Grosch and G. Snelting. Inference-based overloading resolution for ADA. In Proc. 2nd Conf. Programming Language Implementation and Logic Programming, pages 30–44. LNCS 456, 1990.
P. Hudak and P. Wadler. Report on the programming language Haskell. Version 1.0, April 1990.
S. Kaes. Parametric overloading in polymorphic programming languages. In Proc. 2nd European Symposium on Programming, pages 131–144. LNCS 300, 1988.
J. Meseguer, J. Goguen, and G. Smolka. Order-sorted unification. J. Symbolic Computation, 8:383–413, 1989.
R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.
T. Nipkow. Higher-order unification, polymorphism, and subsorts. In Proc. 2nd Int. Workshop Conditional and Typed Rewriting Systems. LNCS ???, 1990.
M. Schmidt-Schauß. A many-sorted calculus with polymorphic functions based on resolution and paramodulation. In Proc. 9th Int. Joint Conf. Artificial Intelligence, pages 1162–1168, 1985.
G. Smolka, W. Nutt, J. Goguen, and J. Meseguer. Order-sorted equational computation. In H. Aït-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2, pages 297–367. Academic Press, 1989.
G. Snelting. The calculus of context relations. Acta Informatica, 1991. To appear.
P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Proc. 16th ACM Symp. Principles of Programming Languages, pages 60–76, 1989.
U. Waldmann. Unification in order-sorted signatures. Technical Report 298, Fachbereich Informatik, Universität Dortmund, 1989.
M. Wand. Type inference for record concatenation and multiple inheritance. In Proc. 4th IEEE Symp. Logic in Computer Science, pages 92–97, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nipkow, T., Snelting, G. (1991). Type classes and overloading resolution via order-sorted unification. In: Hughes, J. (eds) Functional Programming Languages and Computer Architecture. FPCA 1991. Lecture Notes in Computer Science, vol 523. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540543961_1
Download citation
DOI: https://doi.org/10.1007/3540543961_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54396-1
Online ISBN: 978-3-540-47599-6
eBook Packages: Springer Book Archive