如何将comonad和monad合并成comonad？

Question

假设我有

单模D

• a单模T

• a分布律
• D上的单模T.

如何定义comonad D T

Answer 1

假设D是标识comonad，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，这是不能定义的建设性语言。