问题标签 [agda]

不用说，Haskell 中的标准构造

很棒而且非常有用。

尝试在 Agda 中定义类似的东西（为了完整起见，我将其放入）

失败，因为f不一定是严格积极的。这是有道理的——通过适当的选择，我可以很容易地从这个结构中得到一个矛盾。

我的问题是：有没有希望在 Agda 中编码递归方案？已经完成了吗？需要什么？

我有点不确定这是一个 math.SE 问题还是一个 SO 问题，但我怀疑数学家一般不太可能特别了解或关心这一类别，而 Haskell 程序员可能会这样做。

因此，我们知道Hask 或多或少有产品（当然，我在这里使用的是理想化的 Hask）。我对它是否有均衡器很感兴趣（在这种情况下它会有所有有限的限制）。

直觉上似乎不是，因为你不能像在集合上那样进行分离，所以子对象通常似乎很难构造。但是对于您想提出的任何特定情况，似乎您可以通过在Set中计算均衡器并对其进行计数来破解它（毕竟，每种 Haskell 类型都是可数的，并且每个可数集都是同构于有限类型或自然数，Haskell 都有）。所以我看不出我将如何寻找反例。

现在，Agda 似乎更有希望了：在那里形成子对象相对容易。明显的 sigma 类型Σ A (λ x → f x == g x)是均衡器吗？如果细节不起作用，它在道德上是一个均衡器吗？

在 Agda 中，我如何定义一对必须具有相同长度的向量？

我试图弄清楚类型层次结构在 Agda 中是如何工作的。

假设我定义了一个集合类型 X：

然后继续构造一个归纳类型

是什么类型的X -> Set？是设置还是类型？

谢谢！

示例代码中有部分代码。我只是想知道中缀器的含义是什么，以及为什么在那里使用它。

谢谢

any ideal what is << >> mean?

or what the meaning of

_∷⟪_⟫_ : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

thanks

我想有一个归纳类型来描述排列及其对某些容器的作用。很明显，根据对这种类型的描述，算法的定义复杂性（就其长度而言）（计算组合或逆，分解成不相交的循环等）会有所不同。

考虑 Coq 中的以下定义。我相信这是 Lehmer 代码的形式化：

在大小为 n 的向量上定义它的作用很容易，在其他容器上稍微难一些，而且（至少对我而言）很难找到组合或逆的形式化。

或者，我们可以将置换表示为具有属性的有限映射。组合或逆可以很容易地定义，但将其分解为不相交的循环是困难的。

所以我的问题是：有没有解决这个权衡问题的论文？我设法找到的所有作品都处理命令式设置中的计算复杂性，而我对“推理复杂性”和函数式编程感兴趣。