A practical soft type system for scheme

ABSTRACT

A soft type system infers types for the procedures and data structures of dynamically typed programs. Like conventional static types, soft types express program invariants and thereby provide valuable information for program optimization and debugging. A soft type checker uses the types inferred by a soft type system to eliminate run-time checks that are provably unnecessary; any remaining run-time checks are flagged as potential program errors. Soft Scheme is a practical soft type checker for R4RS Scheme. Its underlying type system generalizes conventional Hindley-Milner type inference by incorporating recursive types and a limited form of union type. Soft Scheme accommodates all of R4RS Scheme including uncurried procedures of fixed and variable arity, assignment, and continuations.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Benjamin Pierce , Gordon Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.237-268, April 1991 [doi>10.1145/103135.103138]
• 2: ABADI, M., CARDELLI, L., PIERCE, B., AND RI~MY, D. 1995. Dynamic typing in polymorphic languages. J. Funct. Program. 5, 1 (Jan.), 111-130.
• 3: Alexander Aiken , Manuel Fähndrich, Dynamic typing and subtype inference, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.182-191, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224201]
• 4: 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]
• 5: 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]
• 6: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.104-118, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99600]
• 7: BARENDREGT, H. P. 1984. The Lambda Calculus: Its Syntax and Semantics, Revised ed. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam.
• 8: BEER, R. D. 1987. Preliminary report on a practical type inference system for Common Lisp. Lisp Pointers 1, 2, 5-11.
• 9: L. Cardelli , J. Donahue , M. Jordan , B. Kalsow , G. Nelson, The Modula–3 type system, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.202-212, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75295]
• 10: 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
• 11: Robert Cartwright , Matthias Felleisen, Extensible Denotational Language Specifications, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.244-272, April 19-22, 1994
• 12: Craig David Chambers, The design and implementation of the self compiler, an optimizing compiler for object-oriented programming languages, Stanford University, Stanford, CA, 1992
• 13: H. Abelson , R. K. Dybvig , C. T. Haynes , G. J. Rozas , N. I. Adams, IV , D. P. Friedman , E. Kohlbecker , G. L. Steele, Jr. , D. H. Bartley , R. Halstead , D. Oxley , G. J. Sussman , G. Brooks , C. Hanson , K. M. Pitman , M. Wand , William Clinger , Jonathan Rees, Revised report on the algorithmic language scheme, ACM SIGPLAN Lisp Pointers, v.IV n.3, p.1-55, July, 1991 [doi>10.1145/382130.382133]
• 14: DAMAS, L. M. M. 1985. Type assignment in programming languages. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.
• 15: Hsianlin Dzeng , Christopher T. Haynes, Type reconstruction for variable-arity procedures, Proceedings of the 1994 ACM conference on LISP and functional programming, p.239-249, June 27-29, 1994, Orlando, Florida, United States
• 16: Mike Fagan, Soft typing: an approach to type checking for dynamically typed languages, Rice University, Houston, TX, 1992
• 17: Marc Feeley , Marcel Turcotte , Guy Lapalme, Using Multilisp for solving constraint satisfaction problems: an application to nucleic acid 3D structure determination, Lisp and Symbolic Computation, v.7 n.2-3, p.231-247, June 1994 [doi>10.1007/BF01018696]
• 18: Matthias Felleisen, On the expressive power of programming languages, Science of Computer Programming, v.17 n.1-3, p.35-75, Dec. 1991
• 19: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 20: FLANAGAN, C. AND FELLEISEN, M. 1995. Set-based analysis for full Scheme and its use in softtyping. Tech. Rep. TR95-253, Rice Univ., Houston, Tex. Oct.
• 21: FREEMAN, T. 1993. Refinement types. Ph.D. thesis, Carnegie Mellon Univ., Pittsburgh, Pa.
• 22: Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
• 23: Carsten K. Gomard, Partial type inference for untyped functional programs, Proceedings of the 1990 ACM conference on LISP and functional programming, p.282-287, June 27-29, 1990, Nice, France [doi>10.1145/91556.91672]
• 24: GREENGARD, L. 1987. The Rapid Evaluation of Potential Fields in Particle Systems. ACM Press, New York.
• 25: John Greiner, Standard ML Weak Polymorphism Can Be Sound, Carnegie Mellon University, Pittsburgh, PA, 1993
• 26: Robert Harper , Mark Lillibridge, Explicit polymorphism and CPS conversion, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-219, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158630]
• 27: Nevin Heintze, Set Based Analysis of ML Programs (Extended Abstract), Carnegie Mellon University, Pittsburgh, PA, 1993
• 28: Fritz Henglein, Dynamic typing, Symposium proceedings on 4th European symposium on programming, p.233-253, January 1992, Rennes, France
• 29: Fritz Henglein, Global tagging optimization by type inference, Proceedings of the 1992 ACM conference on LISP and functional programming, p.205-215, June 22-24, 1992, San Francisco, California, United States
• 30: 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]
• 31: HINDLEY, R. 1969. The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29-60.
• 32: J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
• 33: HOANG, M., MITCHELL, J., AND VISWANATHAN, R. 1993. Standard ML-NJ weak polymorphism and imperative constructs. In Proceedings of the 8th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 15-25.
• 34: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• 35: Suresh Jagannathan , Stephen Weeks, Analyzing stores and references in a parallel symbolic language, Proceedings of the 1994 ACM conference on LISP and functional programming, p.294-305, June 27-29, 1994, Orlando, Florida, United States
• 36: Suresh Jagannathan , Andrew K. Wright, Effective Flow Analysis for Avoiding Run-Time Checks, Proceedings of the Second International Symposium on Static Analysis, p.207-224, September 25-27, 1995
• 37: Stefan Kaes, Type inference in the presence of overloading, subtyping and recursive types, Proceedings of the 1992 ACM conference on LISP and functional programming, p.193-204, June 22-24, 1992, San Francisco, California, United States
• 38: Marc A. Kaplan , Jeffrey D. Ullman, A Scheme for the Automatic Inference of Variable Types, Journal of the ACM (JACM), v.27 n.1, p.128-145, Jan. 1980 [doi>10.1145/322169.322181]
• 39: Andreas Kind , Horst Friedrich, A practical approach to type inference for EuLisp, Lisp and Symbolic Computation, v.6 n.1-2, p.159-176, Aug. 1993 [doi>10.1007/BF01025919]
• 40: LEROY, X. 1992a. Typage polymorphe d'un langage Mgorithmique. Ph.D. thesis, L'Universit6 Paris 7, France.
• 41: Xavier Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.177-188, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143205]
• 42: LEROY, X. AND MAUNY, M. 1993. Dynamics in ML. J. Funct. Program. 3, 4, 431-463.
• 43: Xavier Leroy , Pierre Weis, Polymorphic type inference and assignment, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.291-302, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99622]
• 44: K.-L. Ma , R. R. Kessler, TICL—a type inference system for common Lisp, Software—Practice & Experience, v.20 n.6, p.593-623, June 1990 [doi>10.1002/spe.4380200606]
• 45: Robert A. MacLachlan, The Python compiler for CMU Common Lisp, Proceedings of the 1992 ACM conference on LISP and functional programming, p.235-246, June 22-24, 1992, San Francisco, California, United States
• 46: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 47: MARTELLI, A. AND MONTANARI, W. 1976. Unification in linear time and space: A structured presentation. Tech. Rep. B76-16, Ist. di Elaborazione delle Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy. July.
• 48: MILNER, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348-375.
• 49: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 50: MITCHELL, J. C. 1991. Type inference with simple subtypes. J. Funct. Program. 1, 3 (July), 245-286.
• 51: Patrick M. O'Keefe , Mitchell Wand, Type inference for partial types is decidable, Symposium proceedings on 4th European symposium on programming, p.408-417, January 1992, Rennes, France
• 52: PATERSON, M. S. AND WEGMAN, M. N. 1978. Linear unification. J. Comput. Syst. Sci. 16, 2 (Apr.), 158-167.
• 53: 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]
• 54: RI~MY, D. 1991. Type inference for records in a natural extension of ML. Tech. Rep. 1431, INRIA, France. May.
• 55: RI~MY, D. 1992. Extension of ML type system with a sorted equational theory on types. Tech. Rep. 1766, INRIA, France. Oct.
• 56: Zhong Shao , Andrew W. Appel, Smartest recompilation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.439-450, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158702]
• 57: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 58: Guy L. Steele, Jr., Building interpreters by composing monads, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.472-492, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.178068]
• 59: TALPIN, J.-P. AND JOUVELOT, P. 1992. The type and effect discipline. In Proceedings of the 7th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 162-173.
• 60: Satish Thatte, Type Inference with Partial Types, Proceedings of the 15th International Colloquium on Automata, Languages and Programming, p.615-629, July 11-15, 1988
• 61: Satish Thatte, Quasi-static typing, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-381, December 1989, San Francisco, California, United States [doi>10.1145/96709.96747]
• 62: Mads Tofte, Type inference for polymorphic references, Information and Computation, v.89 n.1, p.1-34, Nov. 1990 [doi>10.1016/0890-5401(90)90018-D]
• 63: WAND, M. 1987. Complete type inference for simple objects. In Proceedings of the 2nd IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 37-44.
• 64: 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]
• 65: Andrew K. Wright, Typing references by effect inference, Symposium proceedings on 4th European symposium on programming, p.473-491, January 1992, Rennes, France
• 66: Andrew Kevin Wright, Practical soft typing, Rice University, Houston, TX, 1996
• 67: Andrew K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, v.8 n.4, p.343-355, Dec. 1995 [doi>10.1007/BF01018828]
• 68: Andrew K. Wright , Robert Cartwright, A practical soft type system for Scheme, Proceedings of the 1994 ACM conference on LISP and functional programming, p.250-262, June 27-29, 1994, Orlando, Florida, United States
• 69: WRIGHT, t. K. AND DUBA, B. F. 1993. Pattern matching for Scheme. Rice Univ., Houston, Tex. Available from http://www.neci.nj.nec.com/homepages/wright.html.
• 70: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 71: ZHAO, F. 1987. An O(N) algorithm for three-dimensionM N-body simulations. M.S. thesis, Dept. of Electrical Engineering and Computer Science, Massachusetts Inst. of Technology, Cambridge, Mass.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
          Nouns: SCHEME
      D.3.4 Processors
          Subjects: Optimization

General Terms:
Performance, Reliability

Keywords:
run-time checks, soft typing