Benjamin C. Pierce
David N. Turner
ABSTRACT
We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function. abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices by a statistical analysis of the uses of type inference in a sizable body of existing ML code.
- AN91.Shaft Aditya and Rishiyur S. Nikhil. Incremental polymorphism. In Functional Programming Languages and Computer Architecture, number 523 in Lecture Notes in Computer Science. Springer-Verlag, August 1991. Also available as MIT CSG Memo 329, June 1991. Google Scholar
Digital Library
- AW93.Alexander Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Gonference on Functional Programming Languages and Computer Architecture, pages 31--41. ACM press, 1993. Google ScholarDigital Library
- Boe85.Hans-J. Boehm. Partial polymorphic type inference is undecidable. In 26th Annual Symposium on Foundations of. Computer Science, pages 339-345. IEEE, October 1985.Google ScholarDigital Library
- Boe89.Hans-J. Boehm. Type inference in the presence of type abstraction. In Proceedings of the SIG- PLAN "89 Con}erence on Programming Language Design and Implementation, pages 192- 206, Portland, OR, June 1989. Google ScholarDigital Library
- Car91.Luca Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts. Springer-Verlag, 1991. An earlier version appeared as DEC Systems Research Center Research Report ~45, February 1989.Google Scholar
- Car93.Luca Cardelli. An implementation of F<. Research report 97, DEC Systems Research Center, February 1993.Google Scholar
- CG92.Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption: Minimum typing and type-checking in F<. Mathematical Structures in Computer Science, 2-.55--91, 1992. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994). Google ScholarDigital Library
- CMMS94.Luca Cardelli, Simone Martini, John C. Mitehell~ and Andre Scedrov. An extension of system F with subtyping. Information and Computation, 109(1-2):4-56, 1994. A preliminary version appeared'in TACS '91 (Sendai, Japan, pp. 750- 770). Google ScholarDigital Library
- Com94.Adriana B. Compaguoni. Decidability of higherorder subtyping with intersection types. In Computer Science Logic, September 1994. Kazimierz, Poland. Springer Lecture Notes in Computer Science 933, June 1995. Also available as University of Edinburgh, LFCS technical report ECS- LFCS-94-281, titled "Subtyping in F,~ is decidable".Google Scholar
- CW85.Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), December 1985. Google ScholarDigital Library
- DHKP96.Giiles Dowek, Thdrkse Hardin, Claude Kirchner, and l~rank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In M. Maher, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 259-273, Bonn, Germany, September 1996. MIT Press.Google ScholarDigital Library
- EST95.Jonathan Eifrig, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and its application to OOP. In Proceedings of the 1995 Mathematical Foundations of Programming Semantics Conference, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.Google ScholarCross Ref
- FF97.Cormac Flanagan and Matthias Felhisen. Componential set-based analysis. "ACM SIGPLAN Notices, 32(5):235-248, May 1997. Google ScholarDigital Library
- Gir72.Jean-Yves Girard. Interprgtation fonctionelle et dimination des coupures de l'arithmdtique d'ordre sup.grieur. PhD thesis, Universit4 Paris VII, 1972.Google Scholar
- GP97.Giorgio Ghelli and Benjamin Pierce. Bounded existentials and minimal typing. Theoretical Computer Science, 1997. To appear. Google ScholarDigital Library
- GR97.Jaques Garrigue and Didier Rdrny. Extending ML with semi:explicit polymorphism. In Martfn Abadi and Takayasu Ito, editors, International Symposium on Theoretical Aspects of Computer Software (TAGS), Sendai, Japan, pages 20-46. Springer-Verlag, September 1997. Google ScholarDigital Library
- Hue75.Gdrard Huet. A unification algorithm for typed " A-calculus. Theoretical Computer Science, 1:27- 57, 1975.Google ScholarCross Ref
- JG89.James W. O'Toole Jr. and David K. Gifford. Type reconstruction with first-class polymorphic values. In Proceedinps of the SIGPLAN'89 Conference on Programming Language Design and Implemenfation, Portland, Oregon, pages 207- 217. ACM Press, June 1989. Google ScholarDigital Library
- JW95.Suresh Jagannathan and Andrew Wright. Effective flow analysis for avoiding run-time checks, in Proceedings of the Second International Static Analysis Symposium, volume 983 of LNCS, pages 207-224. Springer-Verlag, 1995. Google ScholarDigital Library
- LO94.Konstantin Lfiufer and Martin Odersky. Polymorphic type inference and abstract data types. A CM Transactions on Programming Languages and Systems (TOPLAS), 16(5):1411- 1430, September 1994. An earlier version appeared in the Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, 1992, under the title "An Extension of ML with First- Class Abstract Types". Google ScholarDigital Library
- Mil92.Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321- 358, October 1992. Google ScholarDigital Library
- OL96.Martin Odersky and Konstantin L~.ufer. Putting type annotations to work. In Conference Record of POPL 'gr: the 23rd ACM SIGPLAN. SIGA CT Symposium on Principles of Program. ming Languages, pages 54-67, St. Petersburg, Florida, January 21-24, 1996. ACM Press. Google ScholarDigital Library
- OW97.Martin Odersky and Philip Wadler. Pizza Into Java: Translating theory into pratt|co. In Principles of Programming Languages (POPL), 1997. A preliminary version appeared as Technical Report, 26/96, University of Karlsruhe, July 1996.Google Scholar
- Per90.Nigel Perry. The Implementation of Practical Functional Programming Languages. PhD thesis, Imperial College, 1990.Google Scholar
- Pfe88.Frank Pfenning. Partial polymorphic type inference and higher-order unification. In Proeeedings of the 1988 A GM Conference on Lisp and Functional Programming, Snowbird, Utath pages 153-163. ACM Press, July 1988. Also available as Ergo Report 88-048, School of Computer Science, Carnegie Mellon University, Pittsburgh. Google ScholarDigital Library
- Pfe89.Frank Pfenning. Elf: A language for logic definition and verified morn-programming. In Fourth Annual Symposium on Logic in Computer Science, pages 313-322, Pacific Grove, California, June 1989. IEEE Computer Society Press. Google ScholarDigital Library
- Pfe93.Frank Pfenning. On the undecidability of partial polymorphic type reconstruction. Fanda. menta lnformaticae~ 19(1,2):185-199, 1993. Preliminary version available as Technical Repor~ CMU-CS-92-105, School of Computer Sclence~ Carnegie Mellon University, January 1992. Google ScholarDigital Library
- Pie97.Benjamin C. Pierce. Bounded quantification with bottom. Technical Report 492, Computer Science Department, Indiana University, t997.Google Scholar
- PL91.Frank Pfenning and Peter Lee. Metacircularlty in the polymorphic A-calculus. Theoretical Gempurer Science, 89(1):137-159, 21 October 1991, A preliminary version appeared in TAPSOFT "89, Proceedings of the International Joint Conference on Theory and Practice in soSttoarc Development, Barcelona, Spain, pages 345-359, Springer-~erlag LNCS 352~ March 1989. Google ScholarDigital Library
- Pot97.Francois Pottier. Simplifying subtyplng constr~nts. In Proceedings of the Interns. lions! Conference on Functional Programming (ICFP), 1997. Google ScholarDigital Library
- PS94.Benjamin Pierce and Martin Steffen. Higherorder subtyping. In 1FIP Working Conference on Pro#ramming Concepts, Methods and Calculi (PROCOMET), 1994. Full version in Theorelf. cal Computer Science, eel. 176, no. 1-2, pp. 235- 282, 1997. Google ScholarDigital Library
- PT97a.Benjamin C. Pierce and David N. Turner. Local type argument synthesis with bounded quantification. Technical Report 495, Computer Scivnco Department, Indiana University, 1997.Google Scholar
- PT97b.Benjamin C. Pierce and David N. "Darner. Local type inference. Technical Report 493, Computer Science Department, Indiana University, 1997.Google Scholar
- PT97c.Benjamin C. Pierce and David N. Turner. Pier: A programming language based on the plcalculus. Technical Report CSCI 476, Computer Science Department, Indian~ University, 1997. To appear in Proof, Language and InteracLion: Essays in Honour of Robin Milner, Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, MIT Press.Google Scholar
- Rém89.Didier P~my. TypechecXing records and variants in a natural extension of ML. In Proceedings of the Sizteenth Annual A CM Symposium on Principles of Programming Languages, Austin, pages 242-249. ACM, January 1989. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Objects-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994). Google ScholarDigital Library
- Rém94.Didier R~my. Programming objects with ML-ART: An extension to ML with abstract and record types. In Masami Hagijra and John C. Mitchell, editors, International Symposium on Theoretical Aspects of Computer Software (TACS), pages 321-346, Sendal, Japan, April 1994. Springer-Verlag. Google ScholarDigital Library
- Rey74.John Reynolds. Towards a theory of type structure. In Proc. Colloque sur la Programmation, pages 408-425, New York, 1974. Springer-Verlag LNCS 19. Google ScholarDigital Library
- RV97.Didier P~my and J6r6me Vouillon. Objective ML: A simple object-oriented extension of ML. In Conference Record of POPL '97: the 24th A CM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 40--53, Paris, Prance, January 15-17, 1997. ACM Press. Full version to appear in Theory and Practice of ObjecA Systems, 1998. Google ScholarDigital Library
- SOW97.Martin Sulzmann, Martin Odersky, and Martin Wehr. Type inference with constrained types. In Fourth International Workshop on Founda- Lions of Object-Oriented Programming (FOOL 4), January 1997. Full version to appear in Theory and Practice of Object S~stems, 1998.Google Scholar
- Ste97.Martin Steffen. PhD thesis, Universit,it Erlangen-Nfirnberg, 1997. Forthcoming Ph.D. thesis.Google Scholar
- TS96.Vaiery "Prifonov and Scott Smith. Subtyping constrained types. In Proce~.dings of the Third International Static Analysis Symposium, volume 1145 of LNGS, pages 349-365. Springer Ver}ag, September 1996. Google ScholarDigital Library
- Wan87.Mitchell Wand. Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic in Computer Science, Ithaca, NY, June 1987.Google Scholar
- Wan88.Mitchell Wand. Corrigendum: Complete type inference for simple objects. In Proceedings of the IEBE Symposium on Logic in Computer Science, 1988.Google Scholar
- Wan94.Mitchell Wand. Type inference for objects with instance variables and inheritance. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming. Types, Semantics, and Language Design, pages 97-120. The MIT Press, 1994. Google ScholarDigital Library
- Wel94.J.B. Wells. Typability and type checking in the second-order A-calculus are equivalent and undecidable. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176-185, 1994.Google ScholarCross Ref
Index Terms
- Local type inference
Recommendations
Local type inference
We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, ...
Colored local type inference
We present a type system for a language based on F≤, which allows certain type annotations to be elided in actual programs. Local type inference determines types by a combination of type propagation and local constraint solving, rather than by global ...
Colored local type inference
POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present a type system for a language based on F≤, which allows certain type annotations to be elided in actual programs. Local type inference determines types by a combination of type propagation and local constraint solving, rather than by global ...
Comments