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]