type level programming in scala introduction
もう旬を逃した感が少しありますが JavaOne Tokyo の JVM 言語 BOF で、よしださんが Scala 型レベルプログラミングという LT をされました。ボクはその場では聞けなかったのですが、後日 Scala 勉強会第 76 回で聞く機会がありました。JavaOne では 5 分間の LT だったらしいのですが、なんとも…
というわけで、触発されてボクも似たような話をさらりと書いてみたいと思います。
そもそも型レベルプログラミングとはなんぞや、ということですが、普通のプログラムは「値」で「実行時」に「計算」をしています。これを単に「型」で「コンパイル時」に「計算」をしてみましょう、ということです。
といわれてもピンとこないと思うので（ピンと来る人はこんなもの読まなくていいですよ）兎に角簡単なところ例から順にやってみましょう。まずは、通常のプログラミングで 0 をどのように扱うことができるかを書いてみましょう。
val zero: Int = 0
特に面白いところはないですね。これが型レベルプログラミングでは以下のようになります。
type zero = O
簡単ですね！
いやいや、その "0" みたいな "O" はどこから来たんだよ、とここは突っ込まないといけないところです。
普通のプログラミングでは、予め様々な型が定義されています。しかし型レベルプログラミングでは、多くの場合、自分で必要な型を定義してやらなければなりません。Int 型、つまり整数型を型レベルプログラミングで扱うのは少し面倒なので、ちょっと卑怯ですが、ここでは自然数を表す型を定義することにしましょう。
sealed trait Nat
あれ、でも型レベルプログラミングでは、型は値として扱われるので、これは Nat という値を定義していることになるような気がしますね。本当に定義しないといけないのは、型ではなく「型の型」でないといけないはず…ところが残念なことに、scala には型の型なんてものはありません。困りました。仕方が無いので、それに近いものを何とかしてひねり出してやる必要があります。ところで、scala はオブジェクト指向言語です。オブジェクト指向には継承というものが存在します。scala の型レベルプログラミングでは、型の型としてこの継承を利用します。つまり、ある型を継承した型を、ある型に属する値としてみなす、ということです。基底クラスは以前として矢張り型ですが、値としての型ではなく、型の型としての型とみなす、ということにします。何故継承を使うべきなのかは後述します。
自然言語で説明するとさっぱりですね、兎に角コードを書いてみます。
trait O extends Nat
0 は自然数です。上のコードは、「Nat 型の O という値」を定義した、と考えて下さい。0 は自然数です。簡単ですね。簡単ですね？
さて自然数は 0 だけではありません。1, 2, 3, 4, 5 ... 兎に角たくさんあります。これらを全て、一つずつ定義していくことは勿論できません。幸い、自然数とはなんぞやということを既に数学者が考えて下さっていますので、それに単に従うことにしましょう。自然数は「ペアノの公理」として形式的に定義されています。非形式的にざっくり説明すると、自然数とは以下のようなものです。
1 ってどこから沸いてきたんだ…？足すってなんだ…？そんな気持ちは囲んで棒で叩いてイカめいて薄くなったところをすかさずケバブだ！それ以上いけない。
1 つ目のルールに対応するものは既に定義できました。2 つ目のルールに対応するものはどのように定義できるでしょうか。まずは値レベルで考えてみましょう。以下のような関数を定義します。
def s(n: Int): Int = 1 + n
こう使います。
val one = s(zero) val two = s(one)
簡単ですね。0 と関数 s さえあれば、その気になればどんな自然数も表現できることが分かってもらえると思います。
さて同じことを型レベルプログラミングでやろうとすると、関数を定義する必要があります。関数というのは通常、値を受け取り値を返すものですが、型レベルプログラミングでは、型を受け取り型を返すものでなければなりません。これは、型パラメタを取るクラスとして表現できそうです。scala ではこれを型コンストラクタと呼んだりもします。
trait S[N <: Nat] extends Nat type one = S[zero] type two = S[one]
型パラメタとして渡される型は自然数でなければいけません。これは型パラメタに対する制約として記述することができます。型の型は継承によって表現されるのでした。すると、型パラメタの上限境界（upper bound）を指定してやることで、型の型を記述することが可能になります。型パラメタの制約として表現可能なら、どのような方法で型の型を表現してもよいのですが、制約の記述が簡単なのと、sealed modifier である程度定義の制限をすることができるので、継承を利用するのは妥当な選択だと思っています。完全に型レベルで「閉じて」いますしね。（問題もあって、例えば継承と上限境界を利用する場合には type invalid = S[Nat] のような記述が許されてしまうため、完璧ではないのですが、まあ色々面倒なので妥協することにしましょう）
嗚呼、さらりと書いてみたいとか最初に書きましたが、この調子ではいつまでたっても終わりそうにないので、とりあえず今回はここまでにします。今回のは part1 ということにして、多分続きます。
おしまい。
