Type-Driven Development with Idrisの読書会をやっています

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

Type-Driven Development with Idris

今年のScalaMatsuriで@cbirchallさんにオススメされたのがキッカケなのですが、依存型（Dependent Type）を使って変態的なことがいろいろできるという話を聞いて面白そうということで有志（いまのところ6人くらい）で集まって緩く読み進めています。

ようやく2章の中盤に差し掛かったところなのでまだ先は長そうですが、1章でIdrisの概要をウォークスルーしたのでIdrisの思想やIdrisでのプログラミングのお作法のようなものが大体わかってきました。いまのところ言語として特徴的な機能だなと感じたのは以下の2点です。

• 依存型では型に値を持たせることができ、型同士の演算が可能
  • たとえばString型の要素を2つ持つVec 2 StringとString型の要素を3つ持つVec 3 Stringを結合するとVec 5 Stringになる
• ホール（hole）というScalaの???に似た機能があり、型だけ書いて実装を省略した状態でコンパイルを通すことができる
  • コンパイラが残っているホールを検出してくれるので、先に型だけ書いて後からホールを埋めていくというプログラミングが可能

数値型にもIntやInteger（BigDecimal的なもの）に加えて正の整数を表すNatがあり、配列の添え字などにはNatを使うというあたりもなるほどと思いました。

このような強力な型の表現力を活かしてより最適な型にリファインを繰り返しながらプログラミングしていくのがType-Driven Developmentのスタイルのようです。まだ、コードを見てもなかなかしっくり来ませんが、後半の章はATMをモデリングしてみるというケーススタディ的な内容になっているようなのでなんとかそこまでたどり着きたいと思います。

ちなみに社内では入門OCamlの読書会も行われているようです。

入門OCaml ~プログラミング基礎と実践理解~

さて、どちらが先に完走できるでしょうか。