依存型言語Idrisが1.0に

アルファ相当になったことを報告して数ヵ月、Idrisの作者で英国セント・アンドルーズ大学のコンピュータサイエンス講師であるEdwin Brady氏が、Idris 1.0のリリースを発表した。

Idrisが1.0になるということは、そのコア言語と基本ライブラリが安定していると見なされたということだ。つまり、将来の1.xバージョンでは、ソースコードの後方互換性が保証されることになる。アルファリリース以降、ツールとライブラリのサポートに重点を置きながら、それほど安定していない機能を有効にするための新しいpragmaと新しいLinearTypes言語拡張が追加された。Brady氏によれば、まだまだコントリビューションの余地がたくさんあるという。具体的には、コンパイラとランタイムの効率改善と、現在オープンになっている200以上のバグの修正を挙げている。

Idrisは主に研究ツールであり、今のところプロダクションに使えると考えるのは時期尚早だとBrady氏は考えている。しかし、Brady氏自身が書いた『Type-Driven Development with Idris』のManningからの出版、GitHubリポジトリのコントリビュータ数の増加、最近の学術成果などが証明しているように、言語への関心は高まっている。まだ言うには早すぎるかもしれないが、<a href="https://github.com/search?p=2&q=language%3Aidris&type=Repositories&utf8=・>Idrisコミュニティのはじまり</a>のサインかもしれない。InfoQでは、Brady氏にコメントを求めて記事を更新するつもりだ。</p>o&#10;&#10;<p>Idrisは純粋関数型プログラミング言語であり、システムプログラミングにも使えるほど汎用で効率が良いことに重点を置きつつ、より多くのプログラマに型ベースのプログラム検証技術を提供することを目指している。Idrisについて学びたければ、<a data-cke-saved-href=" http:="" docs.idris-lang.org="" en="" latest="" tutorial="" "="">チュートリアルを読むとよいだろう。また、依存型によるプログラミングのトレードオフについても読んでおこう。