計算機に推論できる型、できない型

　本記事は Wantedly 21新卒 Advent Calendar の17日目の記事です。本記事では、いくつかの言語の型システムに実装されている様々な機能を紹介するとともに、それが型推論の実現性に与える影響について述べます。

　最近静的型付き言語が盛り上がりを見せ、動的型付き言語の筆頭格だった Ruby もバージョン 3.0 で型解析ツールを導入するまでに至った一因には、きっと型推論の有用性が知られるようになったことが挙げられることでしょう。C言語で、関数ポインタを含んだ複雑なプロトタイプ宣言を書いている時ほどストレスを感じる時間はないし、かと言って Ruby on Rails で書かれたバックエンドを弄っている時に、型チェッカがあれば自明に発見できたであろうエラーでインシデントを起こすほど悲しいことはありません。プログラマが型を書かなくても静的な型チェックの恩恵を受けられる型推論の、何と偉大なことでしょうか。

　型推論によって、プログラマが型を書かなくても処理系が補ってくれる体験に一度染まってしまうと、もう面倒だから全部計算機が推論してくれといった気持ちになりますが、実は計算機には理論上推論のしようがない型というのも存在します。与えられたプログラムが停止するかを有限時間で判定するプログラムは、チューリングマシンと同等な計算能力を持つ計算機では作れないように、ある種の型システムに対しての型推論は我々の目の前にあるコンピューターでは実装できないことが理論的に証明されているのです。

　本記事では、いくつかの言語に実装されている型システムの機能を紹介するとともに、その機能が型推論の実現性にどのような影響があるかを述べます。業務でプログラムを書いていると、「ああ何でこの型が推論されないんだ！」とストレスを感じることも多いかもしれませんが、この記事を読むと、「まぁ理論的に推論できないことが分かってるし仕方ないかな」と寛大な気持ちになれるかもしれません。

多相型

　多くの言語では「ある型を α とおいた時に、α→α みたいな形で書ける型」のように型変数を使って汎用的な型を記述する機能が用意されており、このような型を計算機科学の文脈では多相型、ここで導入した型変数を型パラメーターと言います。言語によって多相型の呼ばれ方は違いますが、ジェネリクスと言ったほうが通りが良いかもしれないですね。

　この多相型、便利なのは便利なのですが表現力が高すぎて計算機には推論が難しいらしく、匿名関数と関数適用、あと変数の使用だけしか書けないような λ 計算と呼ばれる言語でさえ、関数型と多相型だけをサポートする型システムを考えただけで計算機には型推論が行えなくなってしまいます。それどころか、型チェックさえ実装できないことも分かっています。

　しかし、普通に業務でコードを書いていてもジェネリクスとして多相型を使う場面は出てくる訳で、それを使うと型チェックすらできなくなると言われると困ってしまいます。実際の言語はどのようにしてこの問題を回避しているのでしょうか？

let 多相

　実は多相型の推論を難しくしている原因と言うのは関数の引数が多相的な型になりうることらしく、関数引数の型を書く際には型パラメーターを導入できないように制限すると型推論が可能になります。TypeScript で言うなら、

const g = (f : <T>(x : T) => T): [number, boolean] => [f(1), f(true)];

みたいな関数の型は推論しないようにする感じでしょうか？ここで問題になっているのは型パラメーターを導入する位置で、例えば

<S, T>(array: [S], f : (arg: S) => T) => [T]

みたいな型は関数引数の位置で導入しているわけではないので制約には反していません。

　このような制限を設けることで型推論を行えるようにしている言語として有名なのが、OCaml や Haskell といった ML 系の関数型言語でしょう。それら言語の祖先にあたる ML が変数の宣言に let という構文を用いていたことから、ここで説明したように制限した多相性を let 多相と言います。

高 rank 多相

　また、先程話した関数引数では原則型パラメーターを導入してはいけないと言うのは少し行き過ぎた制約で、関数引数で与えられた関数の引数以降では型パラメーターを導入できないことにしても型推論が可能になります。あまり上手い例ではないですが TypeScript で言うと

(f: (g: <T>(x: T) => T) => number) => number

みたいな型は書けないように制限する感じでしょうか？

　このように let 多相の制限を少し緩和した多相性を rank-2 多相といい、実は let 多相をサポートする言語の例として挙げた OCaml や Haskell でも、自分で型を書く場合には rank-2 多相型がサポートされています。

　rank-2 多相で型推論を行えるのならと2匹目の泥鰌を狙いたい気持ちになりますが、残念ながらこれを推し進めた rank-3 多相では型推論を行えないことが分かっています。まあ実際のところ、rank-2 多相くらい緩い制限であれば大抵の用途では困らないのですが。

多相再帰

　let 多相とか rank-2 多相だとかみたいに、関数引数の位置での型パラメーター導入を制限すると型推論できることが分かりましたが、再帰をサポートする言語ではもう一点注意しなければなりません。

　多相型を持つような再帰関数の定義で、元々型引数として受け取った型とは違う型パラメーターによる再帰呼び出しを多相再帰と言うのですが、これをサポートするとまた型推論が行えなくなってしまうのです。多相再帰とはどう言うものか TypeScript で例を挙げると、

const f = <S, T>(i: number, x: S, y: T): (S | T)[] =>
  i <= 0 ? [x, y] : f<T, S>(i - 1, y, x);

みたいな再帰呼び出しでは、元々型 S だったパラメーターに T を渡して、もう一方の型パラメータではその逆を渡しているので多相再帰を行っていることになります。

　このような多相再帰を行うプログラムの型推論は計算機に行えないので、OCaml や Haskell のように気の利いた型推論を行える言語であっても、多相再帰が書きたければ型を明示的に書く必要があるようです。

　まあ再帰関数って自分自身を指す関数を暗黙のうちに引数として受け取る関数みたいなものなので、再帰呼び出しの時に型引数を変えられるように、暗黙的な引数で与えられる自分自身の型に型パラメーターを付けてしまうと、let 多相の時に避けたかった多相的な値を受け取る関数のパターンに嵌ってしまうので型推論ができなくなるのも頷ける話です。

再帰型

　これも多くの言語でサポートされている型ですが、型の定義に自分自身を用いるような型を再帰型と言います。割と書けて当然みたいな雰囲気がある型なので意識してなかったかもしれないですが、例えばC言語による次のようなリスト型の定義は再帰型になっていますし、

struct cons {
  int car;
  struct cons *cdr;
}

TypeScript による次のような JSON 型の定義も再帰型です。

type Json = object | Json[] | number | string | boolean | null

　多相型の推論が難しかったので、再帰型の推論もさぞ難しいのだろうと勘ぐるかもしれませんが、実はこちらはそれほど難しい問題ではありません。そもそも一般的な型推論の実装では、T = undefined | [number, T] を満たす型 T みたいな再帰型が必要になるかどうかチェックして、必要になれば型エラーにしている事情があるので、再帰型を推論して欲しければそこで型エラーにする代わりに再帰型を補うようにすれば良いのです。

　再帰型の推論は難しくないのですが、type や struct 等で再帰型を宣言しなくても推論してくれる言語処理系と言えば OCaml くらいで、その OCaml もコンパイルオプション -rectypes を指定しなければ推論してくれない辺り、積極的にサポートしようと言う雰囲気ではありません。何故多くの言語は、実装が難しい訳でもないのに再帰型の推論を行わないのでしょうか？

　実際に OCaml で再帰型の推論を行うようにしてプログラムを書いてみれば分かるのですが、多くの言語がこれをサポートしない理由は再帰型の表現力が高すぎて望まないプログラムにまで型が付いてしまうからだと思います。例えば、OCaml で関数 g と引数 x を受け取って関数呼び出しを行う関数 f を書きたいと思った時に、間違えて引数 x を関数だと思って関数呼び出しを行なったとしましょう。

(* 正しい実装 *)
let f g x = g x
(* 間違った実装 *)
let f g x = x x

こういったプログラムは型エラーにしてほしいものですが、何と再帰型の推論を行うようにすると後者にまで型が付いてしまいます。

        OCaml version 4.13.1

# let f g x = g x;;
val f : ('a -> 'b) -> 'a -> 'b = <fun>
# let f g x = x x;;
val f : 'a -> ('b -> 'c as 'b) -> 'c = <fun>

型の表現力は高ければ高いほど良いと言うわけでもないとは、言語設計の難しさを感じさせますね。

サブタイピング

　オブジェクト指向言語で主に使われている多相性として、ある型 T のサブタイプの型 S の値を、型 T の値として使っても良いとするサブタイピングが挙げられます。ここでのサブタイプと言うのは Java のような言語で言うところの派生クラスくらいの意味ですね。

　型はできるだけ推論したいといった潮流はオブジェクト指向言語にもあるらしく、Java のような言語では、ある型が別の型のサブタイプになっているかどうかをクラスの継承関係として明示的に書かなくてはならないのに対して、TypeScript のような言語ではサブタイプになっているかどうかを型の構造に従って自動的に推論してくれます。そればかりか、OCaml や SML# のような言語では let 多相に基づいた多相型とサブタイピングをサポートした上で型推論まで実現しているのです。

　例えば SML# で、座標を表すレコード p を受け取ってフィールド X とフィールド Y を取り出して返す関数 f を書くと、以下のように型が推論されます。

# fun f x = (#X x, #Y y);
val f = _ : ['a#{X:'b,Y:'c},'b, 'c. 'a -> 'b * 'c]

この関数が必要とする、フィールド X, Y を持つレコードは、フィールド X, Y, Z を持つレコードのサブタイプになっていますから、当然後者の型を持つ値を関数 f に渡すこともできます。

# f {X = 0.0, Y = 0.0, Z = 0.0};
val it = (0.0, 0.0) : real * real

　このようにサブタイピングをサポートしても型推論は実現できるのですが、一方でサブタイピングと共に用いられる機能が型推論を妨げることもあるので注意しなければなりません。

交差型

　いくつかのオブジェクト指向言語でサポートされている型として、型 S, T の両方で型付けできる式の型、交差型が挙げられます。例えば、TypeScript だと S & T って書くと S と T の交差型を表現できたりしますよね。

　この交差型、実は計算機に推論するのは難しい型らしく、匿名関数と関数適用、あと変数の使用だけしか書けないような λ 計算と呼ばれる言語でさえ、交差型とサブタイピングをサポートする型システムを導入すると型推論が不可能になってしまうのです。まぁ、そもそもその交差型とサブタイピングをサポートした言語って、プログラムの実行が停止することとプログラムに型が付くことが同値になるとか言うヤバ過ぎる性質があるので、型推論できなくて当然なんですが。

　このように制限無しに交差型をサポートすると型推論が不可能になる訳ですが、初期の篩型のように制限した形で交差型をサポートした上で型推論を実現している研究もあります。

まとめ

　本記事では、いくつかの言語に実装されている型システムの機能を紹介するとともに、その機能が型推論の実現性にどのような影響があるかを述べました。

　こうして眺めてみると、我々の目の前の計算機の能力って意外と理論的には大したことないなと思うと共に、計算可能性と言うドラゴンの尻尾をくすぐるようにして強力な型システムと型推論を両立させている言語設計者の偉大さを思い知らされますね。これだけ針の穴を通す仕事をやっている訳ですから、VSCode で TypeScript の型を推定して any しか出なかったとしても大らかな心で接してあげましょう。