- 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.
- Publication status:
- Publisher copy:
- WGP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN WORKSHOP ON GENERIC PROGRAMMING
- Publication date:
- Source identifiers:
- Copyright date:
If you are the owner of this record, you can report an update to it here: Report update to this record