Ralf Hinze and Daniel W.H. James
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.
New York‚ NY‚ USA
Proceedings of the 6th ACM SIGPLAN workshop on Generic programming
Oliveira‚ Bruno C.d.S. and Zalewski‚ Marcin
Baltimore‚ Maryland‚ USA