Idrisとはじめる型駆動開発
この記事はIdris Advent Calendar 2020の20日目の記事です。先に書いておくとIdrisについての有益な情報は残念ながらこの記事にはあまりないです。Windows機でIdrisを使うにはChocolateyを使うと雑にかつ楽に環境作れるよぐらいでしょうか…。型駆動開発に興味がでたものの触ったことないしマイナーで日本語情報があまりないなか、今回参加したアドベントカレンダーを見つけたことで、始める勇気がでました。環境の準備やIdrisについては他のアドベントカレンダーの記事が有益でわかりやすいので、少しでも興味が出た人は私みたいに飛び込んでみてはいかかでしょうか？
Type-driven Development with Idris
- 作者:Brady, Edwin
- 発売日: 2017/04/07
- メディア: ペーパーバック
この本に沿いながら型駆動開発に入門してみます。
型をただエラーを見つけるためのツールとするだけではなく、型駆動開発では型をプログラムを構築するためのツールとする。
💭これだけでは、よくわからん。ので、読み進めていく。
ここで言う「型」とは何か？
型はハードウェアからの視点、コンパイラやインタプリタからの視点もあるが、ここで問題とされるのはプログラマからの視点での型である。
For a programmer, types help name and organize concepts, aiding documentation and supporting interactive editing environments.
型付き言語の恩恵と言われるてるものと理解した（エディタの補完機能にはじまり、データ構造やらなにやらを型で明示的に扱えるクリアさとか可読性とか）。
型駆動開発へ
型駆動開発はプログラミング技法である。ここでは、型を最初に記述し、それらの型をガイドにして関数を定義していく。概要は下記の通りとなる。
入力と出力の型を記載する
入力の型の構造を実装の手引きとしながら、関数を定義する
必要に応じて関数と型を編集、改善する
💭これだけ言われてもそうですか、としか言えない。
以下では、プログラムが意図した動作を型を用いてどのように詳細に記述するかを例を用いて示す。
ATMをモデルに、行列乗算をする処理を記載する。
I’ll summarize the process of type-driven development and introduce the concept of dependent types, which will allow you to express detailed properties of your programs.
💭行列とか高校数学レベルだから、大丈夫…大丈夫…大丈夫のはず。 はてなブログって数式書けるの？
ちょっと行列の計算のところはわかってるものとして飛ばすとして、実装したい処理を整理すると下記の通りとなる。
| Operation | Input types | Output type |
|---|---|---|
| Add | Matrix x y, Matrix x y | Matrix x y |
| Multiply | Matrix x y, Matrix y z | Matrix x z |
| Transpose | Matrix x y | Matrix y z |
💭Transpose分からない人は、転置行列でググって…。行列よくわからない人は例なのであまり気にする必要はないはず。ここでやっていることは、実際に今から実装する処理に必要な入力と出力の型を規定した段階。なので有名なFizzBuzzで例示し直すと、入力値が数値に対して出力を文字列で返す仕様だとして以下の通りとなる。
| Operation | Input types | Output type |
|---|---|---|
| FizzBuzz | Int | String |
これであんまり怖くなくなったはず…。
ATMを実装する
💭ATMってAUTOMATED TELLER MACHINEの略ってはじめて知った。ここから、ATMの仕様が延々と続くので、Idrisについて知りたい人はこの記事を読むのはやめた方が良い気がする。なんか、ケントベックのTDD本の多国籍通貨の実装的なノリで延々と進む感じ…。ちなみに、正直、今、ページをめくる手が止まっている。お金貰えて仕事でやるならするけど感が…。ツラタン。
この本をIdrisを学ぶつもりで読むのはなんか得るものが少ないかもしれない。あくまでも型駆動開発を説明するための実装言語として関数型で型が強力なIdrisを選んだだけといった感じがする。ちなみに私は仕事でTypeScriptをメイン言語として使っているので、頑張ってTypeScriptで例を実装してみるとか勉強になりそうな感じがする。今日は時間切れなのでATMの実装をどう型駆動で実際に進めていくのは明日以降の記事で…。
