メソッド呼び出しの型推論を追いかける(前半)

Java

メソッドの型推論エンジン作ってて、そのテストケースの洗い出し中。
Java言語仕様(第3版)の15.12.2.7 Inferring Type Arguments Based on Actual Argumentsを私なりに解説してみようと思います。理解してしまえば、そんな実装が難しいものではありません。

メソッドの型推論は主に次の2ステップからなります。

  1. 実引数と仮引数の制約から、型変数に対する制約を計算する
  2. 型変数に対する制約から、実際の型を推論する

(前半)では、前者の部分について追いかけてみます。言語仕様の和訳では、p.395〜p.405のあたりです。ちなみに、テストケース洗い出しのために網羅しているので、同じくらいの分量が平気であります。

わかりやすさのために、厳密さを犠牲にしている個所が多々あります。なんとなくわかった気になれば十分、という用途でない場合は素直に本家の言語仕様を読んでください。

具体的には、下記のようなインチキを含む。

  • 呼び出し先のメソッドは、型引数が常に1つ
  • パラメータ化型は、型引数が常に1つ
  • 「そうでなく、」という部分が読みにくいので全力で省略
    • 上から順に適用していく方向で
  • 「型Uをメソッド起動変換によって型Vに変換可能」(U << V)を「UをVに代入可能」と意図的に読み替えてる

利用する記号

いろいろと珍しい記号を使うかも。

A
実引数の型。実際にはプリミティブ型だったり、パラメータ化型だったりする。
F
仮引数の型。実際にはプリミティブ型だったり、パラメータ化型だったりする。
U, V, W
型。ワイルドカードは表現しない。
G, H
パラメータ化型の型名。G<U>, H<? extends V>などと使う。
U <: V
UはVのサブタイプ
X <= Y
XはYに含まれる(X, Yは? extends/super...の形式をとることがある)
U << V
UをVに代入可能
infer(U << V)
UをVに代入可能、という前提で推論を実行する
infer(U = V)
UとVが同一の型、という前提で推論を実行する
infer(U >> V)
VをUに代入可能、という前提で推論を実行する
constraint(T = U)
型変数Tは型Uと同一の型、という制約を追加
constraint(T <: U)
型変数Tは型Uのサブタイプ、という制約を追加
constraint(T :> U)
型変数Tは型Uのスーパータイプ、という制約を追加

最初に考えるべきこと

(前半)の目標は、「実引数と仮引数の制約から、型変数に対する制約を計算する」ということでした。
たとえば、

void test() {
    ArrayList<String> list = ...;
    method(list);
}
<T> void method(List<? extends Comparable<? super T>> list) {
    ...
}

上記に含まれる式「method(list)」において、型引数Tに対して課せられる制約はなにか、ということを計算しようとしています。
現在分かっているのは次の2点です。

  1. 実引数の型は ArrayList<String> である
  2. 仮引数の型は List<? extends Comparable<? super T>> である

メソッドを呼び出す際の規則には次のようなものがあります

  1. 実引数型Aは仮引数型Fに代入可能 (A << F)

現在、実引数の型と仮引数の型は判明しているので、これらを元に次の制約を導出できます。

  1. ArrayList<String> << List<? extends Comparable<? super T>>

上記のルールを元に、「infer(ArrayList<String> << List<? extends Comparable<? super T>>)」というプロセスを実行することで、Tに関する制約を計算していきます。
これは、次項「infer(A << F) のプロセス」のA, Fにそれぞれの型をあてはめて読み進めると最終的にTの制約が分かるようになる予定。

以降、ちょっと読みにくくて申し訳ないですが、

この中に型推論規則の私の解釈と解説を書いていきます。

infer(A << F) のプロセス

最初の推論規則は、A型の実引数をF型の仮引数に代入できるという仮定のもとに行います。
これは疑似的*1には下記のような感じです(A, Fは何らかの別の型を表す)。

method((A) value);
...
<T> void method(F f) {}

これを元に、型変数Tの型を推論していきます。

Fが型変数Tに関連しない場合: (1-a)
  • 何もしない

これは、

<T> void method(int f) {}
<T> void method(String f) {}

など、仮引数型Fに型変数Tが含まれない場合のルール。この場合はTに関する情報が何一つ得られないので、何も行わない。
これ以降は少なくとも次のことが前提として与えられます。

  • F はプリミティブ型、およびその配列型ではない
  • F は(パラメータ化されていない)クラス/インターフェース型、およびその配列型ではない

上記はいずれも型中にTが出現しません。また、上記からFが参照型であることは明らかです。

Aがnullである場合: (1-b)
  • 何もしない

これは、

method(null);
...
<T> void method(T f) {}

など、実引数にnullを渡した場合のルール。これによってTはnullのスーパータイプであることが分かるものの、nullはすべてのサブタイプなので特に制約をかけないらしい。*2

Aがプリミティブ型である場合: (1-c)
  • Aにボクシング変換を適用した型Uに対して、infer(U << F)

これは、

method((int) value);
...
<T> void method(T f) {}

など、実引数にプリミティブの値を渡した場合のルール。FがTに関連しない場合にはこの検証を行わないため、少なくともFは参照型です。このため、Aには何も考えずにボクシング変換を適用した後、変換後の型で再帰的に型推論を実行します。
上記の例では、

method((Integer) value);
...
<T> void method(T f) {}

であるかのように動作することになります。

Fが型変数Tである場合: (1-d)
  • constraint(T :> A)

これは、

method((CharSequence) value);
...
<T> void method(T f) {}

など、呼び出し先のメソッドの仮引数が直接Tだった場合などのルール。上記の場合、「TはCharSequenceのスーパータイプである」という制約が追加されます。Tの型はまだ確定しませんが、「少なくともTのスーパータイプであればうまくいきそうだ」というところまでは分かったという感じです。

Fが配列型U[ ]である場合: (1-e)
  • Aが参照の配列型V[ ]、またはAの上限境界が参照の配列型V[ ]であれば、infer(V << U)

これは、

method((CharSequence[]) value);
...
<T> void method(T[] f) {}

など、呼び出し先メソッドの仮引数が配列型だった場合などのルール。Javaの配列型のサブタイプ関係は、その要素型のサブタイプ関係と一致します。なので、Fが配列型でAも配列型なら、その要素型に対して再帰的に型推論を実行していけばいずれはTにたどり着けるはず。
つまり、次のような流れになります。

  1. CharSequence[ ] << T[ ]
  2. infer(CharSequence << T)
    1. CharSequence << T
    2. constraint(T :> CharSequence)

なお、Aはプリミティブ型の配列であってはいけません。配列の要素型がプリミティブ型であってもボクシング変換は適用できないため、int[ ]とInteger[ ]にサブタイプ関係があるわけではないため推論は終了してメソッドの適用検査のところで失敗します。
なお、Aは配列型ではなくて上限境界に配列型を持つ型変数でもOKです。ただし、これは捕捉変換の結果で出現するくらいなので省略。

Fがパラメータ化型G<U>である場合: (1-f)
  • AがG<V>のサブタイプであれば、infer(V = U)

これは、

method((ArrayList<String>) value);
...
<T> void method(List<T> f) {}

など、呼び出し先メソッドの仮引数がパラメータ化型だった場合のルール。上記の例ではArrayList<String>がList<String>に変換された後、「String = T」という制約で型推論が実行されます。
ここでのプロセスは、

  1. ArrayList<String> << List<T>
  2. List<String> << List<T>
  3. infer(String = T)

というような推論が行われます。注意すべきは、Javaでは「AがBのサブタイプであったとしても、G<A>がG<B>のサブタイプとはならない」という(非常に引っかかりやすい)ルールがあるため、上記はString << TではなくString = Tとなります。
なお、U, Vなどの位置にワイルドカードを入れることはできません。ワイルドカードを使える場合は必ず「? extends U」や「? super V」など、UやVを利用して表現することにします。
上記のルールでは、実引数の型引数にワイルドカードを含めた場合が記載されていません。つまり、実引数にワイルドカードが含まれていた場合は推論が進まないのですが、捕捉変換がうまく働いてたいていの場合に問題になりません。つまり、

ArrayList<? extends CharSequence> value = ...;
method(value);
...
<T> void method(List<T> f) {}

という形式で推論が発生する場合、「? extends CharSequence」の部分は捕捉変換により一時的な型変数(仮にX)と置き換えられ、A=List<X>というようなワイルドカードを含まないパラメータ化型として取り扱うことになります。

Fがパラメータ化型G<? extends U>である場合: (1-g)
  • AがG<V>のサブタイプであれば、infer(V << U)
  • AがG<? extends V>のサブタイプであれば、infer(V << U)

これは、

method((ArrayList<String>) value);
...
<T> void method(List<? extends T> f) {}

など、呼び出し先メソッドの仮引数がパラメータ化型で、さらに型引数が? extends..の形式だった場合のルール。上記の例ではArrayList<String>がList<String>に変換された後、「String << T」という制約で型推論が実行されます。
ここでのプロセスは、

  1. ArrayList<String> << List<? extends T>
  2. List<String> << List<? extends T>
  3. String <= ? extends T
  4. infer(String << T)
    1. String << T
    2. constraint(T > String)

というような推論が行われています(5番目は再帰的に処理した結果を含めています)。なお、ここで利用している演算子<=は型引数の包括*3を表現しています。つまり、Stringは? extends Tに含まれなければならないため、TはCharSequenceやObjectなどのStringのスーパータイプでなければなりません。
2つ目のルールは再現が難しいパターンです。

class X<_> {
    void test() {
        X<List<? extends CharSequence>> a = null;
        method(a);
    }
    <T> void method(X<? extends List<? extends T>> xf) {}
}

上記のように、パラメータ化型を入れ子にすることで、捕捉変換によって内側のワイルドカードが型変数に変換されることを回避しています*4。

実引数がパラメータ化型でさらにワイルドカードを含む場合、通常はワイルドカードが捕捉変換によって一時的な型変数に変換されてしまいます。これを回避するには捕捉変換が再帰的に適用されないことを利用して入れ子になったパラメータ化型の深い位置にワイルドカードを配置するか、。いずれにせよ、次のようなプロセスで推論が行われます。

  1. X<List<? extends CharSequence>> << X<? extends List<? extends T>>
  2. List<? extends CharSequence> <= ? extends List<? extends T>
  3. infer(List<? extends CharSequence> << List<? extends T>)
    1. List<? extends CharSequence> << List<? extends T>
    2. ? extends CharSequence <= ? extends T
    3. infer(CharSequence << T)
      1. CharSequence << T
      2. constraint(T > CharSequence)

要は、実引数がVでも? extends Vでも同じ結果になります。

ここにA=G<? super V>のケースが含まれていないのは、推論のプロセスで

  1. List<? super V> << List<? extends U>
  2. ? super V ... ? extends U

という結果が出現したところで、? super V ... ? extends Uとの関係から導き出せる情報が存在しないためです。これが即座に失敗するかというとそういうわけでもなく、U = Objectの時に「? super V <= ? extends Object」という関係が成立し、エラーもなく動作させることができます。

Fがパラメータ化型G<? super U>である場合: (1-h)
  • AがG<V>のサブタイプであれば、infer(V >> U)
  • AがG<? super V>のサブタイプであれば、infer(V >> U)

これは、

method((ArrayList<Number>) value);
...
<T> void method(List<? super T> f) {}

など、呼び出し先メソッドの仮引数がパラメータ化型で、さらに型引数が? extends..の形式だった場合のルール。上記の例ではArrayList<String>がList<String>に変換された後、「Number >> T」という制約で型推論が実行されます。
このとき、代入変換の向きが反転していることに注意が必要です。上記のプロセスでは、

  1. ArrayList<Number> << List<? super T>
  2. List<Number> << List<? super T>
  3. Number <= ? super T
  4. infer(Number >> T)

というような推論が行われています。? superの包括は? extendsの包括とサブタイプ関係が逆になります。つまり、Numberは? super Tに含まれなければならないため、TはIntegerやLongなどのNumberのサブタイプでなければなりません。
2つ目のルールは? extends Tのときと同様に再現が面倒です。

class X<_> {
    void test() {
        X<List<? super CharSequence>> a = null;
        method(a);
    }
    <T> void method(X<? extends List<? super T>> xf) {}
}

それでも、推論のプロセスは

  1. ...
  2. infer(List<? super Number> << List<? super T>)
    1. List<? super Number> << List<? super T>
    2. ? super Number <= ? super T
    3. infer(Number >> T)

となり、? superが付いていても付いていなくても同じになります。
ここにA=G<? extends V>のケースが含まれていないのは、前述のG<? extends U>と同じような理由です。

infer(A = F) のプロセス

次の制約は、A型の実引数とF型の仮引数は同一の型という仮定における推論です。これは、infer(A << F)における推論中に、

Fがパラメータ化型G<U>である場合: (1-f)
  • AがG<V>のサブタイプであれば、infer(V = U)

という規則で出現します。

また、これらの検証は先ほどの推論規則を元に、次のようなコードで行えます。

class X<_> {
    void test() {
        // A は実引数型
        X<A> a = null;
        method(a);
    }
    // F は仮引数型
    <T> void method(X<F> xf) {}
}

これは、次のようなプロセスで途中まで推論が行われます。

  1. X<A> << X<F>
  2. infer(A = F)
Fが型変数Tに関連しない場合: (2-a)
  • 何もしない
Aがnullである場合: (2-b)
  • 何もしない

この規則が不可解。たぶんinfer(A = F)においてAがnullになるパスがない*5。

Fが型変数Tである場合: (2-c)
  • constraint(T = A)

infer(A << F)との違いは、A = Fという制約であるため、Tに対する制約もT = Aとなっています。
例えばこんな感じ。

class X<_> {
    void test() {
        X<String> a = null;
        method(a);
    }
    <T> void method(X<T> xf) {}
}

これは次のように解釈されます。

  1. X<String> << X<T>
  2. infer(String = T)
    1. String = T
    2. constraint(T = String)

なお、このT = Aという制約は、型変数TがまさにA型と推論されることを表しています。つまり、上記の例でTはString型と推論されます。

Fが配列型U[ ]である場合: (2-d)
  • Aが参照の配列型V[ ]、またはAの上限境界が参照の配列型V[ ]であれば、infer(V = U)

infer(A << F)との違いは、A (= V[ ]) = F (= U[ ])という制約であるため、その要素型に対する制約もV = Uとなっています。

Fがパラメータ化型G<U>である場合: (2-e)
  • AがG<V>という形式であれば、infer(V = U)

infer(A << F)との違いは、AはG<V>のサブタイプではなく、AはG<V>そのものでなければなりません。それ以外は基本的に同じ。

Fがパラメータ化型G<? extends U>である場合: (2-f)
  • AがG<? extends V>という形式であれば、infer(V = U)

先ほどと同様に、AとFは同じ型であるという制約が与えられていますので、AはFと同じ形式でなければなりません。

Fがパラメータ化型G<? super U>である場合: (2-g)
  • AがG<? super V>という形式であれば、infer(V = U)

これも先ほどと同じ。

infer(A >> F) のプロセス

最後の制約は、「F型の仮引数をA型の実引数に適用できる」というinfer(A << F)とは逆の推論規則です。言語仕様書にもあるように、単にinfer(F << A)としてもうまくいきません。このプロセスが一番めんどくさい仕組みで動いてます。

この制約は、infer(A << F)における推論中に、

Fがパラメータ化型G<? super U>である場合: (1-i)
  • AがG<V>のサブタイプであれば、infer(V >> U)
  • AがG<? super V>のサブタイプであれば、infer(V >> U)

という規則で出現します。また、実引数から推論されなかった型変数の推論*6でも使います。

また、これらの検証は先ほどの推論規則を元に、次のようなコードで行えます。

class X<_> {
    void test() {
        // A は実引数型
        X<A> a = null;
        method(a);
    }
    // F は仮引数型
    <T> void method(X<? super F> xf) {}
}

これは、次のようなプロセスで途中まで推論が行われます。

  1. X<A> << X<? super F>
  2. infer(A >> F)
Fが型変数Tに関連しない場合: (3-a)
  • 何もしない
Aがnullである場合: (3-b)
  • 何もしない

この規則も不可解。たぶんinfer(A >> F)においてAがnullになるパスがない。

Fが型変数Tである場合: (3-c)
  • constraint(T <: A)

今回はA >> Fという制約であるため、F=Tの時にA :> Tという制約が導出されます。

Fが配列型U[ ]である場合: (3-d)
  • Aが参照の配列型V[ ]、またはAの上限境界が参照の配列型V[ ]であれば、infer(V >> U)

これまでと同様です。ただし、A (= V[ ]) >> F (= U[ ])という制約が前提にあるため、要素型の制約もV >> Uとなっています。

Fがパラメータ化型G<U>である場合: (3-e)
  • AがG<V>という形式であれば、infer(V = U)
  • AがG<? extends V>という形式であれば、infer(V >> U)
  • AがG<? super V>という形式であれば、infer(V << U)
  • Aの宣言型がGでなくAが宣言型Hをパラメータ化した型である場合、H<V>がG<S>のスーパータイプ(Sは任意の型変数)であり、WをH<V>に出現するSをUに置換した型であり、FがWのサブタイプであれば、infer(A >> W)

最初の3つの形式は、Aの宣言型がFの宣言型であるGと一致しているという前提で推論を行っています。今回はA >> Fということで、Aの宣言型がFの宣言型と一致するか、スーパータイプである必要があります。スーパータイプである場合には4つ目の規則が発火して、宣言型をそろえた後に再帰的にこのアルゴリズムが実行されます。
最初の3つの形式は、それぞれ型引数の包括関係によって推論を進めています。

  • G<V> >> G<U>
    • U = V
      • V = U
  • G<? extends V> >> G<U>
    • U <= ? extends V
      • V >> U
  • G<? super V> >> G<U>
    • U <= ? super V
      • V << U

このような関係になるはずなので、それぞれ型引数にとられたV, Uの関係に関する制約を導出することができるようになります。
最後の一つは非常に前提条件が長いですが、例をみるとわかりやすいと思います。

class X<_> {
    void test() {
        X<List<String>> a = null;
        method(a);
    }
    <T> void method(X<? super ArrayList<T>> xf) {}
}

これは次のようなプロセスで推論が行われます。

  1. X<List<String>> << X<? super ArrayList<T>>
  2. infer(List<String> >> ArrayList<T>)
    1. List<String> >> ArrayList<T>
      • H := List
      • G<S> := ArrayList<X>
      • H<V> := List<X>
      • W := List<X>[X := T] = List<T>
      • assert ArrayList<T> <: List<T>
    2. infer(List<String> >> List<T>)

これによって、型変数がArrayList<T>であったのがList<T>に変わり、実引数List<String>とかなり近い形式になりました。最後の一つでやることは、このように「仮引数の形式を実引数の形式と一致させる」という作業です。途中に出てくるWは、「FがWのサブタイプであれば...」というルールを作っているのは、A >> W :> F というAとFの間にある型Wを用意して、A >> Fを用いて検証するのではなく、より制約の厳しいA >> Wを用いて検証するためです。なお、Aの宣言型とWの宣言型はHで一致しているため、再帰的に実行した推論プロセスでは、前3つの「AがG<...>という形式であれば、...」というルールはFがWに置き換わったことで「AがH<...>という形式であれば、...」というルールに読み替えることができるようになります。つまり、一度Wで媒介することで、前3つのルールを発火できるようにしています。

Fがパラメータ化型G<? extends U>である場合: (3-f)
  • AがG<? extends V>という形式であれば、infer(V >> U)
  • Aの宣言型がGでなくAが宣言型Hをパラメータ化した型である場合、H<V>がG<S>のスーパータイプ(Sは任意の型変数)であり、WをH<? extends V>に出現するSをUに置換した型であり、FがWのサブタイプであれば、infer(A >> W)

先ほどと同様、1つ目の形式はAとFの宣言型が一致しているという前提の推論です。一致しない場合には2つ目の形式で一致させようとする規則が発火して再帰的にこのアルゴリズムが実行されます。
この1つ目の形式は、先ほどと同様に型引数の包括関係によって議論を進めています。

  • G<? extends V> >> G<? extends U>
    • ? extends U <= ? extends V
      • V >> U

AがH<V>やH<? super V>の場合は、上記の計算でUとVの関係を導き出すことができません。
2つ目の規則は、先ほどと同様に「仮引数の形式を実引数の形式と一致させる」という目的で行っています。今回のWはH<V>ではなくH<? extends V>となりました。これはもともとの仮引数がG<? extends U>という形式であるためです。

Fがパラメータ化型G<? super U>である場合: (3-g)
  • AがG<? super V>という形式であれば、infer(V << U)
  • Aの宣言型がGでなくAが宣言型Hをパラメータ化した型である場合、H<V>がG<S>のスーパータイプ(Sは任意の型変数)であり、WをH<? super V>に出現するSをUに置換した型であり、FがWのサブタイプであれば、infer(A >> W)

これまでと同様、1つ目の形式はAとFの宣言型が一致しているという前提の推論です。一致しない場合には2つ目の形式で一致させようとする規則が発火して再帰的にこのアルゴリズムが実行されます。
この1つ目の形式は、これまでと同様に型引数の包括関係によって議論を進めています。

  • G<? super V> >> G<? super U>
    • ? super U <= ? super V
      • V << U

AがH<V>やH<? extends V>の場合は、上記の計算でUとVの関係を導き出すことができません。
2つ目の規則は、これまでと同様に「仮引数の形式を実引数の形式と一致させる」という目的で行っています。

最初の例

最初にこんな例を出しました。

void test() {
    ArrayList<String> list = ...;
    method(list);
}
<T> void method(List<? extends Comparable<? super T>> list) {
    ...
}

これをちょっと計算してみましょう。

ちなみに、型の親子関係はこんな感じです。

  • ArrayList<T> <: List<T>
  • String <: Comparable<String>

初期の制約はこんな感じ。

  • ArrayList<String> << List<? extends Comparable<? super T>>

こんな感じで推論します

  1. ArrayList<String> << List<? extends Comparable<? super T>> (1-g)
  2. List<String> << List<? extends Comparable<? super T>>
  3. String <= ? extends Comparable<? super T>
  4. infer(String << Comparable<? super T>)
    1. String << Comparable<? super T> (1-h)
    2. Comparable<String> << Comparable<? super T>
    3. String <= ? super T
    4. infer(String >> T)
      1. String >> T (3-c)
      2. constraint(T <: String)

ということで、TはString型のサブタイプだとわかりました。String型は継承できないので、TはString型でなければなりません。

実際には型引数も仮引数も2個以上あったりすることがあるため、Tには複数の制約が課せられていることがほとんどです。(後半)では、複数の制約が課せられていた時にTをどんな型にすれば矛盾が起きないかなどの計算を追いかけていく予定です。

まとめ

  • 手続きが多いけど、実はたいしたことやってない
  • 少しずつ簡単にして言って再帰的に処理している
  • 言語仕様書のところどころに「Discussion」が入るのは逆に読みづらくないか

ここまで読んだ人がいるかどうか…

*1:キャスト後に捕捉変換が適用されたりするので厳密には違う

*2:型推論のちょっとしたこと - しげるメモの意図は、nullリテラル式以外でnull型を作れるかなという感じでした。T :> null という制約がかかっててもよい気はしなくもない。

*3:4.5.1.1 Type Argument Containment and Equivalence

*4:パラメータ化型の配列型を利用して捕捉変換を回避することもできるはずですが、Sunのコンパイラではうまくいきませんでした -> SunのコンパイラとEclipse JDTで動きが違う(5) - しげるメモ

*5:型推論のちょっとしたこと - しげるメモ

*6:メソッド呼び出し時の型推論とか - しげるメモ