categories icon indicating copy to clipboard operation
categories copied to clipboard

Witness for isomorphism between Exp and Coexp?

Open Zemyla opened this issue 7 years ago • 0 comments

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?

Zemyla avatar Dec 13 '18 17:12 Zemyla