问题标签 [agda]

我正在努力学习agda。但是，我遇到了一个问题。我在 agda wiki 上找到的所有教程对我来说都太复杂了，并且涵盖了编程的不同方面。在并行阅读了 3 篇关于 agda 的教程后，我能够编写简单的证明，但我仍然没有足够的知识来使用它来实现真实单词算法的正确性。

你能推荐我关于这个主题的任何教程吗？类似于 Learn Yourself a Haskell 但适用于 Agda 的东西。

我开始深入研究依赖类型编程，发现 Agda 和 Idris 语言最接近 Haskell，所以我从那里开始。

我的问题是：它们之间的主要区别是什么？类型系统在它们中是否同样具有表现力？对收益进行全面的比较和讨论会很棒。

我已经能够发现一些：

• Idris 具有类似于 Haskell 的类型类，而 Agda 具有实例参数
• Idris 包括单子和应用符号
• 它们似乎都有某种可重新绑定的语法，尽管不确定它们是否相同。

编辑：这个问题的 Reddit 页面中有更多答案：http ://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

假设我有一个函数（它确实像名字所说的那样）：

现在，我想以某种方式与我返回的依赖对一起工作。我写了简单的head函数：

这当然可以完美地工作。但这让我想知道：有什么方法可以确保该函数只能用 调用n ≥ 1？

理想情况下，我想做函数head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A；但这失败了，因为n当我在IsTrue.

谢谢你的时间！

IsTrue是这样的：

我发现了很多关于使用 Agda 作为证明系统的有用信息。我几乎没有发现关于使用 Agda 编写可用程序的信息。我什至找不到与最新版本的 Agda 一起编译的“hello world”示例。

所以，

1. 有没有关于 Agda 作为编程语言的好教程？

2. 是否有其他类似性质的语言（惰性函数依赖类型）具有更成熟的文档以将它们用作编程语言？（我在 Coq 上找到了大量很棒的文档，但同样没有“Hello World”）。

当我编译一个使用标准库的 Agda 程序时，编译器会花费很长时间打印出如下行：

我猜它安全“跳过”它们的原因是它们已经编译（目录中已经有 .agdai 文件）。但它仍然会花费大量时间跳过它们，并且编译需要一分钟以上。

有没有办法在每次编译时避免所有这些额外的工作？

找出导致未解决的元数据的最佳方法是什么？有没有办法通过扩展所有可解决的周围通配符将所有未解决的元数据（并且只有未解决的元数据）变成孔？

如果不出意外，将未解决的元数据更改为漏洞是否会使有关未解决的元数据的消息消失？因为那时我想我可以尝试将每个通配符和每个隐式参数都更改为漏洞，直到消息消失，然后找出导致问题的原因...

我正在证明 和 的一些性质filter，map一切都非常顺利，直到我偶然发现了这个性质：filter p (map f xs) ≡ map f (filter (p ∘ f) xs). 这是相关的代码的一部分：

现在，因为我喜欢使用该≡-Reasoning模块编写证明，所以我尝试的第一件事是：

但很可惜，这并没有奏效。试了一个小时，终于放弃了，用这种方式证明：

仍然好奇为什么通过≡-Reasoning没有工作，我尝试了一些非常微不足道的事情：

但是 typechecker 不同意我的看法。似乎当前目标仍然存在filter p (f x ∷ map f xs) | p (f x)，即使我在 上进行模式匹配p (f x)，filter也不会减少到f x ∷ filter p (map f xs).

有没有办法让这个工作≡-Reasoning？

谢谢！

我在 Windows 7 64 位电脑上运行 Agda 时遇到问题。我尝试运行以下命令：

和

两者都有效，但我似乎仍然无法使用 emacs，有人可以帮助我吗？我已经尝试过这里的一键安装程序，但它似乎不起作用，我遇到了这个投诉：

我试图在商类型上定义具有多个参数的函数。使用柯里化，我可以将问题减少到在逐点积 setoid 上定义函数：

我的问题是，有没有办法在×-quot不假设外延性的情况下证明它的合理性？

我们必须把这个haskell数据类型转换成agda代码：

这是我到目前为止所拥有的：

但是我收到了这个错误：“Set 应该是一个函数类型，但是当检查 true 是 Set 类型函数的有效参数时，它不是”。我认为 Set 需要更改为其他内容，但我对这应该是什么感到困惑。