A type-preserving compiler in Haskell

ABSTRACT

There has been a lot of interest of late for programming languages that incorporate features from dependent type systems and proof assistants, in order to capture important invariants of the program in the types. This allows type-based program verification and is a promising compromise between plain old types and full blown Hoare logic proofs. The introduction of GADTs in GHC (and more recently type families) made such dependent typing available in an industry-quality implementation, making it possible to consider its use in large scale programs.

We have undertaken the construction of a complete compiler for System F, whose main property is that the GHC type checker verifies mechanically that each phase of the compiler properly preserves types. Our particular focus is on "types rather than proofs": reasonably few annotations that do not overwhelm the actual code.

We believe it should be possible to write such a type-preserving compiler with an amount of extra code comparable to what is necessary for typical typed intermediate languages, but with the advantage of static checking. We will show in this paper the remaining hurdles to reach this goal.

REFERENCES

• 1: Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a c compiler front-end. In International Symposium on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 460--475, aug 2006.
• 2: Chiyan Chen , Hongwei Xi, Implementing typeful program transformations, Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.20-28, June 07-07, 2003, San Diego, California, USA
• 3: James Cheney and Ralf Hinze. First-class phantom types. Technical Report CUCIS TR2003-1901, Cornell University, 2003.
• 4: Adam Chlipala, A certified type-preserving compiler from lambda calculus to assembly language, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 5: Adam Chlipala, Parametric higher-order abstract syntax for mechanized semantics, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 6: Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2 (4):361--391, 1992.
• 7: Leonidas Fegaras , Tim Sheard, Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space), Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.284-294, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237792]
• 8: Louis-Julien Guillemette , Stefan Monnier, Type-Safe Code Transformations in Haskell, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.7, p.23-39, June, 2007 [doi>10.1016/j.entcs.2006.10.036]
• 9: Louis-Julien Guillemette , Stefan Monnier, A type-preserving closure conversion in haskell, Proceedings of the ACM SIGPLAN workshop on Haskell workshop, September 30-30, 2007, Freiburg, Germany [doi>10.1145/1291201.1291212]
• 10: Louis-Julien Guillemette and Stefan Monnier. One vote for type families in Haskell! In The 9th symposium on Trends in Functional Programming, 2008.
• 11: Nadeem A. Hamid , Zhong Shao , Valery Trifonov , Stefan Monnier , Zhaozhong Ni, A Syntactic Approach to Foundational Proof-Carrying Code, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.89-100, July 22-25, 2002
• 12: Fairouz Kamareddine. Reviewing the classical and the de bruijn notation for λ-calculus and pure type systems. Journal of Logic and Computation, 11, 2001.
• 13: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 14: Nathan Linger and Tim Sheard. Programming with static invariants in Omega. Unpublished, 2004.
• 15: 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]
• 16: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 17: 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]
• 18: Emir Pasalic , Timothy E. Sheard, The role of type equality in meta-programming, OGI School of Science & Engineering, 2004
• 19: Simon Peyton-Jones et al. The Haskell Prime Report. Working Draft, 2007.
• 20: Brigitte Pientka, A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 21: Brigitte Pientka , Joshua Dunfield, Programming with proofs and explicit contexts, Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, July 15-17, 2008, Valencia, Spain [doi>10.1145/1389449.1389469]
• 22: François Pottier , Nadji Gauthier, Polymorphic typed defunctionalization, ACM SIGPLAN Notices, v.39 n.1, p.89-98, January 2004
• 23: Tom Schrijvers, Martin Sulzmann, Simon Peyton Jones, and Manuel M. T. Chakravarty. Towards open type functions for Haskell. Presented at IFL 2007, 2007.
• 24: Zhong Shao. An overview of the FLINT/ML compiler. In International Workshop on Types in Compilation, June 1997.
• 25: 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
• 26: Zhong Shao , Bratin Saha , Valery Trifonov , Nikolaos Papaspyrou, A type system for certified binaries, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.217-232, January 16-18, 2002, Portland, Oregon
• 27: Tim Sheard , Simon Peyton Jones, Template meta-programming for Haskell, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.1-16, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581691]
• 28: Martin Sulzmann , Manuel M. T. Chakravarty , Simon Peyton Jones , Kevin Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190324]
• 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: Geoffrey Washburn , Stephanie Weirich, Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.249-262, August 25-29, 2003, Uppsala, Sweden
• 31: Hongwei Xi , Chiyan Chen , Gang Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-235, January 15-17, 2003, New Orleans, Louisiana, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
compilation, de Bruijn, higher-order abstract syntax, typed assembly language