伊德里斯的实际例子答案

【问题标题】：Practical examples of Idris伊德里斯的实际例子
【发布时间】：2013-06-07 07:24:29
【问题描述】：

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

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

【问题讨论】：

【解决方案1】：

Edwin Brady 在https://github.com/edwinb/idris-demos 上有一个充满演示的 repo。除此之外，它还有一个可玩的太空入侵者游戏，使用 SDL 绑定、效果和 !-effect 语法（基本上是 do-notation / >>= 的替代语法）编写。

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

【讨论】：

也许“bang-binding”是一个更好的名字！语法：从 ! 开始，绑定，因为它变成 >>=（来自 #idris 频道的 David Christiansen 的解释）。

【解决方案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 示例。

【讨论】：