Putting curry-howard to work

ABSTRACT

The Curry-Howard isomorphism states that types are propositions and that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately, the type systems of today's functional languages cannot directly express interesting properties of programs. To alleviate this problem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized Algebraic Datatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new features are backward compatible with existing features, and combine to enable a new programming paradigm for functional programmers. This paradigm makes it possible to state and enforce interesting properties of programs using the type system, and it does this in manner that leaves intact the functional programming style, known and loved by functional programmers everywhere.

REFERENCES

• 1: Lennart Augustsson, Cayenne—a language with dependent types, ACM SIGPLAN Notices, v.34 n.1, p.239-250, Jan. 1999
• 2: Lennart Augustsson. Equality proofs in cayenne, July 11 2000.
• 3: Lennart Augustsson and Kent Petersson. Silly type families. Available from: http://www.cs.pdx.edu/~sheard/papers/silly.pdf, 1994.
• 4: Arthur I. Baars , S. Doaitse Swierstra, Typing dynamic typing, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.157-166, October 04-06, 2002, Pittsburgh, PA, USA
• 5: H. P. Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 6: James Cheney and Ralf Hinze. First-class phantom types. Technical Report TR2003-1901, Cornell University, 2003. Also available from: http://www.informatik.uni-bonn.de/~ralf/publications/Phantom.pdf.
• 7: Catarina Coquand. Agda is a system for incrementally developing proofs and programs. Web page describing AGDA: http://www.cs.chalmers.se/~catarina/agda/ .
• 8: Thierry Coquand , Peter Dybjer, Inductive Definitions and Type Theory: an Introduction (Preliminary Version), Proceedings of the 14th Conference on Foundations of Software Technology and Theoretical Computer Science, p.60-76, December 15-17, 1994
• 9: Rowan Davies, Refinement-Type Checker for Standard ML, Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology, p.565-566, December 13-17, 1997
• 10: Dominic Duggan, Dynamic typing for distributed programming in polymorphic languages, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.11-45, Jan. 1999 [doi>10.1145/314602.314604]
• 11: Peter Dybjer , Anton Setzer, A Finite Axiomatization of Inductive-Recursive Definitions, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, p.129-146, April 07-09, 1999
• 12: Robert Harper , Robert Pollack, Type checking with universes, Theoretical Computer Science, v.89 n.1, p.107-136, Oct. 21, 1991
• 13: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 14: James Cheney , Ralf Hinze, A lightweight implementation of generics and dynamics, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.90-104, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581698]
• 15: Infopipe web sites:. http://www.cs.pdx.edu/~walpole/infopipes.html, and http://woodworm.cs.uml.edu/~rprice/ep/koster/.
• 16: Mark P. Jones, A system of constructor classes: overloading and implicit higher-order polymorphism, Proceedings of the conference on Functional programming languages and computer architecture, p.52-61, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165190]
• 17: Simon Peyton Jones and Mark Shields. Practical type inference for arbitrary-rank types. Technical report, Microsoft Research, December 2003. http://research.microsoft.com/Users/simonpj/.
• 18: Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: type inference for generalised algebraic data types. http://research.microsoft.com/Users/simonpj/, 2004.
• 19: A. J. Kfoury and Said Jahama. Type reconstruction in the presence of polymorphic recursion and recursive types. Technical report, March 21 2000.
• 20: Zhaohui Luo and Robert Pollack. LEGO proof development system: User's manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, May 1992. Updated version.
• 21: Connor McBride. Epigram: Practical programming with dependent types. In Notes from the 5th International Summer School on Advanced Functional Programming, August 2004. Available at: http://www.dur.ac.uk/CARG/epigram/epigram-afpnotes.pdf .
• 22: 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]
• 23: Bengt Nordstrom. The ALF proof editor, March 20 1996.
• 24: Emir Pasalic , Timothy E. Sheard, The role of type equality in meta-programming, OGI School of Science & Engineering, 2004
• 25: Emir Pasalic and Nathan Linger. Meta-programming with typed object-language representations. In Generative Programming and Component Engineering (GPCE'04), pages 136 -- 167, October 2004. LNCS volume 3286.
• 26: Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361--386. Academic Press, 1990.
• 27: Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 28: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 29: Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028711]
• 30: Tim Sheard, James Hook, and Nathan Linger. GADTs + extensible kind system = dependent programming. Technical report, Portland State University, 2005. http://www.cs.pdx.edu/~sheard.
• 31: Tim Sheard and Nathan Linger. Programming with static invariants in Omega, September 2004. Available from: http://www.cs.pdx.edu/~sheard/ .
• 32: Tim Sheard and Emir Pasalic. Meta-programming with built-in type equality. In Logical Frameworks and Meta-Languages workshop, July 2004. Available at: http://cs-www.cs.yale.edu/homes/carsten/lfm04/.
• 33: Vincent Simonet and Francois Pottier. Constraint-based type inference for guarded algebraic data types. Available from: http://cristal.inria.fr/~simonet/publis/index.en.html.
• 34: Peter J. Stuckey and Martin Sulzmann. Type inference for guarded recursive data types, February 2005. Available from: http://www.comp.nus.edu.sg/~sulzmann/ .
• 35: Aaron Stump. Imperative LF meta-programming. In Logical Frameworks and Meta-Languages workshop, July 2004. Available at: http://cs-www.cs.yale.edu/homes/carsten/lfm04/.
• 36: Martin Sulzmann and Meng Wang. A systematic translation of guarded recursive data types to existential types, February 2005. Available from: http://www.comp.nus.edu.sg/~sulzmann/ .
• 37: The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 7.4. INRIA, 2003. http://pauillac.inria.fr/coq/doc/main.html.
• 38: Stephanie Weirich, Type-safe cast: (functional pearl), ACM SIGPLAN Notices, v.35 n.9, p.58-67, Sept. 2000
• 39: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, 1998
• 40: Hongwei Xi, Dead Code Elimination through Dependent Types, Proceedings of the First International Workshop on Practical Aspects of Declarative Languages, p.228-242, January 18-19, 1999
• 41: 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
• 42: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, ACM SIGPLAN Notices, v.33 n.5, p.249-257, May 1998
• 43: 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

General Terms:
Languages, Reliability, Theory, Verification

Keywords:
GADT, curry-howard isomorphism, extensional kind system, haskell, logic