型理論における種 Kind とはなにかを考えた思考ノート。
しばしば Haskell の話が出てくるが筆者は Haskeller ではないので誤解等を多く含む恐れがある。こいよマサカリ。
*
値は型を持つ。例えば1という値はInt型だし,‘A’という値はChar型だ。
この関係を逆の視点からみて, “値を持つ型” のことを総称して “具体型” とか “真の型” とかいう。ここで,具体型は*なる種を持つと “定義” する。
* -> *
一方で, “値を持てない型” も存在する。たとえば,Maybeという型は存在するが,Maybe型の値というものはない。しかし,ここにIntを食わせてMaybe Int型としてやると,これはJust 1とかNothingとかの値を持てる。この意味でMaybeは型コンストラクタとかよばれる (項がない型コンストラクタとかいう存在があるらしいが見なかったことにする)。この挙動はあたかも “具体型*を引数に渡して具体型*を返す” かのようだ。a -> bな型の函数とよく似ている。函数に似た挙動であるから,アナロジーで表記してみよう。
- 値を引数にとって値を返すのが函数(函数もまた値である)
- 型を引数にとって型を返すのが型コンストラクタ(型コンストラクタもまた型である)
であるから,Maybeの種は* -> *であるということができる。以下記述のため* -> *なる種の型を “一階の型コンストラクタ” と呼ぶことにする (たぶんそんな用語はない)。
ややこしいが,a -> b型の種は (* -> *ではなく) *である。a -> b型の値 (つまり,函数だ) はラムダ式で表現できることを思い出そう。a -> bは具体型である。型と種で同じアロー演算子を使用していることが混乱を招く。アナロジー的には適しているのだが。
オブジェクト指向言語では,型コンストラクタはジェネリクスを使用したクラスで喩えることができよう。Java を例にすると,Optionalのオブジェクトというのは存在しないが,Optional<Integer>のオブジェクトは存在する。これもオブジェクト指向言語における関数の表記,someFunction(param)に類似している。
* -> * -> *
さて,オブジェクト指向言語ではPair<Integer, String>のように二つのクラスを取るジェネリッククラスが存在できる。これはやはりsomeFunction(param1, param2)な二引数関数に類似している。
おさらいになるが,函数型言語においては (というか Haskell では) 函数とは一つの値を入力とし,一つの値を出力とするものであるが,あたかも二つの値を入力としているかのように扱うこともできる。これは函数もまた値であることを利用している。
たとえば,単に二つの値を足し合わせる函数addを考える。これはadd 2 3のように扱うが,函数は一つの値しか入力にできないので,最初のadd 2の時点でaddの適用は終了してしまっている。かわりに,add 2という函数適用は, “引数に 2 を足して返す函数” を返している。その新たに生成された函数add 2に3を適用しているわけだ。
この函数addの型はInt -> Int -> Intと表記される。これはより理解しやすいよう表記するとInt -> (Int -> Int)で,Int型の値をとりInt -> Int型の値 (つまり,函数だ) を返すという意味になる。
これでオブジェクト指向言語における二引数関数が函数型言語の函数でどのように対応されるかのおさらいができたが,型引数を二つもつジェネリッククラスが函数型言語の型コンストラクタでどのように対応されるかもこれのアナロジーで考えることができる。
たとえば,Eitherという型コンストラクタは,Either String Intのように使用される。これは,最初のEither Stringの時点で新たな一階の型コンストラクタを “生成” し,それに型引数Intを適用している,と考えることができる。その意味で,Eitherという型の種は* -> * -> *であるといえる。これも* -> (* -> *)すなわち, “具体型*を引数に渡して一階の型コンストラクタ* -> *を返す” わけだ。
かつて私は (MaybeやListやIOと同様に) Eitherもモナドである,というような記述を目にして混乱したことがある。モナドは一階の型コンストラクタだと考えていたからだ。しかし,種の概念をなんとなく理解することで,おそらくこれはEither aがモナドということなのだろうと思い直すことができた。先に示したとおり,Either aは一階の型コンストラクタを “返す” からだ。Either ()がMaybe相当と考えることもできるだろう。
総括
具体的な値や函数の型,ないしオブジェクト指向言語における (ジェネリックな / でない) クラスとのアナロジーを想定することで種に対する概説ができたと思う。
同様に,(* -> *) -> * -> *な種の “高階型コンストラクタ” を想定することもできそうだが Haskeller でもない筆者はそろそろ黙るべきと思われる。