Idris的实际示例

Question

有没有什么Idris的例子可以用来研究或者将其应用于一般目的/“现实世界”应用程序？

我精通Haskell，Idris似乎借用了大量的Haskell，官方的FAQ/文档相当不错，但如果有一些更大的例子来探索会非常有帮助。目标是尝试使用Idris进行实际的软件开发。蒂娅。

Answer 1

Edwin Brady在https://github.com/edwinb/idris-demos上有一大堆演示。其中，它有一个可玩的空间入侵者游戏，使用SDL绑定、效果和!-effect语法(基本上是do-notation />>=的替代语法)编写。

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

Answer 2

Idris的创建者Edwin Brady有一篇论文，讨论了诸如效率和并发性等现实世界的问题："Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols"。它不仅解释了如何处理并发性，还在Idris中创建了嵌入式领域特定语言(EDSL)来处理并发性。

它还用于科学计算(这可能是也可能不是真正的应用程序)：Dependently-typed programming in scientific computing。本文包含实际示例和几个Agda示例。