部分型における変性と極性 - なぜScalaの変性は+や-で指定するのか

lang scala article

この記事はScala Advent Calendar 2022の19日目です.

Scalaではジェネリック型の変性(variance)は+や-で指定しますが, 他の言語(たとえば, C#, Kotlin)ではoutやinだったりします. この記事では変性の意味を整理して, なぜScalaでは+/-の記号を使うのか説明します.

追記
ただし, ここで説明している内容は基本的にC#やKotlinでも成立する(はずな)ので「なぜこれらの言語では+/-の記号を使わないのか」を説明するものではありません. 個人的には+/-の方がわかりやすいと思うし, out/inの記法は扱っている概念が簡単であるかのような誤解を生む(悪く言えば騙す)のでどちらかと言うと嫌いです.

発端

こういう話題がありました.

わかっている人にとってはこれで話は終わりなのですよね. でもそれなりに難しくてちゃんとわかっている人はそんなに多くもなさそうな雰囲気を感じ取ったので, 便乗して丁寧に説明してみたいと思います.

なぜ変性が必要か

まずは変性について整理しておきます. 例として継承関係にある3つの型をこの記事全体で使うので覚えておいてください. C <: B <: Aの関係です.

class A
class B extends A
class C extends B
共変がほしいケース

列っぽい何かを扱いたいときに, インタフェースとしてはSeq[A]を期待したい場合があります. ただ実体はListだったりVectorだったりいろいろで, 要素の型ももう少し何かに特化したBしか使ってないかもしれません.

val l: List[B] = List(new B)
val s: Seq[A] = l

このコードが型検査に通るためにはList[B] <: Seq[A]でなければなりません. List[_] <: Seq[_]だし, B <: Aだし, そりゃそうなのでは? と思うかもしれませんが, そうでもありません. 次のコードはコンパイルエラーです.

class Foo[X](value: X)
class Bar[X](value: X) extends Foo[X](value)

val x: Bar[B] = new Bar(new B)
val y: Foo[A] = x // [error] Found:    Bar[B]
                  //         Required: Foo[A]

ジェネリッククラス自身の継承関係とともに型引数の部分型関係も考慮して全体の型の部分型関係も決まってほしい場合は, 型変数に+をつけて「共変(covariant)」であることを指定する必要があります(逆に指定しなかった場合は「不変(invariant)」だと指定したことになります).

class Foo[+X](value: X)
class Bar[+X](value: X) extends Foo[X](value)

val x: Bar[B] = new Bar(new B)
val y: Foo[A] = x

SeqやListの場合も定義には+が登場しますね.

trait Seq[+A] extends ...
Seq 
sealed abstract class List[+A] extends ...
List
反変がほしいケース

+があるなら-もあります. これは「反変(contravariant)」と呼ばれています. ジェネリックな型の部分型関係の向きと, 型引数の部分型関係の向きが逆になるパターンです.

典型的にはこれは関数の引数の型に現れます. Scalaの_ => _の型の実体はFunction1[_, _]というtraitですが, これは次のように定義されています.

trait Function1[-T1, +R] extends AnyRef
Function1

どうしてこうなっているか考えてみましょう. たとえば, B => B型の関数を期待しているところにA => C型の関数を渡すのは安全だから許されてほしいです.

val f: A => C = (a: A) => new C
val g: B => B = f

なぜなら, gを使う場面ではg(b)のようにB型の式bを渡すことになりますが, fはB型を含むより広いA型の値をなんでも渡せるので問題はなく, また, fから返す値はC型で, これはB型より狭く, この値をB型として扱っても問題ないため, gの返り値としても適切だからです.

このとき, A => C <: B => Bなわけですが, 返り値型のC <: Bは同じ向きなのに対して引数型のB <: Aは逆向きです.

逆に, 引数型も同じ向きになっている(共変になっている)場合も許すような言語仕様にしてしまうと安全ではなくなります. たとえば次のような場合です.

class C extends B {
  def somethingOnC(): C = this
}

val f: C => C = (c: C) => c.somethingOnC()
val g: B => B = f // 実際はここでコンパイルエラー

g(new B)

これがコンパイルエラーにならないと, new Bに対して存在しないメソッドsomethingOnC()を呼び出すことになってしまって困りますよね.

変性の性質

少し複雑なパターン

性質を理解するためにもう少し複雑な例を考えてみましょう. 引数として関数を取るような関数の型を考えてみます.

val f1: (C => A) => C = (f: C => A) => new C
val f2: (A => C) => C = (f: A => C) => new C

val g1: (B => B) => B = f1 // OK
val g2: (B => B) => B = f2 // コンパイルエラー

(B => B) => B型を期待するg1にf1を渡すのは合法です. (C => A) => C <: (B => B) => Bになっていることを確認してみましょう. 返り値型は同じ向きでC <: Bだから問題なく, 引数型は逆向きになるのでB => B <: C => Aになっていればよいはずです. この返り値型はB <: Aで, 引数型は逆向きでC <: Bなので問題ありませんね.

一方, g2にf2を渡すのはコンパイルエラーになります. 引数型がB => B <: A => Cとなることが期待されますが, B <: CもA <: Bも成り立ちません.

個々の型引数の部分型関係の向き

さてここで, (S => T) => Rのような型の関数は有用なことがわかり, 名前をつけていろいろ操作できるようにクラス化したとします.

case class UsefulFun[S, T, R](fun: (S => T) => R) {
  def apply(callback: S => T): R = fun(callback)
}

このままだと型引数が不変に指定されているため少し不便です.

val f: UsefulFun[C, A, C] = UsefulFun((f: C => A) => new C)
val g: UsefulFun[B, B, B] = f // コンパイルエラー

fをgに渡せるようにするには, 型引数S, T, Rに適切な変性を指定する必要があります. どう指定するのが正解でしょうか? いったん前節のf1とg1の型を見比べてみましょう.

f1: (C => A) => C
g1: (B => B) => B

前節の議論では, Sの位置の型引数は

f1: (C => A) => C
g1: (B => B) => B

C <: Bになっていることが期待されているのでした. つまり+Sです.

同様にTの位置は,

f1: (C => A) => C
g1: (B => B) => B

B <: Aが期待されるので-Tです.

Rの位置は

f1: (C => A) => C
g1: (B => B) => B

全体の関数型の返り値型なので+Rです.

これらを総合すると, こう定義すればよかったことがわかります.

case class UsefulFun[+S, -T, +R](fun: (S => T) => R) {
  def apply(callback: S => T): R = fun(callback)
}

前節のように一つずつ落ちついて確認していけばどう指定すべきかはわかりますが少し大変ですよね. もう少しなんとかならないものでしょうか.

極性

実は, 各型引数の変性を簡単に計算する方法があります. まず(S => T) => Rの引数型の方に-を, 返り値型の方に+をつけていきます. 

-(-S => +T) => +R

そして=>を足し算だと思って-1倍を括弧の中に分配するとこうなります.

(-(-S) => -(+T)) => +R

掛け算のルールとして

(-1) \times (-1) = +1
(-1) \times (+1) = -1

なので計算してしまうとこうなります.

(+S => -T) => +R

+S, -T, +Rが出てきましたね!

もちろんこれは=>だからではなく, 任意のジェネリック型について同じように計算できます. =>の代わりにFunction1で書くと

Function1[-Function1[-S, +T], +R]

を

Function1[Function1[+S, -T], +R]

と計算してしまってよいということです.

このように, 変性の指定が掛け算の正負のような形で各型引数の部分型関係の向きに反映される性質は極性(polarity)と呼ばれています*1. 逆に言えば, この性質が成り立つためScalaでは変性の記号に+/-を採用しているわけです.

もしこれがoutとinだったら, 「inが偶数回ネストしたらout, 奇数回だったらin」「入ってさらに入ったら出ている, さらにもう1回入ったら入っている」みたいな意味になりますが「お前は何を言っているんだ?」という気持ちになります.

新しい型変数を自分で直接導入する場合以外でも, 型合わせをしていたらたまにこういうコンパイルエラーに遭遇することがあると思います.

contravariant type S occurs in covariant position in type T

このとき「どこがcovariant positionでどこがcontravariant positionなんだ?」と思ったら, 今回の話を思い出してみてください.

歴史

\require{enclose} \def\textsc#1{\dosc#1\csod} \def\dosc#1#2\csod{{\rm #1{\scriptsize #2}}} \def\tinysc#1{\tinydosc#1\tinycsod} \def\tinydosc#1#2\tinycsod{{\rm #1{\tiny #2}}} \def\sout#1{\enclose{horizontalstrike}{#1}} \def\code#1{\texttt{#1}} \def\infrule(#1)#2#3{\displaystyle\frac{#2}{#3}\,(\textsc{#1})} \def\infrulew#1#2(#3)#4#5{\displaystyle\frac{#1}{#2}(\textsc{#3})\frac{#4}{#5}} \def\andalso{\quad\quad} \def\ty|#1|{\left\lfloor #1 \right\rfloor} \def\infer(#1)#2#3{\displaystyle\frac{#3}{#2}\,{\scriptsize (\tinysc{#1})}} \def\inferN#1#2{\displaystyle\frac{#2}{#1}} \def\uninfer(#1)#2#3{\displaystyle\frac{#3}{#2}{\scriptsize \hl{\sout{(\tinysc{#1})}}}} \def\hl#1{{\color{red}{#1}}} \def\subty{<\!\,:} \def\ty{\code{ty}} \def\To{\Rightarrow}

ジェネリックな型の変性の指定を+/-で指定する記法(およびその性質を極性と呼ぶこと)の初出はおそらく以下の辺りの論文だと思われます.

Polarized Higher-Order Subtyping.
Martin Steffen.
Ph.D. thesis, Universität Erlangen-Nürnberg, 1998.

Subtyping for Object Type Constructors.
Dominic Duggan and Adriana Compagnoni.
In the 6th International Workshop on Foundations of Object-Oriented Languages (FOOL6), San Antonio, TX, 1999.

これら以前にも近い性質を極性と呼んだり, 実用として変性に相当することを許すものはもしかしたらあったかもしれませんが, これら以前にはAbadiとCardelliのオブジェクト計算体系\mathbf{Ob}_{\omega \subty \mu}に型変数の変性は導入されていなかったようなので, 理論としてはこれらが初出だと思います. 変性を指定する概念の登場当初から極性の性質は知られており, +/-で表記していたのですね. むしろout/inは後からあえて記法を変えたことになります.

まとめ

  • 反変は典型的には関数型の部分型を考えると必要
  • 反変では部分型関係の向きが逆になる
  • 反変がネストすると偶数回で共変に戻る
  • 偶数回のネストで元に戻るのは掛け算の-と同じだから-で表しており, この性質を極性と呼ぶ

追記 (2022-12-19T19:54+09:00)

>> id:so-apps

Scala には期待していたが、頭がいい人限定言語になってしまったようだ。

https://b.hatena.ne.jp/entry/4729696978372106884/comment/so-apps

>> id:tattyu

Scala難しいな。。

https://b.hatena.ne.jp/entry/4729696978372106884/comment/tattyu

Scalaが難しいという感想まで否定する気はありませんが, このような言い方だと他の言語はもっと簡単であるかのような印象を与えると思うので補足させてください. 今回の内容は, +や-の表記を用いていることを除いて, 他の言語(たとえばC#やKotlin)でも全く同じことが成立する話です.

むしろC#やKotlinではoutやinという表記にして簡単そうに見せている分かえって凶悪とも言えます. Javaに至ってはuse-site varianceというちょっと変わったやり方になっていて, 型理論の専門家が性質を整理するのにJava用に別で1本論文を書く必要があったレベルです. これらの中ではScalaは一番まし, と個人的には思います.

*1:厳密には掛け算のアナロジーが成り立つことだけをもって極性と呼ぶわけではなく, +と-でなんらか逆の向きを表していること, 場面によって向きが入れ替わることなど諸々の特徴もひっくるめて極性と呼ばれていると思います

#Scala #Advent Calendar 2022

tarao 読者になる

広告を非表示にする
コメントを書く