问题标签 [agda]

Agda 文档提供了一些如何使用该Data.AVL模块的示例：

http://darcsden.com/abel/AgdaPrelude/browse/README/AVL.agda

在示例中，模块在导入时被实例化一次，参数指定存储在树中的值的类型，以及键类型的顺序。

如何在同一个客户端模块中使用不同值类型的 AVL 树（例如字符串树和数字树）？

我正在尝试导出元素类型 A 的 AVL 树的可交换幺半群，给定一个可交换幺半群 (A, +, epsilon)，其中派生运算是unionWith +. AVL 树的等价概念是两棵树相等，如果它们具有相同的toList图像。

我一直试图证明这unionWith +是关联的（根据我的等价概念）。我有交换性和 +-cong 作为假设，因为我想在结合性证明中使用它们，但还没有证明它们。

我已将问题与bibble以下代码中的术语隔离开来：

在bibble中，我有一个证明z ≈ z（即refl），还有一个证明x ∪ tree (Indexed.leaf l<u) ≈ (tree (Indexed.leaf l<u)) ∪ x（通过交换律），我相信我应该能够用它∙-cong来推导出 ≈ 参数的并集也是 ≈ 的证明。

但是，编译器似乎留下了一些未解决的元变量，不幸的是我并不真正了解如何阅读这些消息。我只是做错了什么（证明方式），还是我只需要明确提出一些论点，还是什么？

我们可以很容易地在 Agda 中实现一个分隔的延续 monad。

但是，没有必要这样做，因为 Agda“标准库”有一个定界延续 monad 的实现。然而，让我对这个实现感到困惑的是向DCont类型添加了一个额外的参数。

我的问题是：为什么K那里有额外的参数？我将如何使用该DContIMonadDCont实例？我能否open以某种方式在（全局）范围内获得类似于以下参考实现的内容？

我所有使用它的尝试都导致无法解决的元数据。

不使用 Agda“标准库”的分隔延续的参考实现。

我在锻炼。这似乎是一件微不足道的事情（简化以表明问题显然在于列表拆分）：

总而言之，我声明可以定义两个列表的排列，如果它们可以提供Permutation具有一对相等元素的较小列表xand y，并且插入位置y由zsand确定ys。

然后lemma-ripTop（本来打算做一些完全不同的事情，但这里只是idon Permutation）需要证明给定 a Permutationfor a list ( y :: ys) 的东西。

1. 我不明白为什么 Agda 需要查看zs ++ (y1 :: ys1) == y :: ys（这是我得到的错误）-我认为这应该从类型声明和构造函数中清楚吗？即，既然Permutation xs (y :: ys)是在输入中给出的，那么在构造函数中作为见证提供的拆分p::应该加起来为y :: ys.

2. 如何让 Agda 相信这个列表拆分是有效的？

错误信息：

我已经在一个 Agda 项目上工作了几个星期，尽我所能地忽略关卡多态性。不幸的是（或者也许幸运的是）我似乎已经到了需要开始理解它的地步。

到目前为止，我只在需要它们作为第二个参数Rel（或第三个参数REL）时才使用级别变量。否则我就省略了，直接使用Set。现在我有一些客户端代码可以显式量化各个级别a，并尝试将某些类型的表单传递Set a给我现有的代码，这些代码现在不够多态。在下面的示例中，quibble代表客户端代码，并且_[_]×[_]_是≈-List我现有代码的典型代表，它仅使用Set.

≈-List在这里，我可以使用额外的级别参数扩展 的归纳定义，a以便它可以采用 type 的类型参数Set a，但是我不清楚输入和输出关系的宇宙应该如何变化。然后问题蔓延到更复杂的定义，例如_[_]×[_]_我更不确定如何进行。

我应该如何概括给出的示例中的签名，以便quibble编译？有没有我可以遵循的一般规则？我读过这个。

我想对比两种在 Agda 中为代数结构声明新记录类型的风格。

按照标准 Agda 包中使用的样式Algebra，可以定义BoundedJoinSemilattice如下：

使用这种方法，该字段的任何字段都BoundedJoinSemiLattice与其他更抽象结构的字段重叠（直至重命名） ，例如Setoid、和。为了将 a视为其“超类型”之一，必须调用一个投影函数，该函数负责将其字段映射到超类型的字段，例如上面的函数。SemigroupMonoidCommutativeMonoidBoundedJoinSemiLatticeBoundedJoinSemiLatticecommutativeMonoid

但是，这种字段重复可能会导致代码中出现大量样板，这些样板会从不太具体的代数结构中构建出更具体的代数结构。更自然的定义可能是这样的（重命名CommutativeMonoid为CM）：

这里的想法不是复制CommutativeMonoidinto的字段BoundedJoinSemilattice，而是让后者声明一个 type 的字段CommutativeMonoid。然后我们使用 anopen...public将其子字段“继承”到包含记录中。事实上，这正是标准库中其他地方使用的惯用语Algebra.Structures，除了这里我们还重命名了继承的字段，以便在继承上下文中适当地命名它们。

第二种方法不仅不那么冗余，而且现在想要BoundedJoinSemilattice从 a构造 a 的客户端代码CommutativeMonoid可以简单地将其作为参数传递给正在构造的记录。另一方面，想要BoundedJoinSemilattice从头构造 a 的客户端代码现在必须构造一个中间CommutativeMonoid.

Algebra模块不使用这种继承风格 是有原因的Algebra.Structures吗？也许第二种方法存在我没有发现的问题，或者它没有太大区别：例如，对于第一种方法，也许可以简单地定义一个“构造函数”来处理BoundedJoinSemiLattice从 a 构造 a CommutativeMonoid，恢复了第二种方法的很多便利。

假设您要定义一系列二元运算符（例如，由集合索引），其中参数的类型取决于索引的值，并且索引是显式传递的。此外，假设您希望家庭成员可以使用中缀表示法：

A 这里是索引；括号 [-] 应该表明 A 应该被读作下标。为与此语法兼容的此类操作提供类型签名很困难，因为 x 的类型取决于值A，因此A : Set必须出现x : A在 的定义的左侧_<[_]_。

我已经根据syntax声明尝试了以下技巧（hack？）：

这似乎有效，除非您的二进制操作使用隐式实例。如果我尝试将表单{{x}}的参数添加到syntax声明中，Agda 会抱怨。（也许不是不合理的。）

似乎可以通过引入一个cmp显式地采用隐式实例的版本来适应这个习惯用法，然后定义一个调用该版本的语法变体：

（由于syntax似乎不支持{{x}}参数，所以不能只内联cmp到cmp-explicit，而不放弃完全拾取环境 B 的能力。）

这是黑客吗？当 y 的类型取决于 x 的值并且 x 被显式传递时，是否还有另一种方法来翻转参数 x 和 y？

自然地，定义

导致 Agda 在类型检查时抱怨x。

有没有办法让函数要求两个Setoids，其中第一个Setoid相等意味着后者相等？当然这要求两个Setoids 共享它们Carrier，Carrier而不是一个参数，而是一个记录字段。请求相等的天真尝试Carrier被类型检查器拒绝：

这不行，因为我们在等式证明上没有进行模式匹配，所以不同的Carrier类型不统一。我还没有找到一种方法来表达这一点subst。

考虑以下代码：

当加载 Agda（版本 2.3.2.2）时，Agda 打印与倒数第二行有关的错误“Unsolved metas at the following locations”：

并特别指向 assoc+。

如何提供提示或以其他方式更改代码以便在没有此警告的情况下编译？

我当然可以通过取消隐藏参数来摆脱它，但这意味着我必须在任何地方指定显式参数，即使在不需要它的地方......