Swiftの型システムを読む その10 - switch文の網羅チェック

November 15, 2017

前回の記事でSpaceを使った網羅チェックのアルゴリズムを見たので、今回はswiftコンパイラに置けるその実装を見てみる。

なお、アルゴリズム・用語・記号の説明はほとんど省略するので、必要に応じて 元の論文前回の記事を参照。

Swiftのバージョンは4.0.2。

Swiftのswitchと網羅チェック

TypeCheckSwitchStmt.cpp のコメントに網羅チェックと警告について参考にした論文が紹介されている。

/// The SpaceEngine encapsulates an algorithm for computing the exhaustiveness
/// of a switch statement using an algebra of spaces described by Fengyun Liu
/// and an algorithm for computing warnings for pattern matching by
/// Luc Maranget.
///
/// The main algorithm centers around the computation of the difference and
/// the intersection of the "Spaces" given in each case, which reduces the
/// definition of exhaustiveness to checking if the difference of the space
/// 'S' of the user's written patterns and the space 'T' of the pattern
/// condition is empty.

網羅チェックはいつ行われるか?

switch文の型チェックの直後に行われる。たとえばcaseに全然関係ない型がある場合などは型チェック時に警告がでて、網羅チェックは限定的にしか行わない。なので基本的には変なpatternが来ることはない。

let a = 1
switch a {
case is String: // ここで"型チェック時に"警告
}
TC.checkSwitchExhaustiveness(S, /*limitChecking*/hadError);

spaceの実装

まずはspaceを構成する𝒪, 𝒯(T), 𝒦(K, s1, s2, …, sn)あたりの実装がどのように行われているかをみてみる。

Spaceはそのまま Space というクラスによって実装されている。

class Space final { 
    ...
}

swiftでの実装ではSpaceはSpaceKindによって分類されており、BooleanConstantが特別扱いされているのが特徴的。

enum class SpaceKind : uint8_t {
    Empty           = 1 << 0, // 空Space 𝒪
    Type            = 1 << 1, // 𝒯(T)
    Constructor     = 1 << 2, // 𝒦(K, s1, s2, ..., sn) 
    Disjunct        = 1 << 3, // s1 | s2 | s3 
    BooleanConstant = 1 << 4,  // true or false
}

上記それぞれのSpaceKindに対してSpaceのコンストラクタがあって、例えば 𝒯(T) にあたるものは以下のように定義されている。

explicit Space(Type T, Identifier NameForPrinting)
    : Kind(SpaceKind::Type), TypeAndVal(T, false), Head(NameForPrinting),
    Spaces({}){}

パターンのspace

パターンからSpaceへの射影 𝒫(p) は そのまま各caseに対応するPatternを受けとってSpaceを返すprojectPattern という関数になっている。

static Space projectPattern(TypeChecker &TC, const Pattern *item, bool &sawDowngradablePattern)

PatternKindで定義された13種類のPatternに対してそれぞれの𝒫に関する規則が定義されている。いくつかピックアップしてみると

𝒫(_) = 𝒯(T)         // マッチさせたい型そのもの
𝒫(true) = 𝒯(true)   // trueはtrue
𝒫(false) = 𝒯(false) // falseはfalse
𝒫(e) = 0             // その他の式(例えば1, 2.0など) はempty
𝒫(_: T) = 0          // 型に関するパターンもempty
𝒫(is T) = 𝒯(T)       // isはその型

// enumのcaseはconstructorに
𝒫(.enumCase(a, b, c)) = 𝒦(.enumCase, s1, s2, ..., sn)

分解(Decompose)の実装

型Tをsubspaceのunionに分解する𝒟(T)と、分解可能かチェックする𝒟? (T)もそのままdecompose, canDecompose という関数になっている。

static void decompose(TypeChecker &TC, Type tp,
                      SmallVectorImpl<Space> &arr) { ... }
static bool canDecompose(Type tp) { ... }

実装を見ると分かる通り、分解できるのは(swiftでは) Bool、 タプル、enum のみ。

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

規則について整理すると、

𝒟?(Bool) = true
𝒟?((T1, T2, ...)) = true
𝒟?(EnumType) = true
𝒟?(x) = false
𝒟(Bool) = { true, false }
𝒟((T1, T2, ...)) = 𝒦("", 𝒯(T1), 𝒯(T2), ...)
𝒟(EnumType) = 𝒦(K1, ...) | 𝒦(K2, ...) |  …

subtraction (⊖) の実装

Swiftの実装では Space::minus として実装されている。

Space minus(const Space &other, TypeChecker &TC) const { ... }

最初のいくつかピックアップして規則を確認すると、ほぼそのまま実装されていることがわかる。

s ⊖ 0 = s
0 ⊖ s = 0
𝒯(T) ⊖ x = 𝒟(T) ⊖ x if 𝒟?(T)
x ⊖ (s1 | s2 | ···) = x ⊖ s1 ⊖ s2 ⊖ ...

特筆すべきところは特にないが、一応(Swift特有の)Boolはこんな感じ。

PAIRCASE (SpaceKind::BooleanConstant, SpaceKind::BooleanConstant): {
  // The difference of boolean constants depends on their values.
  if (this->getBoolValue() == other.getBoolValue()) {
    return Space();
  } else {
    return *this;
  }
}

intersection(⊓)の実装

こちらも Space::intersect として実装されている。

Space intersect(const Space &other, TypeChecker &TC) const { ... }
s ⊓ 0 = 0
0 ⊓ s = 0
x ⊓ (s1 | s2 | ···) = (x ⊓ s1) | (x ⊓ s2) | ...

こちらもだいたいそのままなので略。

subspace関係 (≼) の実装

論文通りならsubtractionを使って

s1 ≼ s2 if s1 ⊖ s2 = 0

のはずだが

// An optimization that computes if the difference of this space and
// another space is empty.
bool isSubspace(const Space &other, TypeChecker &TC) const { ... }

とのことで各組み合わせについて愚直に実装してある。でも基本はsubstractionを使うのものと同じ(はず)

網羅チェックの実装

SpaceEngine::checkExhaustivenessがそれです。 引数のlimitedChecking はすでに前段のSwitchStmtに対しての型チェックが失敗しているときにtrueが来る。

void checkExhaustiveness(bool limitedChecking) { ... }

SpaceEngineSwitchStmt の参照を持っていて、そこからマッチさせたい型や各case(パターン)などを取り出して使う。

SwitchStmt *Switch;
// マッチさせたい型
auto subjectType = Switch->getSubjectExpr()->getType();
// 各caseを取り出して使う
for (auto *caseBlock : Switch->getCases()) {
    ...
}

ここがコアの部分です、。確かにs1 ⊖ s2 = 0をそのまま実装しているけど、結局isSubspaceをつかってないのはなぜ。。。。

auto uncovered = totalSpace.minus(coveredSpace, TC).simplify(TC);
if (uncovered.isEmpty()) {
  return;
}

where句を持つcaseについて

これも理論通り網羅チェックには使えないことが明記されている。

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

その他の用語

いくつか論文中には出てこないものが実装されているので簡単にメモしておく。

  • isUseful メソッドはこのSpaceが網羅チェックに有用かどうかを表す。空Spaceか、空Spaceのunionなどだとfalseが返る。warningに関する論文の方できちんと定義されているっぽい。

  • computeSizeでSpaceのサイズを返す。空Spaceはサイズ0, 𝒯(T)はサイズ1として、𝒦やunionの場合はそれらを構成するSpaceのサイズの合計になる。何に使われるかというとサイズがでかすぎる(= 複雑すぎる)場合にエラーにするようにしている。
  • canDowngrade@_downgrade_exhaustivity_checkという特定のcaseを網羅チェックから外すのに使えるアトリビューション用っぽいが、Swift4では使えない)みたい。

まとめ

Swiftには珍しく(?) きちんと参考論文が書いてあった&ほぼ論文通り実装されていたのと、1ファイルでほぼ閉じているのでとても読みやすかった。

あと、dottyの方の実装をみたらメソッド名などがほとんど同じでこれを参考にして実装したっぽい??

このエントリーをはてなブックマークに追加