问题标签 [agda]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
module - 用不同的元素类型实例化 Data.AVL 模块
Agda 文档提供了一些如何使用该Data.AVL
模块的示例:
http://darcsden.com/abel/AgdaPrelude/browse/README/AVL.agda
在示例中,模块在导入时被实例化一次,参数指定存储在树中的值的类型,以及键类型的顺序。
如何在同一个客户端模块中使用不同值类型的 AVL 树(例如字符串树和数字树)?
implicit - 等价证明中未解决的元变量
我正在尝试导出元素类型 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
来推导出 ≈ 参数的并集也是 ≈ 的证明。
但是,编译器似乎留下了一些未解决的元变量,不幸的是我并不真正了解如何阅读这些消息。我只是做错了什么(证明方式),还是我只需要明确提出一些论点,还是什么?
standard-library - 如何使用 Agda 的定界延续实现?
我们可以很容易地在 Agda 中实现一个分隔的延续 monad。
但是,没有必要这样做,因为 Agda“标准库”有一个定界延续 monad 的实现。然而,让我对这个实现感到困惑的是向DCont
类型添加了一个额外的参数。
我的问题是:为什么K
那里有额外的参数?我将如何使用该DContIMonadDCont
实例?我能否open
以某种方式在(全局)范围内获得类似于以下参考实现的内容?
我所有使用它的尝试都导致无法解决的元数据。
不使用 Agda“标准库”的分隔延续的参考实现。
agda - 如何证明列表拆分是有效的?
我在锻炼。这似乎是一件微不足道的事情(简化以表明问题显然在于列表拆分):
总而言之,我声明可以定义两个列表的排列,如果它们可以提供Permutation
具有一对相等元素的较小列表x
and y
,并且插入位置y
由zs
and确定ys
。
然后lemma-ripTop
(本来打算做一些完全不同的事情,但这里只是id
on Permutation
)需要证明给定 a Permutation
for a list ( y :: ys
) 的东西。
我不明白为什么 Agda 需要查看
zs ++ (y1 :: ys1) == y :: ys
(这是我得到的错误)-我认为这应该从类型声明和构造函数中清楚吗?即,既然Permutation xs (y :: ys)
是在输入中给出的,那么在构造函数中作为见证提供的拆分p::
应该加起来为y :: ys
.如何让 Agda 相信这个列表拆分是有效的?
错误信息:
set - 适当使用宇宙多态性
我已经在一个 Agda 项目上工作了几个星期,尽我所能地忽略关卡多态性。不幸的是(或者也许幸运的是)我似乎已经到了需要开始理解它的地步。
到目前为止,我只在需要它们作为第二个参数Rel
(或第三个参数REL
)时才使用级别变量。否则我就省略了,直接使用Set
。现在我有一些客户端代码可以显式量化各个级别a
,并尝试将某些类型的表单传递Set a
给我现有的代码,这些代码现在不够多态。在下面的示例中,quibble
代表客户端代码,并且_[_]×[_]_
是≈-List
我现有代码的典型代表,它仅使用Set
.
≈-List
在这里,我可以使用额外的级别参数扩展 的归纳定义,a
以便它可以采用 type 的类型参数Set a
,但是我不清楚输入和输出关系的宇宙应该如何变化。然后问题蔓延到更复杂的定义,例如_[_]×[_]_
我更不确定如何进行。
我应该如何概括给出的示例中的签名,以便quibble
编译?有没有我可以遵循的一般规则?我读过这个。
inheritance - 为代数结构声明记录类型的推荐约定
我想对比两种在 Agda 中为代数结构声明新记录类型的风格。
按照标准 Agda 包中使用的样式Algebra
,可以定义BoundedJoinSemilattice
如下:
使用这种方法,该字段的任何字段都BoundedJoinSemiLattice
与其他更抽象结构的字段重叠(直至重命名) ,例如Setoid
、和。为了将 a视为其“超类型”之一,必须调用一个投影函数,该函数负责将其字段映射到超类型的字段,例如上面的函数。Semigroup
Monoid
CommutativeMonoid
BoundedJoinSemiLattice
BoundedJoinSemiLattice
commutativeMonoid
但是,这种字段重复可能会导致代码中出现大量样板,这些样板会从不太具体的代数结构中构建出更具体的代数结构。更自然的定义可能是这样的(重命名CommutativeMonoid
为CM
):
这里的想法不是复制CommutativeMonoid
into的字段BoundedJoinSemilattice
,而是让后者声明一个 type 的字段CommutativeMonoid
。然后我们使用 anopen...public
将其子字段“继承”到包含记录中。事实上,这正是标准库中其他地方使用的惯用语Algebra.Structures
,除了这里我们还重命名了继承的字段,以便在继承上下文中适当地命名它们。
第二种方法不仅不那么冗余,而且现在想要BoundedJoinSemilattice
从 a构造 a 的客户端代码CommutativeMonoid
可以简单地将其作为参数传递给正在构造的记录。另一方面,想要BoundedJoinSemilattice
从头构造 a 的客户端代码现在必须构造一个中间CommutativeMonoid
.
Algebra
模块不使用这种继承风格 是有原因的Algebra.Structures
吗?也许第二种方法存在我没有发现的问题,或者它没有太大区别:例如,对于第一种方法,也许可以简单地定义一个“构造函数”来处理BoundedJoinSemiLattice
从 a 构造 a CommutativeMonoid
,恢复了第二种方法的很多便利。
macros - 带中缀符号的二元运算符索引系列
假设您要定义一系列二元运算符(例如,由集合索引),其中参数的类型取决于索引的值,并且索引是显式传递的。此外,假设您希望家庭成员可以使用中缀表示法:
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
。
agda - 子集的类型
有没有办法让函数要求两个Setoid
s,其中第一个Setoid
相等意味着后者相等?当然这要求两个Setoid
s 共享它们Carrier
,Carrier
而不是一个参数,而是一个记录字段。请求相等的天真尝试Carrier
被类型检查器拒绝:
这不行,因为我们在等式证明上没有进行模式匹配,所以不同的Carrier
类型不统一。我还没有找到一种方法来表达这一点subst
。
proof - 在 Agda 中定义记录时未解析的元数据
考虑以下代码:
当加载 Agda(版本 2.3.2.2)时,Agda 打印与倒数第二行有关的错误“Unsolved metas at the following locations”:
并特别指向 assoc+。
如何提供提示或以其他方式更改代码以便在没有此警告的情况下编译?
我当然可以通过取消隐藏参数来摆脱它,但这意味着我必须在任何地方指定显式参数,即使在不需要它的地方......