パラメトリック多相
何か具体的な正しいステートメントが存在するときに、それを抽象化する試みは穴あきの文章を考えることから始まる。そうしてその穴の部分にどれだけ一般的な単語を当てはめられるか、どれだけ一般化しても元のステートメントが正しいかを考えていく。という過程は日常的に行う抽象化手段のひとつと思う。
僕はジェネリクス、パラメトリック多相はプログラミングにとってとても重要な機能だと思っている。関数型言語や関数型プログラミングはそれなりに普及して来ている様だが、それらは「もし式の中に一般化したい箇所があるならばそこを変数として関数にしてしまえば良い」という手法を提供する。それを気軽にできる様な機能を提供する。
パラメトリック多相はそれと似た様な機能を型レベルで提供する。つまり型シグネチャの中で一般化したい部分があるならば切り取って型変数にしてしまえば良い、ということが気軽にできる様になる。
それらは同じ様な動機によって必要になる手段だ。
この考えはいろんな箇所で役に立つ。
HaskellにはArrowという型クラスがあるが、これは`(->)`の抽象である。
f :: forall x y. x -> y
という型に対して、`->`をArrowで抽象化すると
f' :: forall a x y. Arrow a => a x y
となる。`a :: * -> * -> *`であるが何も問題はない。
例えばghc-8.4で導入予定のlinear-typeに関する論文、
を読んでいると(->)に下付きの`p`, `q`などが出てくるが、
- >_1`, `->_2`, `->_3`, ...あたりを抽象化して`forall p. ->_p` といったものが現れるのはそんなに不思議ではない。
rustにおいて`mut`とnon `mut`を抽象化したいという声をどこかで見た気がするが、実現可能性はともかく`mut`部分を変数化すると言うアイデアは面白い。
`mut`とnon-`mut`を抽象化しても型チェック通すには多分`mut`相当の扱いをしないといけないよなー...とかそこから色々考えたりするわけだ。
雑な抽象化の試みによってたまに新しい構造が見えたりするのは面白かったりする。
