Concoqtion: indexed types now!

ABSTRACT

Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate Fω-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.

REFERENCES

• 1: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 2: Edwin Brady, Conor McBride, and James McKinna. Inductive families need not store their indices. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of Lecture Notes in Computer Science, pages 115--129. Springer, 2003.
• 3: Luca Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Reports, pages 431--507. Springer-Verlag, New York, 1991.
• 4: 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
• 5: Chiyan Chen , Hongwei Xi, Combining programming with theorem proving, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 6: James Cheney and Ralf Hinze. First-class phantom types. Technical Report 1901, Cornell University, 2003.
• 7: The MetaOCaml Concoqtion web site. Online at http://www.metaocaml.org/concoqtion, July 2006.
• 8: The Coq. The coq proof assistant: Reference manual: Version 7.2, February 2002.
• 9: Thierry Coquand , Gérard P. Huet, Constructions: A Higher Order Proof System for Mechanizing Mathematics, Invited Lectures from the European Conference on Computer Algebra-Volume I, p.151-184, April 01-03, 1985
• 10: Krzysztof Czarneckil, John O'Donnell, Jörg Striegnitz, and Walid Taha. DSL implementation in metaocaml, template haskell, and C++. In Batory, Consel, Lengauer, and Odersky, editors, Dagstuhl Workshop on Domain-specific Program Generation, LNCS. 2004.
• 11: Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur. Thèse de doctorat d'etat, University of Paris VII, 1972.
• 12: P. Hudak, Modular Domain Specific Languages and Tools, Proceedings of the 5th International Conference on Software Reuse, p.134, June 02-05, 1998
• 13: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 14: N. D. Jones, P. Sestoft, and H. Sondergaard. Mix: a self-applicable partial evaluator for experiments in compiler generation. Technical Report DIKU Report 87/08, University of Copenhagen, Denmark, 1987.
• 15: Andrew Kennedy , Claudio V. Russo, Generalized algebraic data types and object-oriented programming, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 16: Xavier Leroy. Objective Caml, 2000. Available from http://caml.inria.fr/ocaml/.
• 17: 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
• 18: MetaOCaml: A compiled, type-safe multi-stage programming language. Available online from http://www.metaocaml.org/, 2004.
• 19: Emir Pasalic, Jeremy Siek, and Walid Taha. Concoqtion: Mixing dependent types and Hindley-Milner type inference (extended version). Technical report, Rice University, 2006. Available from http://www.metaocaml.org/concoqtion.
• 20: Emir PašaliΕ , Walid Taha , Tim Sheard, Tagless staged interpreters for typed languages, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.218-229, October 04-06, 2002, Pittsburgh, PA, USA
• 21: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 22: Zhong Shao , Bratin Saha , Valery Trifonov , Nikolaos Papaspyrou, A type system for certified binaries, ACM SIGPLAN Notices, v.37 n.1, p.217-232, Jan. 2002
• 23: Tim Sheard, Languages of the future, ACM SIGPLAN Notices, v.39 n.12, December 2004 [doi>10.1145/1052883.1052897]
• 24: Tim Sheard and Emir Pasalic. Meta-programming with built-in type equality. In Fourth International Workshop on Logical Frameworks and Meta-Languages (LFM'04), Cork, Ireland, July 2004.
• 25: Vincent Simonet , François Pottier, A constraint-based approach to guarded algebraic data types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.1, p.1-es, January 2007 [doi>10.1145/1180475.1180476]
• 26: Walid Taha. A gentle introduction to multi-stage programming. In Don Batory, Charles Consel, Christian Lengauer, and Martin Odersky, editors, Domain-specific Program Generation, LNCS. 2004.
• 27: Walid Taha , Henning Makholm , John Hughes, Tag Elimination and Jones-Optimality, Proceedings of the Second Symposium on Programs as Data Objects, p.257-275, May 21-23, 2001
• 28: Walid Taha , Michael Florentin Nielsen, Environment classifiers, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-37, January 15-17, 2003, New Orleans, Louisiana, USA
• 29: Walid Taha , Tim Sheard, Multi-stage programming with explicit annotations, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.203-217, June 12-13, 1997, Amsterdam, The Netherlands
• 30: 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
• 31: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada
• 32: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Design, Languages