智能合约适合哪种类型？
我在思考如何用Haskell或Idris等强类型语言来表达智能合约（这样你就可以将其编译以在以太坊网络上运行）。我的主要关注点是：有哪种类型能够涵盖合约可能会做的所有事情？ 天真的解决方案：EthIO 一个天真的解决方案是将合约定义为EthIO类型的成员。这种类型类似于Haskell的IO，但...
Agda和Idris之间的区别
我开始深入研究依赖类型编程，并发现Agda和Idris语言最接近Haskell，所以我从那里开始。 我的问题是：它们之间的主要区别是什么？它们的类型系统是否同样具有表现力？很好地进行全面比较并讨论其优点。 我已经能够发现一些差异： Idris具有类似于Haskell的类型类，而Agda...
单子变换器比效果更强大 - 有哪些例子呢？
该文章 "Programming and reasoning with algebraic effects and dependent types"讨论了Idris中的效应，其中提到了以下（未经引用的）观点： 虽然 [效应和单子变换器]在能力上并不等价- 单子和单子变换器可以表达更多概...
为什么类型转换是一件坏事？
Agda和Idris都有效地禁止对Type类型的值进行模式匹配。看起来Agda总是匹配第一个情况，而Idris则会抛出错误。 那么，为什么typecase是不好的事情？这会破坏一致性吗？我没有找到关于这个问题的太多信息。
依赖类型可以证明您的代码符合规范，但是如何证明规范是正确的？
依赖类型通常被宣传为一种使您能够断言程序对规范的正确性的方法。举个例子，您被要求编写一个 排序列表 的代码 - 您可以通过将 "排序" 的概念编码为类型，并编写一个函数，如 List a -> SortedList a 来证明代码的正确性。但是，如何证明规范 SortedList 是正确...
当使用依赖类型语言编程时，我们如何克服编译时间和运行时间之间的差距？
据我所知，在依赖类型系统中，“类型”和“值”被混合在一起，我们可以将它们都视为“术语”。 但是有些事情我不太理解：在没有依赖类型的强类型编程语言（如Haskell）中，类型在编译时被确定（推断或检查），而值在运行时被确定（计算或输入）。 我认为这两个阶段之间必须存在差距。如果一个值是交互式...
Idris的实际应用举例
有没有一些可以用来学习和应用到一般/“实际世界”应用的 Idris 示例呢？ 我相当熟练于 Haskell，而 Idris 似乎借鉴了大量 Haskell 的思想。虽然官方的FAQ/文档很好，但是拥有一些更大的示例将非常有帮助。目标是尝试使用 Idris 进行实际软件开发。谢谢您。
如何开始依赖类型编程？
有一些 Idris 教程、Agda 教程和其他教程样式的论文，以及无休止地引用尚未学习的东西。我在所有这些中间爬行，大部分时间被数学符号和新术语卡住了，没有解释突然出现。也许我的数学不行 :-) 有没有一种有序的方法来进行依赖类型编程？就像你想学习 Haskell 时，从 “Teach yo...
类型参数和索引的区别是什么？
我对依赖类型还不熟悉，对于两者之间的区别感到困惑。似乎人们通常说一个类型是由另一个类型参数化和由某个值索引。但是，在依赖类型的语言中，类型和术语之间是没有区别的，对吗？参数和索引之间的区别是否是基本的？您能否为我展示一些编程和定理证明中意义差异的例子？
依赖类型：依赖对类型如何类比于不交并？
我一直在学习相关的类型，现在已经理解以下内容： 全称量词会被表示成依赖函数类型。 ∀(x:A).B(x) 的意思是 “对于类型为A的所有x都有一个类型为B(x)的值存在”。因此它被表示为一个函数，当给定任何类型为A的值x时，会返回一个类型为B(x)的值。 存在量词会...