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

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

我已经能够发现一些：

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

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

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

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

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

我在说的是无法定义：

我知道 GHC 只是将其简化为普通函数，解决此问题的惯用方法是：

写完后我不太喜欢它……这种类型分类不能成为脱糖过程的一部分吗？

当我写一些 Aeson JSON 解析时，我想到了。如果只为每种数据类型派生FromJSON实例太容易了，我必须手动写出所有内容（目前 > 1k 行并计数）。在数据记录中具有类似name或简单的名称value并不少见。

http://www.haskell.org/haskellwiki/Performance/Overloading提到函数重载会引入一些运行时开销。但我实际上不明白为什么编译器无法在编译时解决这个问题并在内部给它们不同的名称。

这个 2012 年的 SO 问题或多或少地说明了历史原因，并指向了 2006 年的一个邮件线程。最近有什么变化吗？

即使会有一些运行时开销，大多数人也不会介意，因为大多数代码几乎不是性能关键。

是否有一些隐藏的语言扩展实际上允许这样做？我再次不确定......但我认为伊德里斯实际上是这样做的？

是否有任何Idris示例可用于研究并可能将其应用于通用/“现实世界”应用程序？

我对 Haskell 相当精通，Idris 似乎大量借用了 Haskell，官方的常见问题解答/文档相当不错，但如果有一些更大的示例可供探索，将会非常有帮助。目标是尝试将 Idris 用于实际的软件开发。TIA。

我希望伊德里斯证明那里testMult : mult 3 3 = 9有人居住。

不幸的是，这被键入为

我可以像这样解决它：

有没有办法做类似的事情mult (3 : Nat) (3 : Nat) = (9 : Nat)？

我正在尝试将Cayenne 中的一个示例翻译成 Idris - 一种具有依赖类型的语言 论文。

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

我使用而List Char不是格式参数来促进模式匹配，因为我很快就遇到了模式匹配的复杂性。StringString

不幸的是，我收到一条我无法理解的错误消息：

如果我在and中注释掉所有带有 3 个元素（带有'%' :: ...）的模式匹配案例，那么代码就会编译（但显然没有做任何有趣的事情）。PrintfTypeprintf

如何修复我的代码以使其printf "the %s is %d" "answer" 42正常工作？

我正在尝试使用官方教程中提供的安装指南在 OSX Lion 中安装 Idris 语言。我已经安装了GMP。这是我得到的错误：

尝试在没有 LLVM 的情况下安装 Idris 会产生此错误：

我很感兴趣，因为我想检查 Prelude 中内置函数的定义。

我搜索了它，但只在 ~/.cabal/share/idris 中找到了预编译文件...

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

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

它似乎有效：

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

我看到几个不同的研究小组，以及至少一本书，都在谈论使用 Coq 来设计认证程序。对于认证项目的定义是否有共识？据我所知，它真正的意思是程序被证明是完全的并且类型正确。现在，程序的类型可能是非常奇特的东西，例如证明它是非空的、已排序的、所有元素 >= 5 等的列表。但是，最终，它是一个经过认证的程序，只有 Coq 显示的是完全的和类型安全的，所有有趣的问题都归结为最终类型中包含的内容？

编辑 1

根据 wjedynak 的回答，我查看了 Xavier Leroy 的论文“Formal Verification of a Realistic Compiler”，该论文链接在下面的答案中。我认为这包含了一些很好的信息，但我认为可以在Sandrine Blazy 和 Xavier Leroy的论文Mechanized Semantics for the C 语言的 Clight 子集中找到更多信息。这是“形式验证”论文添加优化的语言。在其中，Blazy 和 Leroy 介绍了 Clight 语言的语法和语义，然后在第 5 节讨论这些语义的验证。在第 5 节中，列出了用于验证编译器的不同策略，. 这些是：

1. 人工审核
2. 证明语义的性质
3. 已验证的翻译
4. 测试可执行语义
5. 与替代语义等价

无论如何，可能有几点可以补充，我当然想了解更多。

回到我最初的问题，即认证程序的定义是什么，我仍然有点不清楚。Wjedynak 提供了一个答案，但实际上 Leroy 的工作涉及在 Coq 中创建一个编译器，然后在某种意义上对其进行验证。理论上，现在证明关于 C 程序的事情成为可能，因为我们现在可以进行 C->Coq->proof。从这个意义上说，似乎有这个工作流程我们可以

1. 用X语言编写程序
2. Coq 或其他证明辅助工具中步骤 1 中程序模型的形式。这可能涉及在 Coq 中创建编程语言模型，也可能涉及直接创建程序模型（即在 Coq 中重写程序本身）。
3. 证明模型的一些性质。也许这是对价值观的证明。也许这是陈述等价性的证明（诸如 3=1+2 或 f(x,y)=f(y,x) 之类的东西。）
4. 然后，根据这些证明，调用认证的原始程序。

或者，我们可以在证明辅助工具中创建程序的规范，然后证明关于该规范的属性，而不是程序本身。

无论如何，如果有人有替代定义，我仍然有兴趣听到它们。