Colored local type inference

ABSTRACT

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 constraint solving. We re ne the previously existing local type inference system of Pierce and Turner[PT98] by allowing partial type information to be propagated. This is expressed by coloring types to indicate propagation directions. Propagating partial type information allows us to omit type annotations for the visitor pattern, the analogue of pattern matching in languages without sum types.

REFERENCES

• ACF+: Andrew Appel, Luca Cardelli, Kathleen Fisher, Carl Gunter, Robert Harper, Xavier Leroy, Mark Lillibridge, David B. MacQueen, John Mitchell, Greg Morrisett, John H. Reppy, Jon G. Riecke, Zhong Shao, and Christopher A. Stone. Principles and preliminary design for ML 2000.
• AW93: Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165188]
• BOSW98: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• Car93: Luca Cardelli. An implementation of F< Technical Report 97, DEC Systems Research Center, February 1993.
• CDG+92: Luca Cardelli , James Donahue , Lucille Glassman , Mick Jordan , Bill Kalsow , Greg Nelson, Modula-3 language definition, ACM SIGPLAN Notices, v.27 n.8, p.15-42, Aug. 1992 [doi>10.1145/142137.142141]
• CT98: Craig Chambers and Cecil Team. The Cecil language, specification and rationale, December 1998.
• EST95: Jonathan Eifrig, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and its application to OOP. In Proc. MFPS '95, Eleventh Conference on the Mathematical Foundations of Programming Semantics, March 1995.
• FG96: Cédric Fournet , Georges Gonthier, The reflexive CHAM and the join-calculus, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.372-385, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237805]
• GHJV94: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• GR99: Jacques Garrigue , Didier Rémy, Semi-explicit first-class polymorphism for ML, Information and Computation, v.155 n.1-2, p.134-169, Nov./Dec. 1999 [doi>10.1006/inco.1999.2830]
• Jon97: Mark P. Jones, First-class polymorphism with type inference, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.483-496, January 15-17, 1997, Paris, France [doi>10.1145/263699.263765]
• Knu68: Donald E. Knuth. Semantics of context-free languages. Mathematical Systems Theory, 2(2):127-145, February 1968.
• Lit98: Vassily Litvinov, Contraint-based polymorphism in Cecil: towards a practical and static type system, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.388-411, October 18-22, 1998, Vancouver, British Columbia, Canada
• Mey92: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• NC97: Johan Nordlander and Magnus Carlsson. Reactive objects in a functional language - an escape from the evil I. In Proceedings of the Haskell Workshop, June 1997.
• Nor98: Johan Nordlander, Pragmatic subtyping in polymorphic languages, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.216-227, September 26-29, 1998, Baltimore, Maryland, United States
• Ode00: Martin Odersky, Functional Nets, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.1-25, April 02, 2000
• OL96: Martin Odersky , Konstantin Läufer, Putting type annotations to work, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-67, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237729]
• OSW99: Martin Odersky , Martin Sulzmann , Martin Wehr, Type inference with constrained types, Theory and Practice of Object Systems, v.5 n.1, p.35-55, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4]
• OW97: Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
• OZZ00: Martin Odersky, Christoph Zenger, and Matthias Zenger. Colored local type inference. http://lampwww.epfl.ch/papers/clti-color.ps.gz, 2000.
• Pfe88: Frank Pfenning, Partial polymorphic type inference and higher-order unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.153-163, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62697]
• Pot96: François Pottier, Simplifying subtyping constraints, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.122-133, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• Pot98: François Pottier, A framework for type inference with subtyping, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.228-238, September 26-29, 1998, Baltimore, Maryland, United States
• PT98: Benjamin C. Pierce , David N. Turner, Local type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.252-265, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268967]
• Rém89: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• Str91: Bjarne Stroustrup, The C++ programming language (2nd ed.), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1991
• TS96: Valery Trifonov , Scott F. Smith, Subtyping Constrained Types, Proceedings of the Third International Symposium on Static Analysis, p.349-365, September 24-26, 1996
• Wad89: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]
• Wel94: J.B. Wells. Typability and type checking in the second order -calculus are equivalent and undecidable. In Proc. 9th IEEE Symposium on Logic in Computer Science, pages 176-185, July 1994.
• WJ00: Keith Wansbrough and Simon Peyton Jones. Simple usage polymorphism. In Proceedings of the Third ACM SIGPLAN Workshop on Types in Compilation, September 2000.
• XP99: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

General Terms:
Design, Languages, Performance, Theory