Idris的实际应用举例

Question

有没有一些可以用来学习和应用到一般/“实际世界”应用的 Idris 示例呢？

我相当熟练于 Haskell，而 Idris 似乎借鉴了大量 Haskell 的思想。虽然官方的FAQ/文档很好，但是拥有一些更大的示例将非常有帮助。目标是尝试使用 Idris 进行实际软件开发。谢谢您。

- Arets Paeglis

---

我也处于类似的位置，相对熟练掌握 Haskell（了解 GADT、Type Families 等），并希望在 Idris 中探索完全依赖类型。找到更多的例子会很不错。 - MFlamer

仅供参考，这里有一个关于使用Agda编写的实际程序的相关问题（不幸已关闭）。 - Joachim Breitner

Answer 1

Edwin Brady在 https://github.com/edwinb/idris-demos 上拥有一个示例代码仓库，其中包括一个可玩的太空侵略者游戏。这个游戏使用了SDL绑定、Effect以及!-effect语法（这基本上是一种替代do-notation / >>=的语法）。

此外，我们试图在维基上维护一份可用库列表：https://github.com/idris-lang/Idris-dev/wiki/Libraries

- pdxleif

---

也许“绑定操作符”是"!"语法的更好称呼：bang源自"!"，binding意为它变成了">>="（来自David Christiansen在#idris频道的解释）。 - pdxleif

Answer 2

Edwin Brady是Idris的创造者，他写了一篇关于现实世界问题（如效率和并发性）的论文："使用依赖类型验证有副作用资源使用协议的实现：通过正确构建实现来保证并发性"。这篇论文不仅解释了如何处理并发性，还在Idris中创建了一个嵌入式特定领域语言(EDSL)来处理并发性。

它也被用于科学计算（可能或可能不符合实际应用要求）：依赖类型编程在科学计算中。这篇论文包含了实际的例子和一些Agda的例子。

2022年更新：现在在github上有一个很棒的列表。

- scravy