问题标签 [agda]

Agda归纳数据类型和模式匹配手册说明：

为了确保归一化，感应事件必须出现在严格的正位置。例如，不允许使用以下数据类型：

因为在构造函数的参数中有一个负面的 Bad 出现。

为什么这个要求对于归纳数据类型是必要的？

由于_+_-Operation forNat通常是在第一个参数中递归定义的，因此类型检查器知道它显然不是微不足道的i + 0 == i。但是，当我在固定大小的向量上编写函数时，我经常遇到这个问题。

一个例子：我如何定义一个 Agda 函数

哪个将第一个n值放在向量的末尾？

由于 Haskell 中的一个简单解决方案是

我在 Agda 中类似地尝试过，如下所示：

但是类型检查器失败并显示消息（与{zero}上述swap-Definition 中的 -case 相关）：

所以，我的问题是：如何教 Agda m == m + zero？以及如何swap在 Agda 中编写这样的函数？

我写了一个 Agda 函数prefixApp，它将向量函数应用于向量的前缀：

我喜欢这样一个事实，它prefixApp可以在不明确提供长度参数的情况下使用，例如

（xorV : Vec Bool 2 -> Vec Bool 1向量异或函数在哪里）

不幸的是，我不知道如何编写一个postfixApp可以在不显式提供长度参数的情况下使用的函数。到目前为止，我的函数定义如下所示：

然而，这似乎postfixApp总是需要一个长度参数。例如

有谁知道如何消除这种不对称性，即如何编写一个postfixApp没有显式长度参数的函数。我想，我需要另一个split-function？

我有下一个定义：

很容易证明下一个引理：

但我找不到证明下一个引理的方法：

我可以将定义更改<=为下一个：

在那种情况下，我可以证明lem-prev'：

但现在我无法证明lem-prev。

有没有办法证明<=和/或的引理<='？如果不是，那么我应该如何更改定义以使其成为可能？

添加：使用 hammar 的辅助引理的解决方案：

我试图证明一些关于使用可判定相等性的函数的简单事情。这是一个非常简化的示例：

现在，我试图证明这样的事情，我已经证明了两边_≟_是相同的。

此时，当前的目标是(check ds x x | x ≟ x) ≡ something。如果x ≟ x它本身是，我会使用类似的东西来解决它refl，但在这种情况下，我能想到的最好的东西是这样的：

就其本身而言，这并没有那么糟糕，但是在一个更大的证明中它是一团糟。当然必须有更好的方法来做到这一点？

我有两个密切相关的问题：

首先，Haskell 的 Arrow 类如何在 Agda 中建模/表示？

（以下博客文章指出它应该是可能的......）

其次，在 Haskell 中，(->)是一等公民，只是另一种高阶类型，它可以直接定义(->)为Arrow类的一个实例。但是在阿格达呢？我可能是错的，但我觉得 Agdas->是 Agda 的一个更不可或缺的部分，而不是 Haskell 的->。那么，是否可以将 Agdas->视为一种高阶类型，即产生Set可以作为 的实例的类型函数Arrow？

我编写了一个 Agda 函数applyPrefix，将一个固定大小向量函数应用于向量大小为的较长向量的初始部分m，n并且k 可能保持隐式。这是定义和辅助函数split：

我需要一个对称函数applyPostfix，它将固定大小的向量函数应用于较长向量的尾部。

正如applyPrefix已经表明的定义，k-Argument 在使用时不能保持隐含applyPostfix。例如：

有谁知道一种技术，如何实现applyPostfix以使k- 参数在使用时保持隐式applyPostfix？

我所做的是校对/编程：

并在定义时使用该引理applyPostfix：

不幸的是，这没有帮助，因为我使用k-Parameter 来调用引理:-(

任何更好的想法如何避免k明确？也许我应该在 Vectors 上使用 snoc-View？

有一个 Idris 教程、一个 Agda 教程和许多其他教程风格的论文和介绍性材料，其中不断引用尚未学习的东西。我有点在所有这些中间爬行，而且大多数时候我都被数学符号和突然出现的新术语所困，没有任何解释。也许我的数学很烂:-)

是否有任何规范的方法来处理依赖类型编程？就像当你想学习 Haskell 时，你从“自学 Haskell”开始，当你想学习 Scala 时，你从 Odersky 的书开始，对于 Ruby，你阅读那个带有变异错误的奇怪教程。但我不能从他们的书开始 Agda 或 Idris。他们在我的头上。我尝试了 Coq 并陷入了它的所有关于 teorm 证明的风格。Agda 需要大量的数学背景，而 Idris，好吧，让我们暂时离开吧！

我非常了解静态类型系统，我精通 Scala，如有必要，我可以使用 Haskell。我了解函数范式并每天使用它，我了解代数数据类型和 GADT（实际上非​​常顺利），并且我最近设法理解了 Lambda Cube。不过，我缺乏数学和逻辑部分。

我想在CoList (Maybe Nat)s 上定义一个仅考虑justs 的相等性。当然，我不能只是从CoList (Maybe A)to 开始CoList A，因为那不一定是富有成效的。

那么，我的问题是如何定义这样的等价关系（不考虑可判定性）？如果我可以将无限just尾视为不等价，它是否有帮助？

下面的@gallais 建议我应该能够天真地定义这种关系：

但是证明它的传递性会从终止检查器中进入（预期的）问题：

所以我试着让双方都不nothing那么模棱两可的情况（就像@Vitus建议的那样）：

但现在我不知道如何定义有问题的情况trans（我留下一个洞的情况）

在 ICFP 2012 上，Conor McBride 发表了主题演讲，主题为“Agda-curious？”。

它具有小型堆栈机器实现。

该视频在 youtube 上： http ://www.youtube.com/watch?v=XGyJ519RY6Y

代码也在线： http: //personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz

我想知道run第 5 部分的功能（即“Part5Done.agda”，如果您下载了代码）。run在解释功能之前谈话停止。

该函数的正确类型签名是run什么？功能应该如何run实现？

编译功能在演讲开始后大约 55 分钟进行了解释。

完整代码可从 Conor 的网页获得。