Idris (プログラミング言語)

Idris
パラダイム	関数型
登場時期	2007年 (17年前)
設計者	Edwin Brady
最新リリース	1.3.4/ 2021年10月22日 (3年前)
評価版リリース	0.6.0 (Idris 2) / 2022年10月28日 (2年前)
影響を受けた言語	Agda, Clean, Coq, Epigram, F#, Haskell, ML, Rust
プラットフォーム	Cross-platform
ライセンス	BSD
ウェブサイト	idris-lang.org
拡張子	.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日閲覧。