Hacker News Reader

> The problem is that no one thinks of type conversions as taking any explicit paths!

Indeed. This is super surprising to me and I’m adding the topic to my “study” list. I had no idea until today - I easily could imagine it’s possible if some of the type conversions are “lossy” (e.g. maps to lists), but I have a strong feeling that simpified lossy conversions are not what is being referenced.

View on HN

Most of Buzzard's examples are indeed lossless (even bijective) conversions, but the notation mathematicians use (and programming languages often support) makes it look like they are completely absent, which comes back to bite you. In mathematics, it bites you when you want to actually compute your function and realize you don't remember how all those canonical arrows go. In programming, it bites you when the default conversions the compiler inserts aren't the ones you meant.

Reply on news.ycombinator.com