research-article

Reason isomorphically!

Authors:

Daniel W.H. JamesAuthors Info & Claims

WGP '10: Proceedings of the 6th ACM SIGPLAN workshop on Generic programming

Pages 85 - 96

https://doi.org/10.1145/1863495.1863507

Published: 26 September 2010 Publication History

Abstract

When are two types the same? In this paper we argue that isomorphism is a more useful notion than equality. We explain a succinct and elegant approach to establishing isomorphisms, with our focus on showing their existence over deriving the witnesses. We use category theory as a framework, but rather than chasing diagrams or arguing with arrows, we present our proofs in a calculational style. In particular, we hope to showcase to the reader why the Yoneda lemma and adjunctions should be in their reasoning toolbox.

Supplementary Material

MOV File (wgp-1630-james.mov)

Download
174.36 MB

References

[1]

}}Altenkirch, T.: From High School to University Algebra (June 2008), http://www.cs.nott.ac.uk/~txa/publ/unialg.pdf

[2]

}}Atanassow, F., Jeuring, J.: Inferring Type Isomorphisms Generically. In: Mathematics of Program Construction. LNCS, vol. 3125, pp. 32--53 (2004)

[3]

}}Backhouse, R., Bijsterveld, M., van Geldrop, R., van der Woude, J.: Categorical fixed point calculus. In: Category Theory and Computer Science. LNCS, vol. 953, pp. 159--179 (1995)

Digital Library

[4]

}}Backhouse, R., Bijsterveld, M., van Geldrop, R., van der Woude, J.: Category theory as coherently constructive lattice theory (2003), working Document, available from http://www.cs.nott.ac.uk/~rcb/MPC/CatTheory.ps.gz

[5]

}}Barr, M., Wells, C.: Category Theory for Computing Science. Les Publications CRM, Montréal, 3rd edn. (1999), the book is available from Centre de recherches mathématiques http://crm.umontreal.ca/

[6]

}}Cáccamo, M., Winskel, G.: A Higher-Order Calculus for Categories. In: Theorem Proving in Higher Order Logics. LNCS, vol. 2152, pp. 136--153 (2001)

Digital Library

[7]

}}Di Cosmo, R.: The Isomorphisms of Types, http://www.dicosmo.org/ResearchThemes/ISOS/ISOShomepage.html

[8]

}}Di Cosmo, R.: A short survey of isomorphisms of types. Math. Struct. in Comp. Sci. 15(05), 825--838 (2005)

Digital Library

[9]

}}Fiore, M.: Isomorphisms of Generic Recursive Polynomial Types. In: Principles of programming languages. pp. 77--88. ACM (2004)

Digital Library

[10]

}}Fokkinga, M. M., Meertens, L.: Adjunctions. Tech. Rep. Memoranda Inf 94--31, University of Twente, Enschede, Netherlands (June 1994)

[11]

}}Fokkinga, M. M.: Calculate categorically! Formal Aspects of Computing 4(2), 673--692 (1992)

[12]

}}Gibbons, J., Paterson, R.: Parametric datatype-genericity. In: Workshop on Generic programming. pp. 85--93. ACM Press (August 2009)

Digital Library

[13]

}}Hinze, R.: Type fusion. In: Pavlovic, D., Johnson, M. (eds.) Algebraic Methodology And Software Technology (2010), to appear

[14]

}}Knuth, D. E.: The Art of Computer Programming, Volume 3: Sorting and Searching. Addison-Wesley Publishing Company, 2nd edn. (1998)

Digital Library

[15]

}}Lambek, J.: A fixpoint theorem for complete categories. Math. Zeitschr. 103, 151--161 (1968)

[16]

}}Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, Springer-Verlag, Berlin, 2nd edn. (1998)

[17]

}}Mazur, B.: When is one thing equal to some other thing? http://abel.math.harvard.edu/~mazur/preprints/when_is_one.pdf (Sept 2007)

[18]

}}Rydeheard, D.E.: Adjunctions. In: Category Theory and Computer Programming. LNCS, vol. 240, pp. 51--57 (1986)

Digital Library

[19]

}}Soloviev, S.: A Complete Axiom System for Isomorphism of Types in Closed Categories. In: Logic Programming and Automated Reasoning. LNCS, vol. 698, pp. 360--371 (1993)

Digital Library

Cited By

Boisseau GGibbons J(2018)What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl)Proceedings of the ACM on Programming Languages10.1145/32367792:ICFP(1-27)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236779
Hinze RJames DHarper TWu NMagalhães JLöh AGarcia R(2012)Sorting with bialgebras and distributive lawsProceedings of the 8th ACM SIGPLAN workshop on Generic programming10.1145/2364394.2364405(69-80)Online publication date: 12-Sep-2012
https://dl.acm.org/doi/10.1145/2364394.2364405
Hinze R(2012)Kan extensions for program optimisation orProceedings of the 11th international conference on Mathematics of Program Construction10.1007/978-3-642-31113-0_16(324-362)Online publication date: 25-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31113-0_16
Show More Cited By

Index Terms

Reason isomorphically!
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory
  2. Semantics and reasoning
    1. Program reasoning
      1. Program specifications

Recommendations

The category of pointwise S-proximity spaces

First it is proved that the category of pointwise quasi-uniform spaces and pointwise quasi-uniformly continuous morphisms is topological. Then the concept of pointwise S-quasi-proximity on lattice-valued fuzzy set theory is introduced in such a way as ...
Generalized Eilenberg Theorem: Varieties of Languages in a Category

For finite automata as coalgebras in a category C, we study languages they accept and varieties of such languages. This generalizes Eilenberg’s concept of a variety of languages, which corresponds to choosing as C the category of Boolean algebras. ...
Limit structures over completely distributive lattices
Possibility theory and fuzzy logic

The notion of a limit molecular lattice--a completely distributive lattice with some kinds of convergence of ideals on it--is introduced. It is proved that the category of limit molecular lattices is a cartesian closed category containing the category ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

WGP '10: Proceedings of the 6th ACM SIGPLAN workshop on Generic programming

September 2010

116 pages

ISBN:9781450302517

DOI:10.1145/1863495

General Chairs:
Bruno C.d.S. Oliveira
Seoul National University, Seoul, Korea
,
Marcin Zalewski
Indiana University, Bloomington, IN

Copyright © 2010 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 September 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '10

Sponsor:

SIGPLAN

ICFP '10: ACM SIGPLAN International Conference on Functional Programming

September 26, 2010

Maryland, Baltimore, USA

Acceptance Rates

Overall Acceptance Rate 30 of 43 submissions, 70%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
275
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Boisseau GGibbons J(2018)What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl)Proceedings of the ACM on Programming Languages10.1145/32367792:ICFP(1-27)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236779
Hinze RJames DHarper TWu NMagalhães JLöh AGarcia R(2012)Sorting with bialgebras and distributive lawsProceedings of the 8th ACM SIGPLAN workshop on Generic programming10.1145/2364394.2364405(69-80)Online publication date: 12-Sep-2012
https://dl.acm.org/doi/10.1145/2364394.2364405
Hinze R(2012)Kan extensions for program optimisation orProceedings of the 11th international conference on Mathematics of Program Construction10.1007/978-3-642-31113-0_16(324-362)Online publication date: 25-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31113-0_16
Hinze R(2010)Generic programming with adjunctionsProceedings of the 2010 international spring school conference on Generic and Indexed Programming10.1007/978-3-642-32202-0_2(47-129)Online publication date: 22-Mar-2010
https://dl.acm.org/doi/10.1007/978-3-642-32202-0_2

View Options

Get Access

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.

Media

Figures

Other

Tables

View Table of Contents