The power of Pi

ABSTRACT

This paper exhibits the power of programming with dependent types by dint of embedding three domain-specific languages: Cryptol, a language for cryptographic protocols; a small data description language; and relational algebra. Each example demonstrates particular design patterns inherent to dependently-typed programming. Documenting these techniques paves the way for further research in domain-specific embedded type systems.

REFERENCES

• 1: Lennart Augustsson and Magnus Carlsson. An exercise in dependent types: a well-typed interpreter. Unpublished manuscript.
• 2: Godmar Back, DataScript - A Specification and Scripting Language for Binary Data, Proceedings of the 1st ACM SIGPLAN/SIGSOFT conference on Generative Programming and Component Engineering, p.66-77, October 06-08, 2002
• 3: Per Bjesse , Koen Claessen , Mary Sheeran , Satnam Singh, Lava: hardware design in Haskell, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.174-184, September 26-29, 1998, Baltimore, Maryland, United States
• 4: Björn Bringert , Anders Höckersten , Conny Andersson , Martin Andersson , Mary Bergman , Victor Blomqvist , Torbjörn Martin, Student paper: HaskellDB improved, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, p.108-115, September 22-22, 2004, Snowbird, Utah, USA [doi>10.1145/1017472.1017473]
• 5: Koen Claessen , John Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.268-279, September 2000
• 6: Conal Elliott , Paul Hudak, Functional reactive animation, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.263-273, June 09-11, 1997, Amsterdam, The Netherlands
• 7: Kathleen Fisher , Robert Gruber, PADS: a domain-specific language for processing ad hoc data, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 8: Kathleen Fisher , Yitzhak Mandelbaum , David Walker, The next 700 data description languages, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.2-15, January 11-13, 2006, Charleston, South Carolina, USA
• 9: Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
• 10: Galois, Inc. Cryptol Reference Manual, 2002.
• 11: Ralf Hinze and Johan Jeuring. Generic Haskell: Practice and theory. In Generic Programming, volume 2793 of Lecture Notes in Computer Science. Springer-Verlag, 2003.
• 12: Graham Hutton , Erik Meijer, Monadic parsing in Haskell, Journal of Functional Programming, v.8 n.4, p.437-444, July 1998 [doi>10.1017/S0956796898003050]
• 13: Oleg Kiselyov , Ralf Lämmel , Keean Schupke, Strongly typed heterogeneous collections, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, September 22-22, 2004, Snowbird, Utah, USA [doi>10.1145/1017472.1017488]
• 14: Daan Leijen , Erik Meijer, Domain specific embedded compilers, Proceedings of the 2nd conference on Domain-specific languages, p.109-122, October 03-06, 1999, Austin, Texas, United States
• 15: Daan Leijen and Erik Meijer. Parsec: Direct style monadic parser combinators for the real world. Technical Report UU-CS-2001-27, Universiteit Utrecht, 2001.
• 16: Conor McBride. Epigram: Practical programming with dependent types. In Advanced Functional Programming, volume 3622 of LNCS-Tutorial, pages 130--170. Springer-Verlag, 2004.
• 17: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 18: Peter J. McCann , Satish Chandra, Packet types: abstract specification of network protocol messages, Proceedings of the conference on Applications, Technologies, Architectures, and Protocols for Computer Communication, p.321-333, August 28-September 01, 2000, Stockholm, Sweden
• 19: James McKinna and Joel Wright. A type-correct, stack-safe, provably correct expression compiler in Epigram. Accepted for publication in the Journal of Functional Programming.
• 20: Peter Morris, Thorsten Altenkirch, and Conor McBride. Exploring the regular tree types. In Types for Proofs and Programs, volume 3839 of LNCS. Springer-Verlag, 2004.
• 21: Henrik Nilsson , Antony Courtney , John Peterson, Functional reactive programming, continued, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.51-64, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581695]
• 22: Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990.
• 23: Ulf Norell. Towards a practical programming language based on dependent type theory. D thesis, Chalmers University of Technology, 2007.
• 24: Simon Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.
• 25: Simon Peyton Jones , Jean-Marc Eber , Julian Seward, Composing contracts: an adventure in financial engineering (functional pearl), Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.280-292, September 2000
• 26: 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
• 27: Tim Sheard, Putting curry-howard to work, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, p.74-85, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088348.1088356]
• 28: Matthieu Sozeau. Subset coercions in Coq. In Types for Proofs and Programs, volume 4502 of LNCS. Springer-Verlag, 2007.
• 29: S. Doaitse Swierstra , Luc Duponcheel, Deterministic, Error-Correcting Combinator Parsers, Advanced Functional Programming, Second International School-Tutorial Text, p.184-207, August 26-30, 1996
• 30: Wouter Swierstra and Thorsten Altenkirch. Dependent types for distributed arrays. In Proceedings of the Ninth Symposium on Trends in Functional Programming, 2008.
• 31: The Agda Team. Agda homepage. http://www.cs.chalmers.se/~ulfn/Agda, 2008.
• 32: Peter Thiemann. Server-side web programming in WASH. In Advanced Functional Programming, volume 3622 of LNCS-Tutorial. Springer-Verlag, 2004.
• 33: P. Wadler, Views: a way for pattern matching to cohabit with data abstraction, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.307-313, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41653]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Design, Languages, Theory

Keywords:
dependent types, domain-specific embedded languages