Implementing typed intermediate languages

ABSTRACT

Recent advances in compiler technology have demonstrated the benefits of using strongly typed intermediate languages to compile richly typed source languages (e.g., ML). A type-preserving compiler can use types to guide advanced optimizations and to help generate provably secure mobile code. Types, unfortunately, are very hard to represent and manipulate efficiently; a naive implementation can easily add exponential overhead to the compilation and execution of a program. This paper describes our experience with implementing the FLINT typed intermediate language in the SML/NJ production compiler. We observe that a type-preserving compiler will not scale to handle large types unless all of its type-preserving stages preserve the asymptotic time and space usage in representing and manipulating types. We present a series of novel techniques for achieving this property and give empirical evidence of their effectiveness.

REFERENCES

• 1: M. Abadi , P. L. Curien , J. J. Levy, Explicit substitutions, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.31-46, December 1989, San Francisco, California, United States [doi>10.1145/96709.96712]
• 2: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 3: A. W. Appel and D. B. MacQueen. Standard ML of New Jersey. In M. Wirsing, editor, Third lnt'l Syrup. on Prog. Lang. Implementation and Logic Programming, pages 1-13, New York, August 1991. Springer-Verlag.
• 4: M. Blume. A compilation manager for SML/NJ. as part of SML/NJ User's Guide, 1995.
• 5: 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]
• 6: Olivier Danvy, Type-directed partial evaluation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.242-257, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237784]
• 7: N. de Bruijn. A survey of the project AUTOMATH. In To H. B. Curry: Essays on Combinator~l Logic, Larnbda Calculus and Formalism, pages 579-606. Edited by J. P. Seldin and J. R. Hindley, Academic Press, 1980.
• 8: Allyn Dimock , Robert Muller , Franklyn Turbak , J. B. Wells, Strongly typed flow-directed representation transformations (extended abstract), Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.11-24, June 09-11, 1997, Amsterdam, The Netherlands
• 9: John Field, On laziness and optimality in lambda interpreters: tools for specification and analysis, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-15, December 1989, San Francisco, California, United States [doi>10.1145/96709.96710]
• 10: Cormac Flanagan , Amr Sabry , Bruce F. Duba , Matthias Felleisen, The essence of compiling with continuations, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.237-247, June 21-25, 1993, Albuquerque, New Mexico, United States
• 11: Lal George , Florent Guillame , John H. Reppy, A Portable and Optimizing Back End for the SML/NJ Compiler, Proceedings of the 5th International Conference on Compiler Construction, p.83-97, April 07-09, 1994
• 12: J. Y. Girard. Interpretation Fonctionnelle et Elimination des Coupures dans l'Arithmetique d'Ordre Superieur. PhD thesis, University of Paris Vii, 1972.
• 13: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 14: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 15: Gérard Huet, Logical foundations of functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 16: 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]
• 17: Xavier Leroy , François Rouaix, Security properties of typed applets, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.391-403, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268979]
• 18: J.-J. Levy. Optimal reductions in the lambda calculus. In To H. B. Curtal: Essays on Uornbinator~t Logic, Lambda Calculus and Formalism. Edited by J. P. Seldin and J. R. Hindley, Academic Press, 1980.
• 19: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 20: Harry G. Mairson, Deciding ML typability is complete for deterministic exponential time, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.382-401, December 1989, San Francisco, California, United States [doi>10.1145/96709.96748]
• 21: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 22: G. Morrisett. Compiling with Types. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, December 1995. Tech Report CMU-CS-95-226.
• 23: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 24: Gopalan Nadathur , Sue D Wilson, A Notation for Lambda Terms II: Refinements and Applications, Duke University, Durham, NC, 1994
• 25: Gopalan Nadathur , Debra Sue Wilson, A representation of Lambda terms suitable for operations on their intensions, Proceedings of the 1990 ACM conference on LISP and functional programming, p.341-348, June 27-29, 1990, Nice, France [doi>10.1145/91556.91682]
• 26: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 27: S. Peyton Jones. Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine. Journal of Functional Programming, 2(2):127-202, April 1992.
• 28: Simon L. Peyton Jones , John Launchbury, Unboxed values as first class citizens in a non-strict functional language, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.636-666, June 1991, Cambridge, Massachusetts, United States
• 29: Simon Peyton Jones , Mark Shields , John Launchbury , Andrew Tolmach, Bridging the gulf: a common intermediate language for ML and Haskell, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268951]
• 30: S. Peyton Jones and E. Meijer. Henk: a typed intermediate language. In Proc. 1997 A CM SIGPLAN Workshop on Types in Compilation, June 1997.
• 31: J. H. Reppy and E. R. Gansner. The eXene library manual. Cornell Univ. Dept. of Computer Science, March 1991.
• 32: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 33: Bratin Saha , Zhong Shao, Optimal Type Lifting, Proceedings of the Second International Workshop on Types in Compilation, p.156-177, March 25-27, 1998
• 34: Zhong Shao, Flexible representation analysis, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.85-98, June 09-11, 1997, Amsterdam, The Netherlands
• 35: Z. Shao. An overview of the FLiNT/ML compiler. In Proc. 1997 A CM SIGPLAN Workshop on Types in Compilation, June 1997.
• 36: Z. Shao. Typed common intermediate format. In Proc. 1997 USENIX Conference on Domain Specific Languages, pages 89-102, October 1997.
• 37: Zhong Shao, Typed cross-module compilation, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.141-152, September 26-29, 1998, Baltimore, Maryland, United States
• 38: Zhong Shao , Andrew W. Appel, Space-efficient closure representations, Proceedings of the 1994 ACM conference on LISP and functional programming, p.150-161, June 27-29, 1994, Orlando, Florida, United States
• 39: Zhong Shao , Andrew W. Appel, A type-based compiler for standard ML, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.116-129, June 18-21, 1995, La Jolla, California, United States
• 40: D. Tarditi. Design and Implementation of Code Optimizations for a 7~ype-Directed Compiler for Standard ML. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, December 1996. Tech Report CMU- CS-97-108.
• 41: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 42: M. Torte. Region-based memory management (invited talk). In Proc. 1998 International Workshop on Types in Compilation, March 1998.
• 43: Andrew Tolmach, Tag-free garbage collection using explicit type parameters, Proceedings of the 1994 ACM conference on LISP and functional programming, p.1-11, June 27-29, 1994, Orlando, Florida, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

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

General Terms:
Design, Experimentation, Languages, Measurement, Performance, Theory