如何将一个 comonad 和一个 monad 组合成一个 comonad？

Question

假设我有

• 共生 D
• 单子 T
• 一个l : D T -> T DcomonadD对 monad的分配法则T。

我如何定义 comonad D T？

Answer 1

你不能。假设D是恒等共子并且T是Cont Void，即空类型的延续单子。

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

那么分配性就变得微不足道了。但extract :: D (T a) -> a不能定义为完全可计算的程序。这将是双重否定消除forall a. ((a -> Void) -> Void) -> a，这在构造性语言中是无法定义的。