Reason Isomorphically!

Journal article

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. © 2010 ACM.

Authors: Hinze, R; James, D; ACM

• Publication status: Published
• Journal: WGP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN WORKSHOP ON GENERIC PROGRAMMING
• Pages: 85-96
• Publication date: 2010-01-01
• DOI: 10.1145/1863495.1863507
• Language: English
• Keywords: adjunctions; isomorphism; category theory; Yoneda lemma