How to combine a comonad and a monad into a comonad?

Question

Assume I have

• a comonad D
• a monad T
• a distributive law l : D T -> T D of the comonad D over the monad T.

How can I define the comonad D T?

Answer 1

You can't. Suppose D is the identity comonad and T is Cont Void, i.e. the continuation monad at the empty type.

newtype D a = D {runD :: a}
newtype T a = T {runT :: (a -> Void) -> Void}

Then distributivity holds trivially. But extract :: D (T a) -> a is not definable as a total computable program. It would be double negation elimination forall a. ((a -> Void) -> Void) -> a, which is not definable in constructive languages.