是否有任何Idris示例可用于研究并可能将其应用于通用/“现实世界”应用程序？
我对 Haskell 相当精通，Idris 似乎大量借用了 Haskell，官方的常见问题解答/文档相当不错，但如果有一些更大的示例可供探索，将会非常有帮助。目标是尝试将 Idris 用于实际的软件开发。TIA。
问问题
6888 次
2 回答
28
Edwin Brady 在https://github.com/edwinb/idris-demos有一个充满演示的 repo 。除此之外，它还有一个可玩的太空侵略者游戏，使用 SDL 绑定、效果和 !-effect 语法（基本上是 do-notation / >>= 的替代语法）编写。
此外，我们尝试在 wiki 上维护一些可用库的列表： https ://github.com/idris-lang/Idris-dev/wiki/Libraries
于 2014-03-01T00:17:19.013 回答
18
Idris 的创建者 Edwin Brady 有一篇论文处理了现实世界中的问题，例如效率和并发性：“Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effective Resource Usage Protocols”。它不仅解释了如何处理并发，而且还在 Idris 中创建了一种嵌入式域特定语言 (EDSL) 来处理并发。
它也用于科学计算（可能有资格或可能没有资格作为现实世界的应用程序）：科学计算中的依赖类型编程。该论文包含实际示例和一些 Agda 示例。
于 2013-06-16T16:01:13.490 回答