Reason isomorphically!
Ralf Hinze and Daniel W.H. James
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.
Details
| Address |
New York‚ NY‚ USA |
| Book Title |
Proceedings of the 6th ACM SIGPLAN workshop on Generic programming |
| Editor |
Oliveira‚ Bruno C.d.S. and Zalewski‚ Marcin |
| ISBN |
978−1−4503−0251−7 |
| Location |
Baltimore‚ Maryland‚ USA |
| Month |
September |
| Pages |
85–96 |
| Publisher |
ACM |
| Series |
WGP '10 |
| Year |
2010 |
Links
Related pages
|
People |