Idris

2022年9月25日 (日) 16:50的最后版本

您可以在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) 量化类型理论

[编辑] 指南

[编辑] 项目

• Idris @ GitHub
• 相似项目:Coq, Agda

[编辑] 文档

• Idris 2: Quantitative Type Theory in Action

[编辑] 图集

[编辑] 链接

• Idris 官网