问题标签 [codata]

换种说法：如果我们要分别删除终止检查和使用归纳和共归纳数据类型的保护条件，那么归纳/共归纳和修复/共定之间是否会不再存在根本区别？

我所说的“根本差异”是指 Coq 核心演算的差异——而不是语法和证明搜索等方面的差异。

这似乎最终归结为一个关于构造微积分的问题。

注意：我知道一个跳过终止检查/递归/核心递归的保护的定理证明器可以证明——False所以，如果它有帮助，请将其视为关于非完全编程而不是证明的问题。

Haskell 有一个名为的类型NFData，其形状如下：

比“功能”更“数据”的类型可以配备NFData. 每个这样的实例都会彻底分析该类型的给定值及其传递包含的任何内容。这迫使重击并爆炸潜在底部。

注意：有点神秘的是，即使是“函数式”类型也配备了实例，尽管它们实际上并没有将它们的参数简化为正常形式。

案例分析就这么多。但有时采取双重视角并考虑更类似于余数据而不是数据的事物是有用的。我们不想分析其案例的总和，而是希望建立一个记录到其领域。

因此，在对我在说什么没有任何真正想法的情况下，我可能会因此而蒙混过关，将遇到的任何箭头都转过来，并在几个选项中穿插Co：

对于表示非严格字段的​​有限乘积的类型（粗略地说，“单一构造函数”类型），我期望以下形式的实例：

对于所有具有少于/多于一个构造函数的数据类型，我希望有以下形式的实例：

注意：这可能有点可疑，但如果我们不提供这些实例，我们将只使用()与NFCodata.

最终结果应该是这样的类型的派生实例：

行为如下：

这个想法是可以使用镜头Foo来Bar填充这个空脊的内容。

所以......问题：

1. 上这样的课有意义吗？是否已经有某种方法可以获取带有底部内容的 codata 类型的“脊椎”？是否NFCodata已经以其他更原则的形式存在？
2. {NF}data 和 {NF}Codata 之间是否存在某种严格的类比？
3. “NF”真的是“NFCodata”中使用的正确前缀吗？有没有更贴切的数学术语（更重要的是思维方式）适用于此？