Swiftコンパイラで採用されているパターンマッチの網羅性チェックの理論と実装

初めまして、@ukitakaです。主にiOS/Swift界隈に生息していて、型についての理解を深めるべく型システム入門を片手に日々Swiftコンパイラの実装を読んで勉強をしています。
今年も型システムには入門失敗しましたが、コードリーディングで得た知見を元にがんばって言語実装アドカレに投稿してみようと思います。。

Swiftではswitch文を使ってパターンマッチを行うことができ、以下のような少し複雑なパターンでも(defaultケースなしに)パターンが網羅されていることをコンパイラが認識してくれます。

enum MyEnum {
    case a
    case b(Bool)
}

let myEnumOpt: MyEnum? = MyEnum.a

switch myEnumOpt {
case .some(.a):
    print("A")
case .some(.b(true)):
    print("true")
case .some(.b(false)):
    print("false")
case .none:
    print("none")
}

逆に、以下のように足りないパターンがあるとコンパイルエラーにしてくれます。

let myEnum: MyEnum = .a

// error: switch must be exhaustive
// note: add missing case: '.b'
switch myEnum {
case .a: print("A")
}

この記事ではこのチェックがどのように実現されているか、背景にあるSpaceという概念を元にしたパターンマッチの網羅性チェックの理論とその実装について、lib/Sema/TypeCheckSwitchStmt.cppとソースコード中で紹介されている論文を元に紹介してみたいと思います。

もちろんすべてを解説すると長くなりすぎてしまうので、**「Swiftコンパイラでの実装が読めるようになる」**ことをゴールに、必要な部分をかいつまんで説明します。

Spaceの導入とsubspace関係を使った"網羅"の定式化

説明は後回しにして、先にコアとなる式を書いてしまいます。

let t: T = ...

switch t {
case p1: ...
case p2: ...
...
}

こんなSwiftのプログラムがあったとして、「網羅されている」ということは以下のように定式化できます。

\mathcal{T}(T) \preceq\mathcal{P}(p_1) \mid \mathcal{P}(p_2) \mid \space ... 

直観的にはこんな感じに読めます。

「型Tがカバーしている部分」 より 「各パターンp1, p2,... がカバーしている部分」の方が大きい

これが成り立つとき**「網羅している」**といえるわけです。シンプルですね！

Space

上では「カバーしている部分」と書きましたがこれをSpaceと呼ぶことにします。
(そのまま"空間"などと訳していいのか自信がなかったのでこの記事ではそのままSpaceでいきます)

Spaceは**「型やパターンがカバーしている値の集合」**です。
上で出てきた記号について説明すると、

• $\mathcal{T}(T)$は型TのSpaceを表す。型Tの値の集合。
• $\mathcal{P}(p)$はパターンpのSpaceを表す。パターンpがカバーしている値の集合。
• $\mathcal{O}$は空space
• $\mid$ はSpaceの和(Disjunction)。和集合のようなイメージ。

subspace関係

上では「大きい」と書きましたが、Space上の二項関係 $\preceq$ を subspace関係 と呼ぶことにします。

s_1 \preceq s_2 

subspace関係を定義するために、もう一つだけ$\ominus$ (subtraction, minus)を新たに導入します。

s_1 \ominus s_2

そしてsubspace関係を以下のように定義します。

s_1 \preceq s_2 \Leftrightarrow s_1 \ominus s_2 = \mathcal{O}

「s2がs1より大きいとは、s1からs2を引くと空になる」のようなイメージです。

必要な定義を駆け足で紹介してしまいましたが、ここまででわかればSwiftの網羅性チェックのメインの流れを読むことができるので、さっそく実際に見て見ましょう。

Swiftの網羅性チェックの実装を読む

lib/Sema/TypeCheckSwitchStmt.cpp のSpaceEngine::checkExhaustiveness が網羅性チェックの実装になります。

主要な部分を抜き出すと、

void checkExhaustiveness(bool limitedChecking) {
    // (略)

    // チェックしたい型の space
    Space totalSpace(subjectType, Identifier());

    // 各パターンの space の disjunction
    Space coveredSpace(spaces);

    // totalSpace ⊖ coveredSpace を計算
    auto uncovered = totalSpace.minus(coveredSpace, TC).simplify(TC);

    // totalSpace ⊖ coveredSpace = O であれば網羅されている
    if (uncovered.isEmpty()) {
        return;
    }

   // 網羅されていない場合はエラーにする処理
   // (略)
}

まさに上で紹介した式がそのまま実装されているのが確認できますね！
メインの流れはわかったので次はminusがどのように実装されているかを見ていきます。

⊖によるsubspace関係の定義

$\preceq$ や $\ominus$ は直観的には集合の包含関係・差ですが、もちろん要素一つ一つをチェックしていくなんてことはせず、型の分解(decompose)を定義していったり、サブタイプ関係を使ったりすることで$\preceq$ や $\ominus$を定義していきます。

例えばAがBのサブタイプであることに基づいて$\preceq$ や $\ominus$ を決めることができます。

\mathcal{T}(A) \preceq \mathcal{T}(B) 

\mathcal{T}(A) \ominus \mathcal{T}(B) = \mathcal{O}

またSwiftでいうとenum/caseに相当する型、型構築子のようなケース(代数的データ型)についてはsubspcaceの和への分解(decompose)を与えることで対応します。たとえば以下のようなenumがあったとして、分解$\mathcal{D}$は以下のように定義できます。

enum E<T, S> {
    case a(T)
    case b(S)
    case c
}

\mathcal{D}(E) = \mathcal{K}(a, T) \mid  \mathcal{K}(b, S) \mid  \mathcal{K}(c)

$\mathcal{K}$は型構築子のSpaceで、$\mathcal{K}$(型構築子の名前, 型 ...)のように表します。

この分解さえ決められれば、以下の例であれば

enum E {
    case a
    case b
    case c
}

let e = E.a

switch e {
case .a: print("a")
case .b: print("b")
case .c: print("c")
}

最初に書いた通り網羅していることは以下のように定式化できるのでした。

\mathcal{T}(E) \preceq (\mathcal{P}(a) \mid \mathcal{P}(b) \mid \mathcal{P}(c))

そしてそれは$\ominus$によって定義されるのでした。以下の式が空Spaceになることを確認していきます。

\mathcal{T}(E) \ominus (\mathcal{P}(a) \mid \mathcal{P}(b) \mid \mathcal{P}(c))

各パターンは型構築子(enumのcase)に対応するのでそのまま$\mathcal{K}$に置き換えます。

\mathcal{T}(E) \ominus (\mathcal{K}(a) \mid \mathcal{K}(b) \mid \mathcal{K}(c))

Eを型構築子のSpaceの和に分解します。

(\mathcal{K}(a) \mid \mathcal{K}(b) \mid \mathcal{K}(c)) \ominus (\mathcal{K}(a) \mid \mathcal{K}(b) \mid \mathcal{K}(c))

あとの細かい計算は省略しますがいくつかの規則にしたがって計算を進めていけば $\mathcal{O}$になりそうなのがわかるかなと思います。

このようにenumの場合は各caseのSpaceの和に分解していくことで $\ominus$ そして $\preceq$ を考えていくことができます。

SwiftのSpaceの実装を読む

SpaceについてはそのままSpaceというクラスで表されています。$\mathcal{T}$などはそれぞれSpaceのコンストラクタに対応していて、そのSpaceが型についてなのか型構築子についてなのかなどはSpaceKindという形で扱われています。

class Space final {
  ...
}

enum class SpaceKind : uint8_t {
  Empty           = 1 << 0,
  Type            = 1 << 1,
  Constructor     = 1 << 2,
  Disjunct        = 1 << 3,
  BooleanConstant = 1 << 4,
};

またBooleanConstantがあるのを見て分かる通り、網羅性チェック時のtrue/falseリテラルに関しては、あたかも以下のようなenumであるかのように扱われています。

enum Bool {
  case true
  case false
}

パターンのSpace $\mathcal{P}$はprojectPatternという関数で実装されていて、直接いずれかのSpaceKindを持ったSpaceに変換されます。

// Recursively project a pattern into a Space.
static Space projectPattern(TypeChecker &TC, const Pattern *item,
                            bool &sawDowngradablePattern) { ... }

分解についてはそのままdecomposeという関数で実装されていて、タプル、enum、Boolについてのみ定義されていることがcanDecomposeを見るとわかります。

static bool canDecompose(Type tp) {
  return tp->is<TupleType>() || tp->isBool()
      || tp->getEnumOrBoundGenericEnum();
}

肝心の $\ominus$の実装はすでに見た通りminusという関数で実装されていて、SpaceKindの組み合わせごとに規則が用意されています。

Space minus(const Space &other, TypeChecker &TC) const {
  // ...
  switch (PairSwitch(this->getKind(), other.getKind())) {
  PAIRCASE (SpaceKind::Type, SpaceKind::Type): { ... }
  PAIRCASE (SpaceKind::Type, SpaceKind::Constructor): { ... }
  // 以下すべての組み合わせについて...
  }
}

網羅性チェックが行えないパターン

元の論文でも言われている通り、あくまでも型や型構築子の関係に基づいて定義されるため、値に直接言及するようなパターン(Swiftでいうとwhere付きのcase)は網羅性チェックには使えません。

// 'where'-clauses on cases mean the case does not contribute to
// the exhaustiveness of the pattern.
if (caseItem.getGuardExpr())
    continue;

enum E {
  case a
  case b(Bool)
}

let e = E.a

// 実際には網羅されていてもコンパイラはそれを認識できない
// error: switch must be exhaustive
switch e {
case .a:
  print("a")
case .b(let bool) where bool == true:
  print("b - true")
case .b(let bool) where bool == false:
  print("b - false")
}

また、一意に分解が定義できないようなIntなどの型についてもチェックは行えません。

let i = 1

// error: switch must be exhaustive
switch i {
case (..<0): print("negative")
case (0...): print("zero or positive")
}

追記: 冗長性(Redundancy)検査について

Swiftでは重複するcaseがある場合は警告を出してくれます。

enum E {
    case a, b, c
}

let e = E.a

switch e {
case .a: print("a")
case .b: print("b")
case .c: print("c")
// Warning: Case is already handled by previous patterns; consider removing it
case .a: print("a")
}

これも各パターンのDisjunctionを考える際にsubspace関係を調べることによってチェックしています。

\mathcal{T}(E) \preceq \mathcal{P}(a) \mid \mathcal{P}(b) \mid \mathcal{P}(c) \mid \mathcal{P}(a)

上の例であれば,まず$\mathcal{P}(a)$と$\mathcal{P}(b)$のDisjunctionを考えますが、その際に

\mathcal{P}(b) \preceq \mathcal{P}(a)

をチェックします。もしsubspace関係があればすでにそのパターンのSpaceはカバーされていることになるので、冗長と判断できます。
上の例であれば4つ目のcase .aの時点で

\mathcal{P}(a) \preceq \mathcal{P}(a) \mid \mathcal{P}(b) \mid \mathcal{P}(c)

が成立してしまうので警告がでます。
Swiftの実装でいうと以下の部分です。

auto projection = projectPattern(TC, caseItem.getPattern(),
                                 sawDowngradablePattern);
if (projection.isUseful()
      && projection.isSubspace(Space(spaces), TC)) {
  sawRedundantPattern |= true;

  TC.diagnose(caseItem.getStartLoc(),
                diag::redundant_particular_case)
    .highlight(caseItem.getSourceRange());
}

ただし検査できるのはsubspace関係になるパターンのみです。Spaceの一部が重複しているようなケースはこの方式では検出できません。

まとめ

Swiftコンパイラの網羅性チェックについての理論と実際の実装をざっくりですが確認しました。
「Swiftの」と言ってしまっていますが、元々はScalaのdottyというコンパイラで採用されているものをSwiftに移植してきたものであり、実装をみてみると関数名などほぼそのまま使われていることが確認できます。ありがとうScala先輩。

ほぼ1ファイル1500行くらいで完結していて、珍しく参考文献も示されており、Swiftコンパイラのソースの中ではかなり読みやすい部類に入ると思うので、パターンマッチでなにかおかしなことが起きた際にはぜひソースを追ってみてください！！

参考文献

• Liu, Fengyun 2016 - A generic algorithm for checking exhaustivity of pattern matching

  • ソースコード中で紹介されている論文です。

• apple/swift - lib/Sema/TypeCheckSwitchStmt.cpp

  • Redo Exhaustiveness Analysis by CodaFi · Pull Request #8908 · apple/swift · GitHub
  • このp-rからなので、おそらくSwift4あたりから採用されている？
  • 一応PatternMatch.rstというドキュメントがありますが、Swift1.0のときのものなので参考になりません。