BT

InfoQ ホームページ ニュース 依存型言語Idrisが1.0に

依存型言語Idrisが1.0に

ブックマーク

原文(投稿日:2017/04/06)へのリンク

アルファ相当になったことを報告して数ヵ月、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="" "="">チュートリアルを読むとよいだろう。また、依存型によるプログラミングのトレードオフについても読んでおこう。

 
 

Rate this Article

Relevance
Style
 
 

この記事に星をつける

おすすめ度
スタイル

こんにちは

コメントするには InfoQアカウントの登録 または が必要です。InfoQ に登録するとさまざまなことができます。

アカウント登録をしてInfoQをお楽しみください。

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

コミュニティコメント

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

BT

あなたのプロファイルは最新ですか?プロフィールを確認してアップデートしてください。

Eメールを変更すると確認のメールが配信されます。

会社名:
役職:
組織規模:
国:
都道府県:
新しいメールアドレスに確認用のメールを送信します。このポップアップ画面は自動的に閉じられます。