4月から社内でType-Driven Development with Idrisの読書会をやっています。
最近ようやくChapter 3まで進み、実際に自分でコードを書くエクササイズなども出てきました。この本ではAtomを使うことを推奨しているのですが、Atom用のIdrisパッケージが非常に強力で、型駆動開発の魅力を存分に感じることができます。そこで、今回は実際にAtomでのIdrisプログラミングがどのようなものかについて紹介したいと思います。
たとえば以下のようなシグネチャを持つ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を押します。 すると関数の実装の雛形が生成されます。
続いてxsのところでCTRL+ALT+Cを押します。すると引数のパターンマッチに分解されます。
?my_vect_map_rhs_1などとなっている部分は「ホール」と呼ばれるもので、Scalaでいうと???に近いものです。ひとまずこれで型チェックを通し、あとから実装を当てはめていくことができます。ホールの部分でCTRL+ALT+Sを押すと型情報から推測が可能な実装が生成されます。
残ったホールでもう一度CTRL+ALT+Sを押します。
なんということでしょう！関数の型を定義したあとは、ショートカットを押していくだけでmy_vect_map関数が完成してしまいました！
もちろんこれは非常に簡単な例ですが、型駆動開発の片鱗は感じ取ることができるのではないでしょうか。静的な型付けのプログラミング言語はコンパイル時の型チェックなど安全性が強調されることが多いですが、型駆動開発は型の力をよりアグレッシブに活用する開発スタイルといえるでしょう。
読書会の感想まではまだまだ長い道のりですが、型駆動開発の奥義を会得するべく日々修業を続けていきたいと思います。