Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ser. POPL
We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.
M. Odersky and K. Läufer, Putting type annotations to work, in Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ser. POPL '96. New York, NY, USA: ACM, 1996, pp. 54-67. [Online]. Available: http://webpages.cs.luc.edu/~laufer/papers/popl96.pdf
Creative Commons License
This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 License.
Copyright © 1996 Martin Odersky and Konstantin Läufer