Idris
维基百科,自由的 encyclopedia
Idris是一个通用的依赖类型纯函数式编程语言,其类型系统与Agda以及Epigram(英语:Epigram (programming language))相似。
Quick Facts 编程范型, 设计者 ...
编程范型 | 函数式编程 |
---|---|
设计者 | Edwin Brady |
发行时间 | 2007年,17年前(2007)[1] |
当前版本 |
|
型态系统 | 静态类型, 强类型, 依赖类型 |
操作系统 | 跨平台 |
许可证 | BSD-3 |
文件扩展名 | .idr, .lidr |
网站 | Idris |
启发语言 | |
Agda, Coq, Epigram(英语:Epigram (programming language)), Haskell, ML |
Close
Idris语言具备堪与Coq媲美的交互式定理证明能力,自带tactics,而其设计目标侧重于通用系统编程更甚于辅助证明。Idris的其他设计目标还包括“可观的”代码性能,对副作用的控制,以及对于实现嵌入式领域特定语言(Embedded Domain Specific Language,EDSL)的支持。
Idris通过一个依赖类型的核心语言TT生成C语言的中间代码并编译到本地机器码,并利用了一个基于Cheney算法的垃圾收集器实现。Idris亦拥有 JavaScript、Java和LLVM的编译器后端。[4]
Idris的名字来自于20世纪70年代的英国儿童动画片《火车头艾弗(英语:Ivor_the_Engine#Idris_the_Dragon)》里,一条会唱歌的龙。[5]