Flexible type analysis

ABSTRACT

Run-time type dispatch enables a variety of advanced optimization techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, and flattened data structures. However, modern type-preserving compilers transform types between stages of compilation, making type dispatch prohibitively complex at low levels of typed compilation. It is crucial therefore for type analysis at these low levels to refer to the types of previous stages. Unfortunately, no current intermediate language supports this facility.To fill this gap, we present the language LX, which provides a rich language of type constructors supporting type analysis (possibly of previous-stage types) as a programming idiom. This language is quite flexible, supporting a variety of other applications such as analysis of quantified types, analysis with incomplete type information, and type classes. We also show that LX is compatible with a type-erasure semantics.

REFERENCES

• 1: Shail Aditya , Christine H. Flood , James E. Hicks, Garbage collection for strongly-typed languages using run-time type reconstruction, Proceedings of the 1994 ACM conference on LISP and functional programming, p.12-23, June 27-29, 1994, Orlando, Florida, United States
• 2: Lars Birkedal , Mads Tofte , Magnus Vejlstrup, From region inference to von Neumann machines via region representation inference, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237771]
• 3: Perry Cheng , Robert Harper , Peter Lee, Generational stack collection and profile-driven pretenuring, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.162-173, June 17-19, 1998, Montreal, Quebec, Canada
• 4: Karl Crary and Stephanie Weirich. Flexible type analysis (extended version). Technical report, Cornell University, 1999.
• 5: Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.301-312, September 26-29, 1998, Baltimore, Maryland, United States
• 6: Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional Polymorphism in Type-Erasure Semantics, Cornell University, Ithaca, NY, 1998
• 7: Joëlle Despeyroux , Frank Pfenning , Carsten Schürmann, Primitive Recursion for Higher-Order Abstract Syntax, Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, p.147-163, April 02-04, 1997
• 8: Dominic Duggan, A Type-Based Semantics for User-Defined Marshalling in Polymorphic Languages, Proceedings of the Second International Workshop on Types in Compilation, p.273-297, March 25-27, 1998
• 9: Jean-Yves Girard. Une extension de l'interpr6tation de GSdel ~ l'aaalyse, et son application ~ l'61imiaation de coupures dans l'analyse etla th~orie des types. In J. E. Fenstad, editor, Proceedi~~s of the Second Scandinavian Logic Symposium, pages 63-92. North-Holland Publishing Co., 1971.
• 10: Jean-Yves Girard. Interprdtation fonctionelle et dlimination des coupures de l'arithmdtique d'ordre supdrieur. PhD thesis, Universit~ Paris VII, 1972.
• 11: Andrew D. Gordon, Functional programming and input/output, Cambridge University Press, New York, NY, 1994
• 12: 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]
• 13: Brian T. Howard, Fixed points and extensionality in typed functional programming languages, Stanford University, Stanford, CA, 1992
• 14: Brian T. Howard, Inductive, coinductive, and pointed types, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.102-109, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 15: 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]
• 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: Nax Paul Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1-2):159-172, 1991. Earlier version in LICS '88. (pp. 15,19,134,135).
• 18: Paul Francis Mendler. Inductive Definition in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, September 1987.
• 19: Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
• 20: G. Morrisett, D. Taxditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through type~. In Workshop on Compiler Support for Systems Software, Tucson, February 1996.
• 21: Greg Morrisett. Compiling with Types. PhD thesis~ Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania, December 1995.
• 22: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Fred Smith, Dave Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. Technical report, Cornell University, 1999. Submitted to the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software.
• 23: G. Morrisett , R. Harper, Semantics of memory management for polymorphic languages, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 24: 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]
• 25: Erik Ruf, Partitioning dataflow analyses using types, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-26, January 15-17, 1997, Paris, France [doi>10.1145/263699.263705]
• 26: 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
• 27: Zhong Shao. An overview of the FLINT/ML compiler. In 1997 Workshop on Types in Compilation, Amsterdam, June 1997. Published as Boston College Computer Science Department Technical Report BCCS-97-03.
• 28: Zhong Shao , Christopher League , Stefan Monnier, Implementing typed intermediate languages, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.313-323, September 26-29, 1998, Baltimore, Maryland, United States
• 29: 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
• 30: 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
• 31: Benjamin Werner. Une Thdorie des Constructiones lnductives. PhD thesis, Universit~ Paris VII, 1994.

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

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES

General Terms:
Languages, Theory