Abstract
This paper presents an algorithm for polymorphic type inference involving the let construct of ML in the context of higher order abstract syntax. It avoids the polymorphic closure operation of the algorithm W of Damas and Milner by using a uniform treatment of type variables at the meta-level. The basic technique of the algorithm facilitates the declarative formulation of type inference as goal-directed proof-search in a logical frameworks setting.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andrew Appel and Zhong Shao. Smartest Recompilation. In Tenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1993. Longer version as Princeton University Technical Report CS-TR-395-92.
Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Ninth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 207–212, January 1982.
Scott Dietzen and Frank Pfenning. A declarative alternative to assert in logic programming. In Proceedings of the 1991 International Logic Programming Symposium, pages 372–386. MIT Press, 1991.
G. Dowek et al. The Coq proof assistant user's guide. Technical Report 134, INRIA, 1993.
C. A. Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. MIT Press, 1992.
John Hannan. Extended natural semantics. Journal of Functional Programming, 3(2):123–152, April 1993.
Robert Harper. Systems of polymorphic type assignment in LF. Technical Report CMU-CS-90-144, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1990.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993.
P. M. Hill and J. G. Gallagher. Meta-programming in logic programming. Technical Report Report 94.22, University of Leeds, hill@scs.leeds.ac.uk, August 1994. To appear in Vol. 5 of the Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press.
Trevor Jim. What are principal typings and what are they good for? Technical Report MIT/LCS TM-532, MIT, November 1995. Extended version of a paper appearing in ACM Symposium on Principles of Programming Languages, 1996.
Stefan Kaes. Type Inference in the presence of Overloading, Subtyping, and Recursive types. In 1992 ACM conference on LISP and Functional Programming, San Francisco, CA, pages 193–204. ACM Press, 1992.
Daniel Leivant. Polymorphic type inference. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 88–98, 1983.
Chuck Liang. Substitution, Unification and Generalization in Meta-Logic. PhD thesis, University of Pennsylvania, September 1995.
Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329–359. Academic Press, 1990.
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.
Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, September 1989.
Frank Pfenning and Conal Elliot. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, June 1988.
Mitchell Wand. A simple algorithm and proof for type inference. Fundamenta Infomaticae, 10:115–122, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liang, C. (1997). Let-polymorphism and eager type schemes. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030621
Download citation
DOI: https://doi.org/10.1007/BFb0030621
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive