问题标签 [agda]

我对依赖类型的语言感兴趣。有限数字对我来说似乎非常有用。例如，安全地索引固定大小的数组。但是这个定义对我来说不是很清楚。

Idris 中有限数的数据类型如下：（在 Agda 中可能类似）

它似乎有效：

但这是如何工作的？k 是什么意思？为什么类型检查器接受第一个实现而拒绝第二个实现？

我将 Emacs 与 一起使用agda-mode，并编写了这个函数：

Nat,succ并且*被定义为与 Agda 的自然数内部定义兼容。

当我评估时，(pow 2 100000)我得到一个堆栈溢出错误。但是，鉴于递归调用是尾调用，我希望 agda 解释器优化pow'成一个循环。

如何启用此优化？

是否有一种类型化的编程语言，我可以像以下两个示例一样约束类型？

1. 概率是一个浮点数，最小值为 0.0，最大值为 1.0。

   /li>

2. 离散概率分布是一个映射，其中：键都应该是相同的类型，值都是概率，并且值的总和 = 1.0。

   /li>

据我了解，这对于 Haskell 或 Agda 是不可能的。

是否有函数式语言可以在类型检查器中指定某个计算是否保证终止？或者，您可以仅在 Haskell 中执行此操作吗？

关于 Haskell，在这个答案中，张贴者说

通常的思考方式是每个 Haskell 类型都被“提升”——它包含 ⊥。也就是说，Bool对应于{⊥, True, False}而不是仅仅{True, False}。这代表了 Haskell 程序不能保证终止并且可能有异常的事实。

另一方面，这篇关于 Agda的论文指出

一个正确的 Agda 程序是一个同时通过类型检查和终止检查的程序

即，所有的 Agda 程序都会终止，而BoolAgda 中的 a 正好对应{True, False}.

例如，在 Haskell 中你可以有一个 type 的值IO a，它告诉类型检查器需要 IO 来计算有问题的值。你能有一个类型Lifted a断言有问题的计算可能不会终止吗？也就是说，您允许不终止，但在类型系统中将其分开。（显然，就像在 Agda 中一样，您只能将值分为“绝对终止”和“可能不终止”）如果不是，是否有语言可以做到这一点？

假设我们定义一个函数

Agda 将在鲑鱼中绘制 f，因为它无法判断 n/2 是否小于 n。我不知道如何告诉 Agda 的终止检查器任何事情。我在标准库中看到他们有一个除以 2 和一个证明 n/2 < n。但是，我仍然看不到如何让终止检查器意识到已经对较小的子问题进行了递归。

从我收集到的关于 agda 的点点滴滴的信息中，我（显然是错误地）得出结论，这∀ {A}相当于{A : Set}. 现在我注意到了

是无效的（关于 Set\omega 的东西又似乎是一些内部的东西，但是

很好。谁能帮我解决这个问题？

这就是我所理解的Relation.Binary.PropositionalEquality.TrustMe.trustMe：它似乎需要一个任意的xandy和：

• 如果x和y真正相等，则变为refl
• 如果不是，它的行为就像postulate lie : x ≡ y.

现在，在后一种情况下，它很容易使 Agda 不一致，但这本身并不是一个问题：它只是意味着任何使用trustMe的证明都是诉诸权威的证明。而且，虽然你可以用这样的东西来写coerce : {A B : Set} -> A -> B，但事实证明，情况coerce {ℕ} {Bool} 0并没有减少（至少，不是根据 Cc Cn），所以它真的不像 Haskell 的语义跺脚unsafeCoerce。

那我有什么好害怕的trustMe？另一方面，有没有理由在实现原语之外使用它？

没有其他游戏比ADOM 更让我印象深刻，因为它几乎可以用无穷无尽的方式与它的世界互动。仅举几例：如果您有防水毯子，您的物品就不会在雨中生锈，您可以砍树建桥、将武器浸入药水、踢锁门等。

由于交互如此复杂，每个新功能都可能需要重构、重新编译，然后导致测试中断、错误等。这似乎是表达式问题的一个有趣案例。

问题：

表达式问题的解决方案可以在 Agda 或 Haskell 中表达为可重用库或设计模式吗？

我试图证明整数的可分性。首先，我试图证明可分性是反射性的。

因为我根据减法定义了除法...

...如果我使用以下事实似乎很容易n-n=0：

但是 Agda 拒绝在 refl 上进行模式匹配。即使没有其他可能的范式n-n=0 n。我已经用其他功能证明了这一点。我只需要使用n-n=0.

笔记：

• a - b定义为a + (neg b)
• 我已经证明了n-n≡0 : (n : ℤ) → n - n ≡ zero