%0 Conference Paper %1 hinze2010reason %A Hinze, Ralf %A James, Daniel W. H. %B WGP '10: Proceedings of the 6th ACM SIGPLAN workshop on Generic programming %D 2010 %E d. S. Oliveira, Bruno C. %E Zalewski, Marcin %I ACM %K 68n18-functional-programming-and-lambda-calculus %P 85-96 %R 10.1145/1863495.1863507 %T Reason isomorphically! %U https://dl.acm.org/doi/10.1145/1863495.1863507 %X 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. %@ 978-1-4503-0251-7

@inproceedings{hinze2010reason, 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.}, added-at = {2023-10-31T07:47:30.000+0100}, author = {Hinze, Ralf and James, Daniel W. H.}, biburl = {https://www.bibsonomy.org/bibtex/2ff9550802787025832f952c4f4034f22/gdmcbain}, booktitle = {WGP '10: Proceedings of the 6th ACM SIGPLAN workshop on Generic programming}, crossref = {conf/icfp/2010wgp}, doi = {10.1145/1863495.1863507}, editor = {d. S. Oliveira, Bruno C. and Zalewski, Marcin}, ee = {https://doi.org/10.1145/1863495.1863507}, interhash = {6c2e6d8cde73b0aef5036168b71ef9b5}, intrahash = {ff9550802787025832f952c4f4034f22}, isbn = {978-1-4503-0251-7}, keywords = {68n18-functional-programming-and-lambda-calculus}, month = sep, pages = {85-96}, publisher = {ACM}, timestamp = {2023-10-31T23:16:19.000+0100}, title = {Reason isomorphically!}, url = {https://dl.acm.org/doi/10.1145/1863495.1863507}, year = 2010 }