Observational equality, now!

ABSTRACT

This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type

• which is substitutive, allowing us to reason by replacing equal for equal in propositions;
• which reflects the observable behaviour of values rather than their construction: in particular, we have extensionality-- functions are equal if they take equal inputs to equal outputs;
• which retains strong normalisation, decidable typechecking and canonicity--the property that closed normal forms inhabiting datatypes have canonical constructors;
• which allows inductive data structures to be expressed in terms of a standard characterisation of well-founded trees;
• which is presented syntactically--you can implement it directly, and we are doing so this approach stands at the core of Epigram 2;
• which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system [21].

.

Until now, it has always been necessary to sacrifice some of these aspects. The closest attempt in the literature is Altenkirch's construction of a setoid-model for a system with canonicity and extensionality on top of an intensional type theory with proof-irrelevant propositions [4]. Our new proposal simplifies Altenkirch's construction by adopting McBride's heterogeneous approach to equality [19].

REFERENCES

• 1: Michael Abbott , Thorsten Altenkirch , Neil Ghani, Containers: constructing strictly positive types, Theoretical Computer Science, v.342 n.1, p.3-27, 6 September 2005 [doi>10.1016/j.tcs.2005.06.002]
• 2: Andreas Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München, 2006.
• 3: Andreas Abel , Thierry Coquand , Peter Dybjer, Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.3-12, July 10-14, 2007 [doi>10.1109/LICS.2007.33]
• 4: Thorsten Altenkirch, Extensional Equality in Intensional Type Theory, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.412, July 02-05, 1999
• 5: 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
• 6: Alexandre Buisse and Peter Dybjer. Formalizing categorical models of type theory in type theory. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007.
• 7: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 8: Thierry Coquand. Pattern matching with dependent types. In BNordström, KPettersson, and GPlotkin, editors, Informal Proceedings Workshop on Types for Proofs and Programs, Båstad, Sweden, 8--12 June 1992, pages 71--84. Dept. of Computing Science, Chalmers Univ. of Technology and Göteborg Univ., 1992.
• 9: 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
• 10: Peter Dybjer, Inductive sets and families in Martin-Lo¨f's type theory and their set-theoretic semantics, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 11: Conor McBride et al. Epigram, 2004. http://www.e-pig.org.
• 12: Healfdene Goguen, Conor McBride, and James McKinna. Eliminating dependent pattern matching. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and José Meseguer, editors, Essays Dedicated to Joseph A. Goguen, volume 4060 of Lecture Notes in Computer Science, pages 521--540. Springer, 2006.
• 13: Martin Hofmann, Conservativity of Equality Reflection over Intensional Type Theory, Selected papers from the International Workshop on Types for Proofs and Programs, p.153-164, June 05-08, 1995
• 14: Martin Hofmann. Extensional concepts in intensional type theory. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, 1995. Available from http://www.lfcs.informatics.ed.ac.uk/reports/95/ECS-LFCS-95-327/.
• 15: Martin Hofmann and Thomas Streicher. A groupoid model refutes uniqueness of identity proofs. In LICS 94, pages 208--212, 1994.
• 16: GHuet and ASaïbi. Constructive Category Theory. MIT Press, 1998.
• 17: Zhaohui Luo, Computation and reasoning: a type theory for computer science, Oxford University Press, Inc., New York, NY, 1994
• 18: Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999. Available from http://www.lfcs.informatics.ed.ac.uk/reports/00/ECS-LFCS-00-419/.
• 19: Conor McBride, Elimination with a Motive, Selected papers from the International Workshop on Types for Proofs and Programs, p.197-216, December 08-12, 2000
• 20: 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]
• 21: Ulf Norell. Agda 2. http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php.
• 22: Nicolas Oury. Extensionality in the calculus of constructions. In TPHOL 05, pages 278--293, 2005.
• 23: C. Paulin-Mohring, Extracting &ohgr;'s programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.89-104, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75285]
• 24: 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
• 25: 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]
• 26: 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]
• 27: David A. Turner. A new formulation of constructive type theory. In Peter Dybjer et al., editor, Proceedings of the Workshop on Programming Logic. Programming Methodology Group, University of Gothenburg and Chalmers University of Technology, 1989.
• 28: B. Werner. Une Théorie des Constructions Inductives. PhD thesis, Université Paris 7, 1994.
• 29: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Carnegie Mellon University, Pittsburgh, PA, 1998

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

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

General Terms:
Languages, Theory

Keywords:
equality, type theory