Article

Observational equality, now!

Authors:

Thorsten Altenkirch,

Wouter SwierstraAuthors Info & Claims

PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification

Pages 57 - 68

https://doi.org/10.1145/1292597.1292608

Published: 02 October 2007 Publication History

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, and Neil Ghani. Containers - constructing strictly positive types. Theoretical Computer Science, 342:3--27, September 2005.

Digital Library

[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, and Peter Dybjer. Normalization by evaluation for Martin-Löf type theory with typed equality judgements. In Logic in Computer Science, 2007.

Digital Library

[4]

Thorsten Altenkirch. Extensional equality in intensional type theory. In LICS 99, 1999.

Digital Library

[5]

Lennart Augustsson. Cayenne - a language with dependent types. In ICFP '98: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, pages 239--250, 1998.

Digital Library

[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]

Robert L. Constable, Stuart F. Allen, HM. Bromley, WR. Cleaveland, JF. Cremer, RW. Harper, Douglas J. Howe, TB. Knoblock, NP. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986.

Digital Library

[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]

PDybjer and ASetzer. A finite axiomatization of inductive-recursive definitions. Typed Lambda Calculi and Applications, 1581:129--146, 1999.

Digital Library

[10]

Peter Dybjer. Inductive Sets and Families in Martin-Löf's Type Theory. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.

Digital Library

[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. In TYPES 95, pages 153--164, 1995.

Digital Library

[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, 1994.

Digital Library

[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. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, Types for Proofs and Programs (Proceedings of the International Workshop, TYPES'00), volume 2277. Springer-Verlag, 2002.

Digital Library

[20]

Conor McBride and James McKinna. The view from the left. Journal of Functional Programming, 14(1):69--111, 2004.

Digital Library

[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.

Digital Library

[23]

CPaulin-Mohring. Extracting F_Ω's programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989. ACM.

Digital Library

[24]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, 2006.

Digital Library

[25]

Tim Sheard. Putting Curry-Howard to work. In Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, pages 74--85, 2005.

Digital Library

[26]

Martin Sulzmann, Manuel MT. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. System f with type equality coercions. In TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, pages 53--66, New York, NY, USA, 2007. ACM Press.

Digital Library

[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. Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, 1998.

Digital Library

Cited By

Ceulemans JNuyts ADevriese D(2025)BiSikkel: A Multimode Logical Framework in AgdaProceedings of the ACM on Programming Languages10.1145/37048449:POPL(210-240)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704844
Van Muylder ANuyts ADevriese D(2024)Internal and Observational Parametricity for Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328508:POPL(209-240)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632850
Šefl V(2024)Programming with Dependent Additive PairsTrends in Functional Programming10.1007/978-3-031-74558-4_5(92-111)Online publication date: 8-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-74558-4_5
Show More Cited By

Index Terms

Observational equality, now!

Recommendations

Impredicative Observational Equality

In dependent type theory, impredicativity is a powerful logical principle that allows the definition of propositions that quantify over arbitrarily large types, potentially resulting in self-referential propositions. Impredicativity can provide a system ...
Observational equality: now for good

Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TTobs, a new type theory based on the setoidal interpretation of dependent type theory. TTobs equips every type with an ...
Proof Search in Intuitionistic Logic with Equality, or Back toSimultaneous Rigid E -Unification

We characterize provability in intuitionistic logic with equality in terms of a constraint calculus. This characterization uncovers close connections between provability in intuitionistic logic with equality and solutions to simultaneous rigid E -...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification

October 2007

76 pages

ISBN:9781595936776

DOI:10.1145/1292597

Program Chairs:
Aaron Stump
Washington University in St. Louis, USA
,
Hongwei Xi
Boston University, USA

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 October 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP07

Sponsor:

ICFP07: ACM SIGPLAN International Conference on Functional Programming

October 5, 2007

Freiburg, Germany

Acceptance Rates

PLPV '07 Paper Acceptance Rate 6 of 8 submissions, 75%;

Overall Acceptance Rate 18 of 25 submissions, 72%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

75
Total Citations
View Citations
715
Total Downloads

Downloads (Last 12 months)62
Downloads (Last 6 weeks)3

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ceulemans JNuyts ADevriese D(2025)BiSikkel: A Multimode Logical Framework in AgdaProceedings of the ACM on Programming Languages10.1145/37048449:POPL(210-240)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704844
Van Muylder ANuyts ADevriese D(2024)Internal and Observational Parametricity for Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328508:POPL(209-240)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632850
Šefl V(2024)Programming with Dependent Additive PairsTrends in Functional Programming10.1007/978-3-031-74558-4_5(92-111)Online publication date: 8-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-74558-4_5
Laurent TLennon-Bertrand MMaillard K(2024)Definitional Functoriality for Dependent (Sub)TypesProgramming Languages and Systems10.1007/978-3-031-57262-3_13(302-331)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_13
Pujet LTabareau N(2024)Observational Equality Meets CICProgramming Languages and Systems10.1007/978-3-031-57262-3_12(275-301)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_12
Pujet LTabareau N(2023)Impredicative Observational EqualityProceedings of the ACM on Programming Languages10.1145/35717397:POPL(2171-2196)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571739
Allais G(2023)Builtin Types Viewed as Inductive FamiliesProgramming Languages and Systems10.1007/978-3-031-30044-8_5(113-139)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_5
Maillard KLennon-Bertrand MTabareau NTanter É(2022)A reasonably gradual type theoryProceedings of the ACM on Programming Languages10.1145/35476556:ICFP(931-959)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547655
Eremondi JGarcia RTanter É(2022)Propositional equality for gradual dependently typed programmingProceedings of the ACM on Programming Languages10.1145/35476276:ICFP(165-193)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547627
Pujet LTabareau N(2022)Observational equality: now for goodProceedings of the ACM on Programming Languages10.1145/34986936:POPL(1-27)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498693
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten