kmizuの日記

プログラミングや形式言語に関係のあることを書いたり書かなかったり。

あなたの知らないKotlinのsmart cast(known as Flow-Sensitive Type)

皆さん、Kotlin触っていますか?Kotlinかわいいですよね、Kotlin(どの口がそんなことを言うかって感じですが)。Kotlinにはsmart castという機能があり、安全なキャストができます、というのは不正確で、KotlinはFlow-Sensitive Typeと呼ばれる型システムを持っています。おおざっぱに言えば、制御フローによってある変数や式の型が変わる型システムの総称(だと思います。間違ってたらご指摘願います)Kotlinではそれをsmart cast(と公式ドキュメントには書いてある)と呼んでいるという話のようです。

公式ドキュメントにある例からいくつか引用します:

fun demo(x: Any) {
  if (x is String) {
    print(x.length) // x is automatically cast to String
  }
}
  if (x !is String) return
  print(x.length) // x is automatically cast to String
when (x) {
  is Int -> print(x + 1)
  is String -> print(x.length + 1)
  is IntArray -> print(x.sum())
}
  // x is automatically cast to string on the right-hand side of `||`
  if (x !is String || x.length == 0) return

  // x is automatically cast to string on the right-hand side of `&&`
  if (x is String && x.length > 0)
      print(x.length) // x is automatically cast to String

説明もなんからさらっとして、わかったような、わからないような…と思うかどうかは人それぞれだと思いますが、自分は少なくとも不思議に思いました。そこで、処理系のソースを読まずにいくつかのコードを書いて実験してみました。

まずは準備から。

interface D {
    fun d(): Unit
}

interface A : D{
    fun a(): Unit
}

interface B : D{
    fun b(): Unit
}

class C : A, B {
    override fun a() {
        println("A")
    }
    override fun b() {
        println("B")
    }
    override fun d() {
        println("C")
    }
}

inline fun random(): Boolean = (Math.random() * 2).toInt() == 1

例1:

fun demo1() {
    val x: Any = "FOO"
    if(random() && x is A) {
        x.a() //OK
    }
}

順当な結果ですね。random()trueを返そうが返すまいが、ifの本体が評価されるときには、必ずx is Atrueになるわけですから。まあ、実際のところ、random()は読む人を撹乱するためだけに使っています。

例2:

fun demo2() {
    val x: Any = "FOO"
    if(!(random() || !(x is A))) {
        x.a() //OK
    }
}

より式を複雑にしてみましたが、これもOKです。これは、いうなれば、

if(!random() && !!(x is A)) {
  x.a()
}

としているのと同じわけですが、!!(x is A) = x is Aなので、やっぱりifの本体が評価されるときには、x is Aが成り立っているわけです。ちゃんと論理式を計算しているところがミソです。

例3

fun demo3() {
    val x: Any = "FOO"
    if(false || x is A) {
        x.a() //NG
    }
}

これは意味的にはx is Aと同じになりますが、truefalseといったリテラルは特別扱いの対象ではないようです。

例4

fun demo4() {
    val x: Any = "FOO"
    if(x is A && !(x is A)) {
        x.a() //OK
    }
}

x is A && !(x is A) というのは決してtrueに評価されませんが、もし仮に全体がtrueに評価されるならば、そのときは必ずx is Aが成り立つのでOKということでしょう。ちなみに、順番をひっくり返した次の式でもOKです

例5

fun demo5() {
    val x: Any = "FOO"
    if(!(x is A) && x is A) {
        x.a()
    }
}

これは妥当ですね。次行ってみましょう。

例6

fun demo6() {
    val x: Any = "FOO"
    if(x is A && x is B) {
        x.a() //OK
        x.b() //OK
        x.d() //OK
    }
}

型Aかつ型Bという条件が成り立ったときにどうなるかということですが、両方のメソッドを呼び出すことができています。内部的にはintersection typeのようなものを持っているのではないかと推測されます。

例7

fun demo7() {
    val x: Any = "FOO"
    if(x is A || x is B) {
        x.d() //NG
    }
}

残念ながらこれはNGでした。least upper boundのようなものが計算されることを意図したのですが、union typeとして表現されているのでしょうか。

さて、demo6と同じ意味になる次の式はどうでしょうか。

例8

fun demo8() {
    val x: Any = "FOO"
    if(!(!(x is A) || !(x is B))) {
        x.a() //OK
        x.b() //OK
        x.d() //OK
    }
}

ちゃんとOKになります。賢いですね。次はnullable typeを混ぜてみます。

例9

fun demo9() {
    val x: Any? = null
    if(x is A? && x is B) {
        x.a() //OK
        x.b() //OK
        x.d() //OK
    }
}

次はどうなるでしょう。

例10

fun demo10() {
    val x: Any? = null
    if(x is A? && x is B?) {
        x.a() //NG
        x?.a() //OK
        x?.b() //OK
        x?.d() //OK
    }
}

?.でnullをはずしてやればOKです。内部的には、 (A & B)?という扱いになっているのでしょうか。ややこしいですね。

まとめ

  • KotlinはFlow-Sensitive Typeと一般的(?)に呼ばれる型システムを持っている。
  • 型推論をする上で、is&&||! が特別扱いされている
  • (推測)型のintersectionやunionを内部的に持っている
  • どうやら、nullableとnon-nullableのintersectionも扱える模様
  • シンプルなケース以外でKotlinの型推論の結果を推測するのは自明ではない。というか複雑。
  • 基本的にこの辺の挙動はundocumented(ある程度推測は可能だが)