win*_*zki 7 monads continuations haskell category-theory dependent-type
类型构造函数上的代码密度 monadf定义如下：
newtype C f a = C { unC \xe2\x88\xb7 forall r. (a \xe2\x86\x92 f r) \xe2\x86\x92 f r }\n众所周知，它C f是任何类型构造函数的 monad f（不一定是协变的）。代码密度单子有多种用途，但它是一种复杂的类型，包含通用类型量词下的高阶函数。
我的问题是，什么f可以证明C f相当于一个没有类型量词定义的更简单的 monad？
一些可以简化的示例：
\nf 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)（作家单子），为此C f a = ((a -> w) -> a, (a -> w) -> w)
f a = a -> s（逆变函子）然后C f a = (a -> s) -> s（延续单子）。
f a = a -> a（既不是协变也不是逆变）并且C f a = List a
在前四种情况中，类型等价可以从米田恒等式导出：forall r. (a -> r) -> F r = F awhenF是协变函子。最后一种情况是通过归纳类型的 Church 编码导出的List。
我查看了其他一些示例，发现在大多数情况下C f似乎并不等同于任何更简单的事情。
即使我们只是采用f a = Maybe a结果类型似乎并不等同于更简单的类型表达式：
newtype CMaybe a = CMaybe { unCMaybe \xe2\x88\xb7 forall r. (a \xe2\x86\x92 Maybe r) \xe2\x86\x92 Maybe r }\n此处不能使用米田恒等式。我最好的猜测（到目前为止我还没有证据）是CMaybe a = (a -> Bool) -> Bool对该类型的函数施加了一些额外的法律。对值施加方程只能在依赖类型语言中充分表达。
可以简化 上的代码密度单子吗Maybe？
是否还有其他类型构造函数的示例f可以C f简化为没有类型量词的类型？
正如评论中提到的，函数C Maybe a返回的信息比布尔值多一点，因为它r返回标识回调中的单个输入，因此f k选择x这样k x的Just。
将回调类型从a -> Maybe rto简化a -> Bool，得到以下依赖函数类型，分别用 Agda 和 Coq 编写，供参考：
-- Agda\n\n(\xe2\x88\x80 {r} \xe2\x86\x92 (a \xe2\x86\x92 Maybe r) \xe2\x86\x92 Maybe r)\n\xe2\x89\xa1\n((k : a \xe2\x86\x92 Bool) \xe2\x86\x92 Maybe (\xe2\x88\x83[ x ] k x \xe2\x89\xa1 true))\n(* Coq *)\n\n(forall r, (a -> option r) -> option r)\n=\n(forall (k : a -> bool), option { x : a | k x = true })\nAgda 中的等价性证明：https://gist.github.com/Lysxia/79846cce777f0394a6f69d84576a325b
\n\xe2\x88\x80 {r} \xe2\x86\x92 (a \xe2\x86\x92 Maybe r) \xe2\x86\x92 Maybe r这证明了和 不带量词的类型的等价性： ((f : a \xe2\x86\x92 Bool) \xe2\x86\x92 Maybe (\xe2\x88\x83[ x ] f x \xe2\x89\xa1 true))，这相当于仅等于if 的q:: (a \xe2\x86\x92 Bool) \xe2\x86\x92 Maybe a限制。q(p)Just xp(x) = true
请注意，如果a是有限的，那么C Maybe a也是有限的。解决该问题的一种方法是计算相应的基函数。
您可以将基数的表达式重新解释为类型，从而为形式的类型提供问题的解决方案Finite a -> C f a。
您可以在在线整数序列百科全书中查找它，以找到替代的组合解释。遗憾的是，相关序列没有太多信息。
\nProduct_{j=1..n} j^C(n-1,j-1)\n\n-- https://oeis.org/A064320\n如果您可以为 找到一个更简单的类型C f a，仅包含和、乘积（不按 的基数索引a）和指数，那么这可能对应于一个非平凡的组合恒等式。相反，找到这种组合恒等式的困难为不存在简单解决方案提供了令人信服的证据。它还提供了一种通过将候选简化的基数与预期基数进行比较来测试候选简化的有效性的快速方法。