Idris + Atomによる型駆動開発入門

4月から社内でType-Driven Development with Idrisの読書会をやっています。

takezoe.hatenablog.com

最近ようやくChapter 3まで進み、実際に自分でコードを書くエクササイズなども出てきました。この本ではAtomを使うことが推奨されているのですが、Atom用のIdrisパッケージが非常に強力で、型駆動開発の魅力を存分に感じることができます。そこで、今回は実際にAtomでのIdrisプログラミングがどのようなものかについて紹介したいと思います。

github.com

たとえば以下のようなシグネチャを持つVect(要素数を型情報に持つリスト)用のマップ関数を実装するとします。Vect n aの各要素に(a -> b)という関数を適用してVect n bを返すというものです。

my_vect_map : (a -> b) -> Vect n a -> Vect n b

まずmy_vect_map関数の型を定義し、関数定義部分でCTRL+ALT+Aを押します。 すると関数の実装の雛形が生成されます。

f:id:takezoe:20170615134138p:plain

続いてxsのところでCTRL+ALT+Cを押します。すると引数のパターンマッチに分解されます。

f:id:takezoe:20170615134149p:plain

?my_vect_map_rhs_1などとなっている部分は「ホール」と呼ばれるもので、Scalaでいうと???に近いものです。ひとまずこれで型チェックを通し、あとから実装を当てはめていくことができます。ホールの部分でCTRL+ALT+Sを押すと型情報から推測が可能な実装が生成されます。

f:id:takezoe:20170615134206p:plain

残ったホールでもう一度CTRL+ALT+Sを押します。

f:id:takezoe:20170615134219p:plain

なんということでしょう!関数の型を定義したあとは、ショートカットを押していくだけでmy_vect_map関数が完成してしまいました!

f:id:takezoe:20170615134237p:plain

もちろんこれは非常に簡単な例ですが、型駆動開発の片鱗は感じ取ることができるのではないでしょうか。静的な型付けのプログラミング言語コンパイル時の型チェックなど安全性が強調されることが多いですが、型駆動開発は型の力をよりアグレッシブに活用する開発スタイルといえるでしょう。

読書会の完走まではまだまだ長い道のりですが、型駆動開発の奥義を会得するべく日々修業を続けていきたいと思います。