前置き
「型システム入門入門」という記事を書いているのですが、形式的な話を持ち込まずに、型システムに対する直観をうまく説明するのに苦労しています。そこで、ちょっとした息抜きに、最近思っていたことを書いてみることにしました。言い訳をするわけではありませんが、あえて誇張している箇所もあります。ただ、明らかな誤りはなるべくしないようにしているつもりなので、ツッコミは歓迎します。
最近「型推論」を持った言語が増えている
最近、静的型付き言語では、いわゆる「型推論」1 を持った言語が多く出てきています。また、既存の言語に型推論を追加したものも少なくありません。2000年以降の実用言語で、そのような型推論を持った言語をリストアップしてみます。
- C# (3.0以降）
- Java (10以降）
- C++ （C++ 11以降）
- Swift
- Scala
- Kotlin
- Go
- Rust
これを見る限り、主要な言語の多くに型推論が導入されたといえそうです。さて、これだけ多くの言語に型推論が導入されたにも関わらず、世間的には型推論というものに対して誤った理解や偏見、さらに動的型付けとの混同もあり、型推論というものに関して理解が進んでいないようです。そこで、ちょっと最近型推論に関して起こる議論に関する私の雑感を書き起こしてみることにしました。即興で書いたものなので厳密さを欠く部分や誤りもあるかと思いますので、その辺はコメント欄で指摘していただければ。
そもそも型推論って？
静的型付き言語において、型のごく一部を省略できるような技術、という程度に思っている人が多いようですが、それはその言語の型推論が雑魚なだけです。古典的には、静的な型システムを持った言語において、（関数の引数や返り値の）型を全く書かなくとも、そこから最も一般的な型（主要型と呼びます）を推論する技術を型推論と呼びます。この意味での型推論を昔から実装している言語には、ML（系）言語があります。特に、SMLでは、関数の引数や返り値の型を一切書かない場合でも、そこから主要型を推論できるという特性を持っています（SMLの言語仕様をちゃんと読んでいるわけではないので、主要型が求められないケースがあったら教えてください）。
たとえば、他言語で reduce や foldLeft と呼ばれる関数を、SMLでは次のように書くことができます。
fun fold_left f [] z = z
| fold_left f (x::xs) z = fold_left f xs (f z x);
val fold_left = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a
一番下の行が、実際に推論された型ですが、これは、 ('a -> 'b -> 'a) という関数と 'b 型の list と 'a 型の値を受け取ったら 'a 型の値を返してくれる、と読みます。ここで関数の引数の型も返り値も一切書かれていませんが、型パラメータを含む最も汎用的な型（主要型）が推論されているところが強力なところです。人間が型を書くより型推論に任せた方が汎用的な関数が定義できてしまうのです。
しかし、主要型が必ず推論できるという性質を成り立たせるには、型システムに制限を加える必要があります。そのため、実際の型システムによってはそもそも主要型が存在しないケースや型推論によって主要型が発見困難なケースもあり、現在では、部分的ではあっても、型が明記されていないプログラムから型を復元する手法一般を型推論と呼ぶことが多いように感じます（専門家のツッコミをお待ちしています）。
ただ、その意味での型推論も、一般的には結構「賢く」て、ちゃんと「推論」ぽいことをしてくれるのですが（推論手法については略）、最近の「型推論」は、単に変数宣言時の右辺の型（これは型推論に関係なく処理系が内部的に持っている）を変数に割り当てている程度のものを型推論と呼んでいるケースが多くて、たかがその程度のものを型推論と呼んでいいのか、個人的には非常に微妙に感じるところです（できれば別の用語が欲しい）。
Java 10の型推論が「推論」していないと思うワケ
Java 10の「型推論」は、ローカル変数の宣言において、
var x = expression;
というのがあったときに、 expression の型（ E とします）を x の型として宣言するというものですが、これは別に、別途「推論」処理を走らせる必要がありません（コーナーケースで推論しなければいけないことはあるかも）。というのは、 expression の型 E は、型推論関係なく、コンパイラが内部的に持っているはずで（でないと型チェックができない）、その型を単に var で宣言した名前に結び付ければいいだけだからです。ScalaやKotlinのローカル変数の型推論についても似たようなことが言えます。ただ、静的な型がある言語において、型の一部あるいは全部が欠けているときに、それを補完する技術を総称して型推論と呼ぶのであれば、これも型推論と呼ぶことはできる…のかもしれません。
ちなみに、上記SMLの型推論では、「単一化（unification）」をベースとした、それなりに複雑な処理が走っています。
型推論のメリット
最近、「型推論」に触れた人からすると、単にちょっとタイプ数を減らせる程度の技術に見えるかもしれません。しかし、内部的なヘルパ関数を定義しようとするときなどに、事前にどのような型になるのかをあらかじめ決めるのは簡単でないことも多々あります。そういうときに、強力な型推論があれば、推論結果と自分で書いた型を突き合わせることで、自分が定義しようとしていた関数の型がわかることもあります。上記 fold_left などを初めとして、型が思いつかなくても実装はすぐ思いつくということは考えられますし、そういうときに実装から型を導きだせるのはメリットと言えます。また、高階関数を多用するプログラムにおいて、いちいち型を付けているととても面倒な上に、その型も自明ではないので、型推論なしでやってられるか、という場面にしばしば遭遇します。ただ、こういう利点は、型推論が強力な言語であってこそ、という面があるので、型推論の本当の力を知りたいのなら、SMLやOCaml、Haskellなどの言語をかじってみることをお勧めします。
型推論のデメリット
最近、Java 10に「型推論」が入ったこともあり、そのデメリットあるいは危険性についても盛んに議論されています。その一部については私もうなずけるところもあります。たとえば、ScalaやKotlinはメソッドの返り値の型推論を許していますが、主要型が存在しない（要検証）こともあり、メソッドの中身が変わったら返り値の型が変わるという事態が起こる恐れがありますし、実際変わってしまうこともあります。そのとき、そのメソッドが公開されていれば、実装の都合で公開している型が変わってしまうことになり、特にライブラリが公開する型でそういう事態が起きるのは望ましくありません。Scalaのプロジェクトでも、返り値の型推論を濫用しているのを見ることがあるので、公開されている部分のメンバの型を推論させるのは良くないと感じます。
ただ、Java 10やC#のvarはたかだかローカル変数の型の割り当てを省略できる程度に過ぎないですし、他のローカル変数の「型推論」がある言語で、その点が大きな問題になったことはあまり聞いたことがないので、はっきり言って杞憂だと思います。今までに遭遇したことのない機能であるために過度に慎重になっているだけだろうと想像しています。
型推論と動的型付けの混同
Twitterなどを見ていると、何故かわからないのですが、型推論と動的型付け、あるいは暗黙の型変換を混同している人をしばしば見かけます。曰く「Rubyには型推論がある」「Pythonには型推論がある」「型推論はエラーの元になるので止めて欲しい」「PHPの型推論のせいで、整数と文字列が言語の中で混同されている」などなど。当然のことですが、型推論は、静的型がある言語において、型の一部が欠けているプログラムに対して、静的型システムに違反しない範囲で型を補完する技術であり、実行時に最低限のチェックが行われるだけの動的型付けとは全く別物です。
型推論の技術が進歩すれば、動的型付け言語でも、全てのプログラムに対して型を書かずに検証できるようになる
某カンファレンスでの某氏の基調講演が元になって生まれた話題ですが、型推論だけでそのようなことを実現するのは控えめに言ってもかなり難しいです。というか夢物語です。型推論に関する研究の歴史はかなり長く、その限界（型システムがある形になるとき、完全な型推論が無理になる、など）もある程度知られています。SMLのように型システムに対して制約をつける（歴史的には、型推論のために制約をつけたかどうかは知らないのですが、強力な型推論のためには型システムに制限をある程度付ける必要があることが多いです）ならともかく、既存の縛りが緩い型システムや、そもそも元々静的型がなかった言語に対して、型推論で全て解決するのはとてもとても難しいです。2
おわりに
説明（特にコード例）が不足している箇所も多々あり、わかりにくい記事だったかと思いますが、型推論に関する話題で思うところがあるものを、つらつらと書いてみました。この駄文をきっかけに、型推論という技術自体を調べるきっかけになってくれればいいなと思う次第です。
