构建 Idris 2 应用程序

关于使用 Control.App 构建Idris 2应用程序的教程。

备注

Idris 的文档已在知识共享 CC0 许可下发布。因此，在法律允许的范围内，Idris 社区 已经放弃了 Idris 文档的所有版权和相关或邻近的权利。

关于CC0的更多信息，可以在网上找到：http://creativecommons.org/publicdomain/zero/1.0/

Idris 应用程序有 main : IO () 作为一个入口点， 类 型 IO a 是对交互式操作的描述，它产生一个类型 a 的值。这对原语来说很好，但 IO 不支持异常，所以我们必须明确说明一个操作如何处理失败。另外，如果我们确实想支持异常，我们也要解释异常和线性（见章节 多重性 ）如何交互。

在本教程中，我们描述了一个参数化类型 App 和一个相关的参数化类型 App1 ，它们共同允许我们在考虑到异常和线性的情况下构造更大的应用程序。 App 和 App1 的目的是：

  • 使得在其类型中表达一个函数所做的交互成为可能，而没有太多的符号开销。

  • 与写在 IO 中相比，几乎没有性能开销。

  • 与其他副作用相关的库和技术兼容，如代数副作用『algebraic effects』或单子变压器『monad transformers』。

  • 足够易于使用和性能，它可以成为 所有 进行外部函数调用的库的基础，就像 IO 在 Idris 1 和 Haskell 中一样

  • 与线性类型兼容，也就是说，它们应该表达一段代码是否是线性的（保证只执行一次而不抛出异常）或是否可能抛出异常。

我们首先介绍 App ，用一些小的示例程序，然后展示如何用异常、状态和其他接口来扩展它。