categories
categories copied to clipboard
Witness for isomorphism between Exp and Coexp?
I've been trying to write various combinators using just the functions in the Control.Category.* and Control.Categorical.* packages, and I've wound up repeatedly getting stuck trying to produce a witness for what seems to be the obvious isomorphism:
type Zero t = Id t (Sum t)
type One t = Id t (Product t)
expToCoexp :: (CCC t, CoCCC t, Distributive t) => t (Exp t a (Zero t)) (Coexp t a (One t))
coexpToExp :: (CCC t, CoCCC t, Distributive t) => t (Coexp t a (One t)) (Exp t a (Zero t))
With those I could derive things like callCC :: (CCC t, CoCCC t, Distributive t) => t (Exp t (Exp t a b) a) a, which seems rather obvious given that the primary type that is both CCC and CoCCC is Kleisli (ContT r m).
Can those be derived from the combinators in the categories package, or is a separate class required to be able to "cross the streams" like this, the way Distributive is to cross them between sums and products?