Idris (プログラミング言語)
From Wikipedia, the free encyclopedia
| パラダイム | 関数型 |
|---|---|
| 登場時期 | 2007年[1] |
| 設計者 | Edwin Brady |
| 最新リリース | 1.3.4[2]/ 2021年10月22日 |
| 評価版リリース | 0.6.0 (Idris 2)[3] / 2022年10月28日 |
| 影響を受けた言語 | Agda, Clean[4], Coq[5], Epigram, F#, Haskell[5], ML[5], Rust[4] |
| プラットフォーム | Cross-platform |
| ライセンス | BSD |
| ウェブサイト |
idris-lang |
| 拡張子 | .idr, .lidr |
Idrisは依存型やオプショナルな遅延評価、全域性チェッカーを特徴とする純粋関数型プログラミング言語である。Idrisは証明アシスタントとしても使われるが、 Haskellのように汎用プログラミング言語として設計されている。
Idrisの型システムはAgdaに、証明はCoqに似ていて、elaboratorリフレクションによるタクティクスを含む[6]。AgdaやCoqと比べ、Idrisは副作用管理と内部ドメイン固有言語のサポート重点を置いている。 IdrisはC言語 (Cheneyのアルゴリズムを使ったコピーガベージコレクタに依存) とJavaScript (ブラウザーとNode.jsの両方) にコンパイルされる。JVMや、CIL、LLVMを含む他のプラットフォーム用のコード生成器もある[7]。