Discriminative sum types locate the source of type errors

ABSTRACT

We propose a type system for locating the source of type errors in an applied lambda calculus with ML-style polymorphism. The system is based on discriminative sum types---known from work on soft typing---with annotation subtyping and recursive types. This way, type clashes can be registered in the type for later reporting. The annotations track the potential producers and consumers for each value so that clashes can be traced to their cause.Every term is typeable in our system and type inference is decidable. A type derivation in our system describes all type errors present in the program, so that a principal derivation yields a principal description of all type errors present. Error messages are derived from completed type derivations. Thus, error messages are independent of the particular algorithm used for type inference, provided it constructs such a derivation.

REFERENCES

• 1: Martín Abadi , Butler Lampson , Jean-Jacques Lévy, Analysis and caching of dependencies, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.83-91, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 2: ACM. Proc. of the 13th Annual ACM Symposium on Principles of Programming Languages, St. Petersburg, Florida, 1986.
• 3: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 4: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
• 5: H. P. Barendregt. The Lambda Calculus --- Its Syntax and Semantics. North-Holland, 1984.
• 6: Mike Beaven , Ryan Stansifer, Explaining type errors in polymorphic languages, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.17-30, March–Dec. 1993 [doi>10.1145/176454.176460]
• 7: Robert Cartwright , Mike Fagan, Soft typing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.278-292, June 24-28, 1991, Toronto, Ontario, Canada
• 8: Olaf Chitil, Compositional explanation of types and algorithmic debugging of type errors, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 9: Dominique Clément , Thierry Despeyroux , Gilles Kahn , Joëlle Despeyroux, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming, p.13-27, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319847]
• 10: Luis Damas. Type Assignment in Programming Languages. PhD thesis, Computer Science Department, Edinburgh University, 1985. report CST-33-85.
• 11: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 12: Dominic Duggan , Frederick Bent, Explaining type inference, Science of Computer Programming, v.27 n.1, p.37-83, July 1996 [doi>10.1016/0167-6423(95)00007-0]
• 13: Cormac Flanagan , Matthias Felleisen, Componential set-based analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.2, p.370-416, March 1999 [doi>10.1145/316686.316703]
• 14: Christian Haack and Joe Wells. Type error slicing in implicitly typed, higher-order languages. In Proc. 12th European Symposium on Programming, Lecture Notes in Computer Science, Warsaw, Poland, April 2003. Springer-Verlag.
• 15: Bastiaan Heeren, Johan Jeuring, Doaitse Swierstra, and Pablo Azero Alcocer. Improving type-error messages in functional languages. Technical Report UU-CS-2002-009, Institute of Information and Computing Science, University Utrecht, Netherlands, February 2002. Technical Report.
• 16: Nevin Heintze, Control-Flow Analysis and Type Systems, Proceedings of the Second International Symposium on Static Analysis, p.189-206, September 25-27, 1995
• 17: Fritz Henglein, Dynamic typing: syntax and proof theory, Science of Computer Programming, v.22 n.3, p.197-230, June 1994
• 18: Fritz Henglein , Jakob Rehof, Safe polymorphic type inference for a dynamically typed language: translating Scheme to ML, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.192-203, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224203]
• 19: Mark P. Jones, Qualified types: theory and practice, Cambridge University Press, New York, NY, 1995
• 20: Oukseh Lee , Kwangkeun Yi, Proofs about a folklore let-polymorphic type inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.707-723, July 1998 [doi>10.1145/291891.291892]
• 21: Bruce J. McAdam, On the Unification of Substitutions in Type Interfaces, Selected Papers from the 10th International Workshop on 10th International Workshop, p.137-152, September 09-11, 1998
• 22: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348--375, 1978.
• 23: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
• 24: John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 13):245--286, July 1991.
• 25: 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]
• 26: Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-378, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199533]
• 27: Jens Palsberg , Christina Pavlopoulou, From polyvariant flow information to intersection and union types, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.197-208, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268963]
• 28: François Pottier, A versatile constraint-based type inference system, Nordic Journal of Computing, v.7 n.4, p.312-347, Winter 2000
• 29: 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]
• 30: Didier Rémy, Projective ML, Proceedings of the 1992 ACM conference on LISP and functional programming, p.66-75, June 22-24, 1992, San Francisco, California, United States
• 31: Didier Rémy, Type inference for records in natural extension of ML, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 32: Christian Skalka and Scott Smith. Set types and applications. Electronic Notes in Theoretical Computer Science, 75, 2003.
• 33: Gregory F. Johnson , Janet A. Walz, A maximum-flow approach to anomaly isolation in unification-based incremental type inference, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.44-57, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512649]
• 34: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 35: M. Wand, Type inference for record concatenatiOn and multiple inheritance, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.92-97, June 1989, Pacific Grove, California, United States
• 36: Mitchell Wand, Type inference for record concatenation and multiple inheritance, Information and Computation, v.93 n.1, p.1-15, July 1991 [doi>10.1016/0890-5401(91)90050-C]
• 37: J. B. Wells, The Essence of Principal Typings, Proceedings of the 29th International Colloquium on Automata, Languages and Programming, p.913-925, July 08-13, 2002
• 38: Andrew K. Wright , Robert Cartwright, A practical soft type system for scheme, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.87-152, Jan. 1997 [doi>10.1145/239912.239917]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

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

General Terms:
Languages, Theory

Keywords:
polymorphism, type errors, type inference