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

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

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

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