BT

Idrisが間もなくバージョン1.0に

| 作者: Sergio De Simone フォローする 18 人のフォロワー , 翻訳者 吉田 英人 フォローする 0 人のフォロワー 投稿日 2017年1月19日. 推定読書時間: 2 分 |

原文(投稿日:2016/12/19)へのリンク

依存型(dependent type)ベース言語のIdrisが間もなくバージョン0.99に到達する。Idrisチームによると,1.00のアルファ版として見ることができるものだ。Idris 1.0のリリースは2017年2月頃と予想される。

Idrisは,多くのプログラマが型ベースのプログラム検証技術を利用できることを目的としながら,汎用性とシステムプログラムにも使用可能な効率性にも重点を置いた,純粋関数型プログラミング言語である。

Idrisの基本的なアイデアは,関数が値の間の依存性を表現する方法であるように,型と値の間の依存性を表現を目的とする依存型(dependent type)にある。例えば,各要素が次の要素より小さいリストを返すソート関数を定義する場合,関数の実装がコンパイルできるのは,その特性が真であると証明された時に限られる。同じようにIdrisでは,ソフトウェアの特性を表現として,例えばファイルハンドルにアクセスする際の,分散型システムや並列システムにおける配列範囲の検証やプロトコルの正当性を,特定のプロトコルに従うすべてのプログラムに対して保証することができる。次の例はIdrisのVect型と,2つのベクタを加算するapp関数の定義を示したものだ。


infixr 5 ::;
data Vect : Set -> Nat -> Set where
   VNil : Vect a O
 | (::) : a -> Vect a k -> Vect a (S k);

vapp : (Vect A n) -> (Vect A m) -> (Vect A (plus n m));
vapp VNil ys = ys;
vapp (x :: xs) ys = x :: vapp xs ys;

上のコード例では,次に示すvapp不正な実装のような関連型の誤用を,コンパイラによって検出することができる。


vapp : Vect a n -> Vect a m -> Vect a (plus n m);
vapp VNil      ys = ys;
vapp (x :: xs) ys   = x :: vapp xs xs; -- BROKEN

1.0のリリースを決定したおもな理由は言語が安定したことだ,とidrisのコア開発者は述べている。ただしこれは,言語が“実用レベル”であるという意味ではない。開発チームが長期にわたるサポートや実装の品質を保証することができない,という点がその大きな理由だ。そうではあっても,依存型を使用するプログラムを探求するための研究ツールとして,Idrisに大きな価値のあることには代わりない。

Coqと同様に,Idrisもバック推論(back reasoning)を含むインタラクティブな定理証明をサポートするが,Idrisは定理証明よりも汎用目的のプログラム言語であることを優先している。IdrisのC言語へのコンパイラは,メモリ管理にガベージコレクションを使用する。

 
 

この記事を評価

関連性
スタイル
 
 

この記事に星をつける

おすすめ度
スタイル

こんにちは

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

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

あなたの意見をお聞かせください。

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

このスレッドのメッセージについてEmailでリプライする
コミュニティコメント

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

このスレッドのメッセージについてEmailでリプライする

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

このスレッドのメッセージについてEmailでリプライする

ディスカッション

InfoQにログインし新機能を利用する


パスワードを忘れた方はこちらへ

Follow

お気に入りのトピックや著者をフォローする

業界やサイト内で一番重要な見出しを閲覧する

Like

より多いシグナル、より少ないノイズ

お気に入りのトピックと著者を選択して自分のフィードを作る

Notifications

最新情報をすぐ手に入れるようにしよう

通知設定をして、お気に入りコンテンツを見逃さないようにしよう!

BT