Gradual typing with unification-based inference

ABSTRACT

Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence or absence of type annotations. This paper studies the combination of gradual typing and unification-based type inference with the goal of developing a system that helps programmers increase the amount of static checking in their program. The key question in combining gradual typing and type inference is how should the dynamic type of a gradual system interact with the type variables of a type inference system. This paper explores the design space and shows why three straightforward approaches fail to meet our design goals. This paper presents a new type system based on the idea that a solution for a type variable should be as informative as any type that constrains the variable. The paper also develops an efficient inference algorithm and proves it sound and complete with respect to the type system.

REFERENCES

• 1: M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237--268, April 1991.
• 2: C. Anderson and S. Drossopoulou. BabyJ - from object based to class based programming via types. In WOOD '03, volume 82, pages 53--81. Elsevier, 2003.
• 3: G. Bracha. Pluggable type systems. In OOPSLA'04 Workshop on Revival of Dynamic Languages, 2004.
• 4: G. Bracha and D. Griswold. Strongtalk: typechecking smalltalk in a production environment. In OOPSLA '93: Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications, pages 215--230, New York, NY, USA, 1993. ACM Press.
• 5: Y. Bres, B. P. Serpette, and M. Serrano. Compiling scheme programs to .NET common intermediate language. In 2nd International Workshop on .NET Technologies, Pilzen, Czech Republic, May 2004.
• 6: R. Cartwright and M. Fagan. Soft typing. In PLDI '91: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, pages 278--292, New York, NY, USA, 1991. ACM Press.
• 7: C. Chambers and the Cecil Group. The Cecil language: Specification and rationale. Technical report, Department of Computer Science and Engineering, University of Washington, Seattle, Washington, 2004.
• 8: L. Damas and R. Milner. Principal type-schemes for functional programs. In POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 207--212, New York, NY, USA, 1982. ACM Press.
• 9: R. B. de Oliveira. The Boo programming language. http://boo.codehaus.org, 2005.
• 10: J. Eifrig, S. Smith, and V. Trifonov. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics, 1995.
• 11: N. Feinberg, S. E. Keene, R. O. Mathews, and P. T. Withington. Dylan programming: an object-oriented and dynamic language. Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, USA, 1997.
• 12: C. Flanagan. Hybrid type checking. In POPL 2006: The 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 245--256, Charleston, South Carolina, January 2006.
• 13: C. Flanagan and M. Felleisen. Componential set-based analysis. In PLDI '97: Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, pages 235--248, New York, NY, USA, 1997. ACM Press.
• 14: C. Flanagan and M. Felleisen. Componential set-based analysis. ACM Trans. Program. Lang. Syst., 21(2):370--416, 1999.
• 15: C. Flanagan, S. N. Freund, and A. Tomb. Hybrid types, invariants, and refinements for imperative objects. In FOOL/WOOD '06: International Workshop on Foundations and Developments of Object-Oriented Languages, 2006.
• 16: D. P. Friedman, C. T. Haynes, and M. Wand. Essentials of programming languages (3rd ed.). MIT Press, Cambridge, MA, USA, 2008.
• 17: K. E. Gray, R. B. Findler, and M. Flatt. Fine-grained interoperability through mirrors and contracts. In OOPSLA '05: Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming systems languages and applications, pages 231--245, New York, NY, USA, 2005. ACM Press.
• 18: J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In R. Findler, editor, Scheme and Functional Programming Workshop, pages 93--104, 2006.
• 19: J. J. Heiss. Meet Peter von der Ahé, tech lead for Javac at Sun Microsystems. Sun Developer Network (SDN), April 2007.
• 20: D. Herman and C. Flanagan. Status report: specifying JavaScript with ML. In ML '07: Proceedings of the 2007 workshop on Workshop on ML, pages 47--52, New York, NY, USA, 2007. ACM.
• 21: D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. In Trends in Functional Prog. (TFP), page XXVIII, April 2007.
• 22: R. Hindley. The principal type-scheme of an object in combinatory logic. Trans AMS, 146:29--60, 1969.
• 23: G. Huet. Resolution d'equations dans les langages d'ordre 1, 2, …, omega. PhD thesis, Université Paris VII, France, 1976.
• 24: G. L. S. Jr. An overview of COMMON LISP. In LFP '82: Proceedings of the 1982 ACM symposium on LISP and functional programming, pages 98--107, New York, NY, USA, 1982. ACM Press.
• 25: R. Kelsey, W. Clinger, and J. R. (eds.). Revised⁵ report on the algorithmic language scheme. Higher-Order and Symbolic Computation, 11(1), August 1998.
• 26: K. Knight. Unification: a multidisciplinary survey. ACM Comput. Surv., 21(1):93--124, 1989.
• 27: X. Leroy. The Objective Caml system: Documentation and user's manual, 2000. With Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon.
• 28: J. Matthews and R. B. Findler. Operational semantics for multi-language programs. In The 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2007.
• 29: E. Meijer and P. Drayton. Static typing where possible, dynamic typing when needed: The end of the cold war between programming languages. In OOPSLA'04 Workshop on Revival of Dynamic Languages, 2004.
• 30: R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348--375, 1978.
• 31: R. Milner, M. Tofte, and R. Harper. The definition of Standard ML. MIT Press, Cambridge, MA, USA, 1990.
• 32: W. Naraschewski and T. Nipkow. Type inference verified: Algorithm W in Isabelle/HOL. J. Autom. Reason., 23(3):299--318, 1999.
• 33: A. Oliart. An algorithm for inferring quasi-static types. Technical Report 1994-013, Boston University, 1994.
• 34: X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types (extended abstract). In 3rd IFIP International Conference on Theoretical Computer Science, August 2004.
• 35: M. S. Paterson and M. N. Wegman. Linear unification. In STOC '76: Proceedings of the eighth annual ACM symposium on Theory of computing, pages 181--186, New York, NY, USA, 1976. ACM Press.
• 36: S. Peyton Jones. Haskell 98 Language and Libraries: The Revised Report, December 2002.
• 37: B. C. Pierce. Types and Programming Languages. MIT Press, Cambridge, MA, USA, 2002.
• 38: B. C. Pierce and D. N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1):1--44, 2000.
• 39: F. Pottier. A framework for type inference with subtyping. In ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pages 228--238, New York, NY, USA, 1998. ACM Press.
• 40: F. Pottier. Simplifying subtyping constraints: a theory. Inf. Comput., 170(2):153--183, 2001.
• 41: J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513--523, Amsterdam, 1983. Elsevier Science Publishers B. V. (North-Holland).
• 42: J. Riely and M. Hennessy. Trust and partial typing in open systems of mobile agents. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 93--104, New York, NY, USA, 1999. ACM Press.
• 43: J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23--41, 1965.
• 44: M. Serrano. Bigloo: a practical Scheme compiler. Inria-Rocquencourt, April 2002.
• 45: A. Shalit. The Dylan reference manual: the definitive guide to the new object-oriented dynamic language. Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, USA, 1996.
• 46: J. Siek and M. Vachharajani. Gradual typing with unification-based inference. Technical Report CU-CS-1039-08, University of Colorado at Boulder, January 2008.
• 47: J. G. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, pages 81--92, September 2006.
• 48: J. G. Siek and W. Taha. Gradual typing for objects. In ECOOP 2007, volume 4609 of LCNS, pages 2--27. Springer Verlag, August 2007.
• 49: R. E. Tarjan. Efficiency of a good but not linear set union algorithm. J. ACM, 22(2):215--225, 1975.
• 50: S. Thatte. Quasi-static typing. In POPL 1990, pages 367--381, New York, NY, USA, 1990. ACM Press.
• 51: S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: From scripts to programs. In OOPSLA'06 Companion, pages 964--974, NY, 2006. ACM.
• 52: S. Tobin-Hochstadt and M. Felleisen. The design and implementation of typed scheme. In POPL 2008: The 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2008.
• 53: G. van Rossum. Python Reference Manual. Python Software Foundation, http://docs.python.org/ref/ref.html, 2.5 edition, September 2006.
• 54: P. Wadler. Theorems for free! In FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture, pages 347--359, New York, NY, USA, 1989. ACM.
• 55: P. Wadler and R. B. Findler. Well-typed programs can't be blamed. In D. Dube, editor, Workshop on Scheme and Functional Programming, pages 15--26, 2007.
• 56: B. Wagner. Local type inference, anonymous types, and var. Microsoft Developer Network, 2007.
• 57: M. Wand. A simple algorithm and proof for type inference. Fundamenta Informatica, 10:115--122, 1987.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Languages

Keywords:
dynamic typing, gradual typing, simply typed lambda calculus, static typing, type inference, unification