Hey! First of all, that's a great post, and I definitely like your writing style!
Regarding this bit:
Huh. This is totally useless. I suspect I have performed the flipping of arrows incorrectly. Edward Yang has a really good post on category theory and flipping arrows, so I'll read that and come back to this.
Given catch0 :: start -> handler -> result, the arrows there should've been also flipped, resulting in
cocatch0
:: result
-> handler
-> start
or, substituting the flipped versions:
cocatch
:: (rest, a)
-> ((rest, a) -> small)
-> ((small, rest), a)
I think that makes a tad more sense and is actually very close to what you later derive using monadic and comonadic reasoning (in fact that's equivalent modulo keeping the original rest in the resulting tuple).
Hey! First of all, that's a great post, and I definitely like your writing style!
Regarding this bit:
Given
catch0 :: start -> handler -> result, the arrows there should've been also flipped, resulting inor, substituting the flipped versions:
I think that makes a tad more sense and is actually very close to what you later derive using monadic and comonadic reasoning (in fact that's equivalent modulo keeping the original
restin the resulting tuple).Cheers!