Idris

您可以在Wikipedia上了解到此条目的英文信息 Idris Thanks, Wikipedia.

Idris programming language

简介

Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。

Idris 语言具备堪与 Coq 媲美的交互式定理证明能力，自带 tactics，而其设计目标侧重于通用系统编程更甚于辅助证明。Idris 的其他设计目标还包括可观的代码性能，对副作用的控制，以及对于实现嵌入式领域特定语言（Embedded Domain Specific Language，EDSL）的支持。

Idris 语言使用 Haskell 编写实现，采用 BSD licenses 许可证。

功能

• Theorem Proving（定理证明）
• 通过允许程序员描述对象语言的类型系统来帮助嵌入式 DSL 开发
• Idris 2 is based on Quantitative Type Theory (QTT) 量化类型理论

项目

• Coq
• Agda

链接

• Idris 官网
• Idris @ GitHub