Are*_*lis 41 dependent-type idris
是否有任何可用于研究并可能将其用于通用/"现实世界"应用的Idris的例子？
我对Haskell有一定的精通,其中Idris似乎借用了很多,官方常见问题/文档相当不错,但是有一些更大的例子可供探讨.目标是尝试使用Idris进行实际的软件开发.TIA.
pdx*_*eif 25
Edwin Brady在https://github.com/edwinb/idris-demos上有一个充满演示的回购.除此之外,它还有一个可玩的太空入侵者游戏,使用SDL绑定,效果和!-effect语法编写(基本上是do-notation/>> =的替代语法).
此外,我们尝试在维基上维护一些可用库的列表:https: //github.com/idris-lang/Idris-dev/wiki/Libraries
scr*_*avy 16
伊德里斯的创建者Edwin Brady撰写了一篇论文,论述了效率和并发等现实问题:"构建并发正确:使用依赖类型来验证有效资源使用协议的实现".它不仅解释了如何处理并发,还在Idris中创建了一个嵌入式域特定语言(EDSL)来处理并发.
它还用于科学计算(可能或可能不符合现实世界的应用程序):科学计算中的依赖型编程.本文还包含实际示例和一些Agda示例.