如何将一个逗号和一号组合成一个逗号?

Question

假设我有

• 一个科莫纳德D
• 一个单子T
• l : D T -> T D的分配法则D于单子T。

如何定义D T

？

Answer 1

你不能。假设D是恒等式 comonad，T是Cont Void的，即空类型的延续 monad。

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，这在建构语言中是无法定义的。