Our website is made possible by displaying online advertisements to our visitors.
Please consider supporting us by disabling your ad blocker.
Idris
| 编程范型 | 函数式编程 |
|---|---|
| 設計者 | Edwin Brady |
| 发行时间 | 2007年[1] |
| 当前版本 |
|
| 型態系統 | 静态类型, 强类型, 依赖类型 |
| 操作系统 | 跨平台 |
| 許可證 | BSD-3 |
| 文件扩展名 | .idr, .lidr |
| 網站 | Idris |
| 啟發語言 | |
| Agda, Coq, Epigram, Haskell, ML | |
預覽警告：页面使用了Template:Infobox programming language不存在的参数"latest_test_version"
預覽警告：页面使用了Template:Infobox programming language不存在的参数"latest_test_date"
預覽警告：页面使用了Template:Infobox programming language不存在的参数"latest_release_date"
預覽警告：页面使用了Template:Infobox programming language不存在的参数"latest_release_version"
Idris是一个通用的依赖类型纯函数式编程语言，其类型系统与Agda以及Epigram相似。
Idris语言具备堪与Coq媲美的交互式定理证明能力，自带tactics，而其设计目标侧重于通用系统编程更甚于辅助证明。Idris的其他设计目标还包括“可观的”代码性能，对副作用的控制，以及对于实现嵌入式领域特定语言（Embedded Domain Specific Language，EDSL）的支持。
Idris通过一个依赖类型的核心语言TT生成C语言的中间代码并编译到本地机器码，并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java和LLVM的编译器后端。[4]
Idris的名字来自于20世纪70年代的英国儿童动画片《火车头艾弗》里，一条会唱歌的龙。[5]
- ^ Brady, Edwin. Index of /~eb/darcs/Idris. University of St Andrews School of Computer Science. 2007-12-12. （原始内容存档于2008-03-20）.
- ^ Release 1.3.3. 2020年5月23日 [2020年5月24日].
- ^ Release 1.3.3. [2020-05-25]. （原始内容存档于2021-02-04）.
- ^ Idris - News. [2013-12-24]. （原始内容存档于2013-12-24）.
- ^ Idris - FAQ. [2013-12-24]. （原始内容存档于2012-03-11）.
Previous Page Next Page
