能否简化Maybe上的Codensity monad？哪些f的Codensity monad可简化？

类型构造器f上的Codensity monad定义如下：

newtype C f a = C { unC ∷ forall r. (a → f r) → f r }

我们知道，无论f是否为协变类型构造器，C f都是一个monad。Codensity monad虽有诸多用途，但它的类型包含带全称量词的高阶函数，结构较为复杂。

这里提出两个技术问题：

1. 对于哪些f，可证明C f等价于无需类型量词定义的更简单monad？
2. 能否简化Maybe上的Codensity monad？

以下是几种可简化的示例：

• f a = a（恒等函子）：此时C f a = a。
• f a = r -> a（Reader monad）：此时C f是State monad，即C f a = r -> (a, r)。
• f a = (w, a)（Writer monad）：此时C f a = ((a -> w) -> a, (a -> w) -> w)。
• f a = a -> s（逆变函子）：此时C f a = (a -> s) -> s（continuation monad）。
• f a = a -> a（既非协变也非逆变）：此时C f a = List a。

前四种情况的类型等价性可通过Yoneda恒等式推导：当F为协变函子时，forall r. (a -> r) -> F r = F a。最后一种情况则是通过归纳类型List的Church编码推导得出。

多数情况下C f似乎无法简化，比如f a = Maybe a时，其Codensity monad定义为：

newtype CMaybe a = CMaybe { unCMaybe ∷ forall r. (a → Maybe r) → Maybe r }

此处无法应用Yoneda恒等式。我们推测CMaybe a = (a -> Bool) -> Bool，但该类型的函数需要附加额外法则，而这类等式约束仅能在依赖类型语言中充分表达。

内容的提问来源于stack exchange，提问作者winitzki