Idris Idris是一个通用的依赖类型纯函数式编程语言其类型系统与Agda以及Epigram英语Epigram programming language相似 Idris语言具备堪与Coq媲美的交互式定理证明能力自带tactics而其设计目标侧重于通用系统编程更甚于辅助证明Idris的其他设计目标还包括可观的代码性能对副作用的控制以及对于实现嵌入式领域特定语言Embedded Domain Specific LanguageEDSL的支持 Idris通过一个依赖类型的核心语言TT生成C语言的中间代码并编译到本地机器码并利用了一个基于Cheney算法的垃圾收集器实现Idris亦拥有 JavaScriptJava和LLVM的编译器后端 Idris的名字来自于世纪年代的英国儿童动画片火车头艾弗英语IvortheEngineIdristheDragon里一条会唱歌的龙