如何将comonad和monad组合成comonad？

Question

假设我有

• comonad D
• 一个单子T
• 共单子D对单子T的分配律l : D T -> T D。

我怎样才能定义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，这在建设性语言中是无法定义的。