利用者:Tlorr/Idris (プログラミング言語)
 |
| パラダイム | 関数型 |
|---|---|
| 登場時期 | 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]
関連項目
[編集]参考文献
[編集]- ^ Brady, Edwin (2007年12月12日). “Index of /~eb/darcs/Idris”. University of St Andrews School of Computer Science. 2008年3月20日時点のオリジナルよりアーカイブ。2023年5月14日閲覧。
- ^ “Release 1.3.4”. 2022年12月31日閲覧。
- ^ “Idris 2 version 0.6.0 Released”. www.idris-lang.org. 2022年12月31日閲覧。
- ^ a b “Uniqueness Types”. Idris 1.3.1 Documentation. 2019年9月26日閲覧。
- ^ a b c “Idris, a language with dependent types”. 2014年10月26日閲覧。
- ^ “Elaborator Reflection — Idris 1.3.2 documentation”. 27 April 2020閲覧。
- ^ “Code Generation Targets — Idris Latest documentation”. docs.idris-lang.org. 2023年5月14日閲覧。
外部リンク
[編集]- Idrisのホームページ (ドキュメントや、よくある質問、例など)
- IdrisのHackageリポジトリ
- Idris言語のドキュメント (チュートリアル、言語リファレンスなど)