Automatic type inference via partial evaluation

ABSTRACT

Type checking and type inference are fundamentally similar problems. However, the algorithms for performing the two operations, on the same type system, often differ significantly. The type checker is typically a straightforward encoding of the original type rules. For many systems, type inference is performed using a two-phase, constraint-based algorithm.We present an approach that, given the original type rules written as clauses in a logic programming language, automatically generates an efficient, two-phase, constraint-based type inference algorithm. Our approach works by partially evaluating the type checking rules with respect to the target program to yield a set of constraints suitable for input to an external constraint solver. This approach avoids the need to manually develop and verify a separate type inference algorithm, and is ideal for experimentation with and rapid prototyping of novel type systems.

REFERENCES

• 1: Alexander Aiken , Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su, A Toolkit for Constructing Type- and Constraint-Based Program Analyses, Proceedings of the Second International Workshop on Types in Compilation, p.78-96, March 25-27, 1998
• 2: S.-J. Craig and M. Leuschel. LIX: an effective self-applicable partial evaluator for prolog. In Proceedings of the 7th International Symposium on Functional and Logic Programming, FLOPS'04, Apr. 2004.
• 3: R. F. Crew. ASTLOG: A language for examining abstract syntax trees. In Proceedings of the USENIX Conference on Domain-Specific Languages, Oct. 1997.
• 4: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 5: C. Flanagan and S. N. Freund. Type inference against races. In Proceedings of the 2004 Static Analysis Symposium, SAS'04, Aug. 2004.
• 6: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 7: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 8: T. Frühwirth, E. Shapiro, M. Vardi, and E. Yardeni. Logic programs as types for logic programs. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 300--309, 1991.
• 9: T. W. Frühwirth. Type inference by program transformation and partial evaluation. In Proceedings of the Workshop on Meta-Programming in Logic (META'88), pages 263--282, 1988.
• 10: Y. Futamura. Partial evaluation of computation process---an approach to a compiler-compiler. Systems, Computers, Controls, 2(5):45--50, 1971.
• 11: Susan Horwitz , Thomas Reps , Mooly Sagiv, Demand interprocedural dataflow analysis, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.104-115, October 12-15, 1995, Washington, D.C., United States
• 12: B. Joy, G. Steele, J. Gosling, and G. Bracha. The Java™ Language Specification, Second Edition. Addison-Wesley, 2000.
• 13: J. Kodumal. Banshee, a toolkit for building constraint-based analyses. PhD thesis, University of California at Berkeley, 2002.
• 14: Arun Lakhotia , Leon Sterling, ProMiX: a Prolog partial evaluation system, The practice of Prolog, MIT Press, Cambridge, MA, 1990
• 15: M. Leuschel. The ECCE partial deduction system. In Proceedings of the ILPS'97 Workshop on Tools and Environments for (Constraint) Logic Programming, 1997.
• 16: Lunjin Lu , Andy King, Backward Type Inference Generalises Type Checking, Proceedings of the 9th International Symposium on Static Analysis, p.85-101, September 17-20, 2002
• 17: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 18: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 19: C. Schürmann. Towards practical functional programming with logical frameworks, July 2003.
• 20: Jens Peter Secher , Morten Heine Sørensen, From checking to inference via driving and dag grammars, Proceedings of the 2002 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.41-51, January 14-15, 2002, Portland, Oregon
• 21: Dan Sahlin, Mixtus: an automatic partial evaluator for full Prolog, New Generation Computing, v.12 n.1, p.7-51, 1993 [doi>10.1007/BF03038271]
• 22: Z. Somogyi, F. Henderson, and T. Conway. Mercury: an efficient purely declarative logic programming language. In Proceedings of the Australian Computer Science Conference, Feb. 1995.
• 23: G. A. Venkatesh , Charles N. Fischer, SPARE: A Development Environment for Program Analysis Algorithms, IEEE Transactions on Software Engineering, v.18 n.4, p.304-318, April 1992 [doi>10.1109/32.129219]
• 24: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.6 Logic Programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Constraint and logic languages

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

General Terms:
Experimentation, Languages

Keywords:
applications of declarative programming, logic programming, program analysis, type systems