Idrisは依存型やオプショナルな遅延評価、全域性チェッカーを特徴とする純粋関数型プログラミング言語である。Idrisは証明アシスタントとしても使われるが、 Haskellのように汎用プログラミング言語として設計されている。

Idrisの型システムはAgdaに、証明はCoqに似ていて、elaboratorリフレクションによるタクティクスを含む。AgdaやCoqと比べ、Idrisは副作用管理と内部ドメイン固有言語のサポート重点を置いている。 IdrisはC言語 (Cheneyのアルゴリズムを使ったコピーガベージコレクタに依存) とJavaScript (ブラウザーとNode.jsの両方) にコンパイルされる。JVMや、CIL、LLVMを含む他のプラットフォーム用のコード生成器もある。

脚注

関連項目

外部リンク Idrisのホームページ (ドキュメントや、よくある質問、例など) IdrisのHackageリポジトリ Idris言語のドキュメント (チュートリアル、言語リファレンスなど)