このドキュメントでは，Swiftにおける型検査器の設計と実装について説明する． 型検査器の修正，拡張，改良をしたい開発者，あるいは型検査器がどのように働くかを深く理解したいだけの開発者に向けたものである． Swiftに精通していることが前提である．
Swift及びその型システムには，クラスによるオブジェクト指向プログラミング，関数や演算子のオーバーロード，派生型，制約付きパラメータ多相性などの一般的な言語機能が多く組み込まれている． Swiftでは型推論を広範囲に用いており，多くの変数や式で型を省略することができるようになっている．
例えば：
func round(_ x: Double) -> Int { /* ... */ }
var pi: Double = 3.14159
var three = round(pi) // 'three' の型は 'Int'
func identity<T>(_ x: T) -> T { return x }
var eFloat: Float = -identity(2.71828) // 数値リテラルの型は 'Float' になるSwiftの型推論は型情報が2方向に流れることを可能にしている．
主流言語のほとんどと同様，型情報は式木の葉(例えば浮動小数を参照する表現 pi)から根(変数 three の型)への上方向に流れることができる．
しかし，Swiftでは，型情報は式木の根にあるコンテキスト(例えば eFloat の固定型)から葉(数値リテラル 2.71828 の型)への下方向に流れることもできる．
この双方向型推論は，MLのような型システムを使う言語では一般的だが，C++，Java，C#，Objective-Cのような主流言語には存在しない．
Swiftでは，古典的なHindley-Milner型推論アルゴリズムを彷彿とさせる，制約ベースの型検査器を用いて双方向型推論を実装している． 制約システムを用いることで，ソルバーの実際の実装から切り離された言語意味論における，率直で一般的な表現が可能になる． ソルバーが性能と診断の改善のために時間の経過とともに進化していく一方で，制約自体は比較的安定していると予想される．
Swiftには，制約付き多相型や関数オーバーロードといった，Hindley-Milner型システムにない機能がいくつか含まれており，体裁や実装が多少複雑になる．
一方で，純粋に実用的な理由から，Swiftは型推論のスコープを単一式や単一文に限定している： 問題のスコープが限定されていれば，より良いパフォーマンスと非常に優れた診断を行えると考えられる．
型検査は3つの主な段階で実施される：
Constraint Generation_
入力式や(場合によっては)追加のコンテキスト情報が与えられ，様々な部分式の型の間の関係を表す型制約の集合を生成する．
生成された制約には，型変数によって表される未知の型が含まれることがあり，これはソルバーによって決定される．
Constraint Solving_
制約システム中の型変数それぞれに具体的な型を割り当て，制約システムを解く．
制約ソルバーは，様々な選択肢の中で可能な限りもっとも具体的な解を示す必要がある．
Solution Application_
入力式，式から生成された型制約の集合，各型変数への具体的な型の割り当ての集合が与えられ，全ての暗黙の変換(及び他の変換)を明示的にし全ての不明な型とオーバーロードを解決するような適切に型付けされた式を生成する．
このステップは失敗しない．
入力式、その式から生成された型制約のセット、および各型変数への具体的な型の割り当てのセットは、すべての暗黙の変換（および他の変換）を明示的にし、すべてを解決する適切な型の式を生成します 不明なタイプと過負荷。
以下の章では，これら3つの型検査の段階，パフォーマンスと診断の問題について説明する．
制約システムは型制約の集合からなる．
各型制約は単一型(例えば整数のリテラル型)に対する要求や2つの型(例えば1つはもう1つの派生型)に関係する．
制約で表現された型は，組み込み型やタプル型，関数型，列挙型/構造体/クラス型，プロトコル型，総称型といったSwiftの型システムの任意の型となりうる．
さらに，型は型変数 T (通常，必要に応じて T0 ， T1 ， T2 などと番号がつけられる)となることがある．
型変数は他の型の代わりに使うことができ，例えばタプル型 (T0, Int, (T0) -> Int) は型変数 T0 を含む．
Swiftの型システムの表現のため，様々な種類の制約がある：
同一性
同一性制約は2つの型が同一であることを要求する．
例えば，制約 T0 == T1 は T0 と T1 が同じ具体型束縛を持つことを効果的に保証する．
同一性制約には2つの異なる種類がある：
* 厳密な同一性制約，つまり束縛で，ある型変数 T0 と型 X に対し T0 := X と書き，これは T0 が厳密に X と同一であることを要求する
* 同一性制約で，型 X と Y に対し X == Y と書き，これは X と Y が同じ型を持ち，作業中は左辺値の型を無視する．例えば，制約 T0 = X は T0 を 型 X に割り当て型 @lvalue X に T0 を割り当てることで充足する．
派生型
派生型制約は，1つ目の型が2つ目の型と同一または派生型であることを要求する．例えば，クラス型 Dog がクラス型 Animal を直接または間接的に継承していれば， Dog は Animal の派生型である．派生型制約は X < Y と書く．
変換
変換制約は，1つ目の型が2つ目の型に変換可能であることを要求し，これには派生型及び同一性が含まれる．また，ユーザー定義の変換関数を呼び出すことができる．変換制約は X <c Y と書き，これは「 X は Y に変換可能」と読む．
コンストラクション
コンストラクション制約は X <C Y と書き，2つ目の型が1つ目の型の値を受け取るコンストラクタを持つ名前型であることを要求する．例えば，制約 Int <C String は String が Int を受けるコンストラクタを持つことから充足する．
メンバー
メンバー制約 X[.name] == Y は，1つ目の型( X )が与えられた名前のメンバー(またはオーバーロードされたメンバーの集合)を持ち，そのメンバーの型が2番目の型( Y )に束縛されていることを意味する．メンバー制約には2つの種類がある：式コンテキスト内のメンバーを参照する値メンバー制約と，型コンテキスト中のメンバーを参照する(つまり型のみを参照できる)型メンバー制約である．
適合性
適合性制約 X conforms to Y は，1つ目の型( X )がプロトコル( Y )に従わなければならないことを示す．
検査済みキャスト
1つ目の型から2つ目の型への検査済みキャストを示す制約 x as T
適用可能関数 適用可能関数は，両方が同じ入出力型を持つ関数型であることを要求する．関数適用の目的で，左辺の関数型を入力型と出力型に分割する時に用いる．マッチングに型属性を必要としないことに注意する．
オーバーロード束縛 オーバーロード束縛制約は，オーバーロード集合から特定の選択肢を選ぶことで型変数を束縛する．複数のオーバーロードは選言制約によって表される．
連言 2つ以上の他の制約の連言である制約．一般的には選言で用いられる．
選言 2つ以上の制約の選言である制約． Disjunctions are used to model different decisions that the solver could make, i.e., the sets of overloaded functions from which the solver could choose, or different potential conversions, each of which might resolve in a (different) solution.
原型 原型制約は，制約付き型を原型に束縛することを要求する．これはプロトコル内で演算子の呼び出しを行うためだけに用いられる非常に特殊な種類の制約である．
クラス クラス制約は，制約付き型をクラス型に束縛することを要求する．
プロトコルのSelfオブジェクト
内部使用のみの制約で， Self 型のプロトコルへの適合を示す．これは適合性制約に似ているが，(たとえ存在する型が自己プロトコルに準拠しない場合でも)プロトコル型が自己プロトコルのselfオブジェクトであることを許可するため，より「ゆるい」ものである．
動的検索値 制約付き型がDynamicLookupまたはその左辺値であることを要求する制約．
制約生成の段階では，式中の様々な部分式の型を関連付ける制約システムを生成する． プログラムにより，制約生成は葉から根に向かって式を走査し、各部分式に型(しばしば型変数を含む)を割り当てる．
制約生成は式の構文によって駆動され，異なる種の式(関数適用やメンバーアクセス等)は特殊な制約集合を生成する．
ここでは，言語における主な式の種類を列挙し，その式に割り当てられる型と式から生成される制約を説明する．
部分式 a に割り当てられた型を参照するために T(a) を用いる．
一次式の種類から生成される制約と型は次の通り：
宣言参照
宣言 x を参照する式には， x への参照の型が割り当てられる．例えば，もし x が var x: Int と宣言されたとすると，式 x には型 @lvalue Int が割り当てられる．制約は生成されない．
名前がオーバーロード宣言の集合を参照する場合，ソルバーにより適切な宣言が選択される．この問題についてはオーバーロード章で議論する．
また，名前が総称関数や総称型を参照する場合，宣言参照は新しい型変数を導入することがある．詳しくは多相型章で議論する．
メンバー参照
メンバー参照式 a.b では，新しい型変数 T0 に型 T0 が割り当てられる．
さらに，この式は値メンバー制約 T(a).b == T0 を生成する．
メンバー参照は，最終的に名前型のメンバーやタプルの要素に決定されることがある．後者の場合，名前( b )が識別子または位置引数(例えば 1 )のいずれかであることがある．
メンバー制約の解決はオーバーロード宣言の集合を参照できることに注意する．詳しくはオーバーロード章で
未解決メンバー参照
未解決メンバー参照 .name は列挙型のメンバーを参照する．列挙型は，新しい変数型 T0 (コンテキストからしか知ることができないため)と，新しい型変数 T1 に対する値メンバー制約 T0.name == T1 を持っていることが想定され， まだ知られていない型 T1 を持ち name と名付けられたメンバーを持つことを捕捉する．
未解決メンバー参照の型は T1 であり，これはメンバーの型である．
未解決メンバー参照が実際には .name(x) の呼び出しである時，関数適用は未解決メンバー参照により生成された制約に折りたたまれる．
上記制約システムは，実際には追加コンテキスト情報なしで型 T0 の決定のための不十分な情報しか持っていないことに注意する．
オーバーロード章でこの問題の解決のためにオーバーロード選択メカニズムがどのように用いられるか説明する．
関数適用
関数適用 a(b) は2つの制約を生成する．まず，適切な関数の制約 T0 -> T1 ==Fn T(a) (型変数 T0 T1 に対する)は，その関数( a )に適用された右辺値から左辺値への変換を捕捉し，関数の型を引数と結果の型に分解する．次に，変換制約 T(b) <c T0 は，実引数型( b )が関数の引数型に変換可能であるという要求を得る．
最後に，式には型 T1 ，すなわち関数の結果型が与えられる．
コンストラクション
型コンストラクション A(b) は， A が型を参照しており，コンストラクション制約 T(b) <C A を生成し，これは A が b を受けるコンストラクタを持つことを要求する．式の型は A である．
コンストラクションと関数適用は同じ構文を用いることに注意する．ここで，制約生成器は関数引数(上の説明では A または a )の型のシャロー解析を行う．もし明らかにメタタイプ型の場合，式は関数適用ではなく強制またはコンストラクションと見なされる．
言語のこの領域はより多くの作業を必要とする．
添え字
添え字演算 a[b] は関数適用と似ている．値メンバー制約 T(a).subscript == T0 -> T1 は，それぞれ T0 と T1 という新しい型変数で表される，キー型から値型への関数として添え字を扱う．
制約 T(b) <c T0 はキー型へ変換可能な型引数を要求し，添え字演算の型は T1 である．
リテラル
17 ， 1.5 ， "Hello, world!" のようなリテラル式は，新しい型変数 T0 に割り当てられる．さらに，リテラルの種類に応じて型変数にリテラル制約が設定される．例えば「 T0 は整数リテラル」
クロージャ
パラメータと戻り値の型に応じてクロージャーに関数型が割り当てられる．
パラメータに指定の型がない場合や位置的( $1 や $2 など)の場合，型をキャプチャするために新しい型変数を割り当てる．
同様に，戻り値の型が省略されると新しい型の変数を割り当てる．
クロージャの本体が単一式である場合，式は包含する式の型検査に直接関与する．それ以外の場合では，コンテキストの型検査により完全な関数型が計算されると，クロージャの本体が個別に型検査される．
配列割り当て
配列割り当て new A[s] には型 A[] が割り当てられる．
型検査器は(個別に) T(s) が配列の境界型であることを検査する．
Address of
アドレス式 &a は常に @inout 型を返す．
従って，新しい型変数 T0 について @inout T0 型が割り当てられる．
派生型制約 @inout T0 < @lvalue T(a) は，入力式がある型の左辺値であるという要件を示す．
したがって、新しいタイプの変数 T0に @inout T0型が割り当てられます。
三項演算子
三項演算子 x ? y : z はいくつかの制約を生成する．
型 T(x) はどの分岐を選ぶかを決定するために LogicValue プロトコルに従わなければならない．
次に，新しい型変数 T0 を導入して戻り値の型を取得し，制約 T(y) <c T0 と T(z) <c T0 は，共通の型へ変換するための三項演算子の両方の分岐に対する要求を得る．
この言語には他にもいくつかの式の種類がある．制約へのマッピングについては制約生成器を参照すること．
オーバーロードは複数の異なる定義を同じ名前に与えるプロセスである．例えば， negate 関数を Int 型と Double 型の両方に対して働くようにオーバーロードするかもしれない．
例えば：
func negate(_ x: Int) -> Int { return -x }
func negate(_ x: Double) -> Double { return -x }negate の2つの定義があるとすると，宣言参照式 negate の型は何か？
もし最初のオーバーロードを選択した場合，型は (Int) -> Int である．2つ目のオーバーロードの場合，型は (Double) -> Double である．
しかし，制約生成では何か特定の型を式に割り当てる必要があるため，親式はその型を参照することができる．
型検査器におけるオーバーロードは，新しい型変数( T0 と呼ぶ)をオーバーロードされた宣言への参照の型に導入することでモデル化される．
次に選言制約が導入され，各項は(厳密な同一性制約により)型変数をオーバーロード集合中のオーバーロード1つから生成される型に束縛する．
negate の例では，選言は T0 := (Int) -> Int or T0 := (Double) -> Double である．
後のConstraint Solving章で説明する制約ソルバーは可能な束縛両方を探索し，オーバーロードされた参照は全ての制約を充足する解の束縛結果を
The constraint solver, discussed in the later section on Constraint Solving, explores both possible bindings, and the overloaded reference resolves to whichever binding results in a solution that satisfies all constraints.
オーバーロードは，オーバーロードされた宣言の集合を参照する式と，最終的にオーバーロードされた宣言の集合を解決するメンバー制約の両方により導入される．
特に興味深い例の1つとして未解決メンバー参照，例えば .name がある．
前章で述べたように，これは制約 T0.name == T1 を生成し，ここで T0 は列挙型に束縛される新しい型変数， T1 は選択したメンバーの型に束縛される新しい型変数である．
前章で述べた問題とは，この制約がソルバーに対し，推論なしで T0 を決定するための十分な情報を与えないことである．
しかし，列挙型メンバーの型は実際には規則的な構造を持っていることに注意する．
例として Optional 型を考える：
enum Optional<T> {
case None
case Some(T)
}Optional<T>.None の型は Optional<T> だが， Optional<T>.Some の型は (T) -> Optional<T> である．
実際，列挙型の要素は2つの形式のうち1つを持つことができる：追加のデータを持たない列挙型の要素は T0 ， T2 が列挙型の要素に付属したデータのとき T2 -> T0 である．
後者の場合，実際の引数は未解決メンバー参照の一部としてパースされるため，関数適用制約は入力型 T2 への変換を記述する．
Swiftには総称型があり，総称型とは多相型と多相関数を可能にする制約付きパラメータ多相性である．
例えば min 関数を実装することができる：
func min<T : Comparable>(x: T, y: T) -> T {
if y < x { return y }
return x
}ここで， T はプロトコル Comparable に従う任意の具体的な型に置き換え可能な総称パラメータである．
min の型は(内部的には) <T: Comparable> (x: T, y: T) -> T と書くことができ，これは
「 Comparable に従う全ての T に関して，関数の型は (x: T, y: T) -> T である」と読むことができる．
min 関数の異なる使い方は，総称パラメータ T に異なる束縛を与えることがある．
制約生成器が総称関数への参照を検出すると，直ちに関数型内の各総称パラメーターを新しい型変数に置き換え，総称関数であげられた制約に一致するように型変数に対して制約を導入し，新しく生成された型変数をもとに単相的関数型を生成する．
例えば，最初の宣言参照式 min で，型 (x: T0, y: T0) -> T0 になる．ここで T0 は新しい型変数であり，プロトコル準拠を表現する派生型制約 T0 < Comparable を含む．次の宣言参照式 min により型 (x: T1, y: T1) -> T1 が生成される．ここで T1 は新しい型変数(したがって T0 とは異なる)である．
この置換処理は総称関数型を「開く」と呼ばれ，ソルバーの複雑化なしに制約システム中の多相関数の使用をモデル化するためのかなり単純な(しかし効果的な)方法である．
Swiftは第一級多相関数をサポートしておらず，例えば <T> T -> T 型の変数を宣言できないので，直ちに総称関数型を開くことのみ有効である．
総称型の使用も制約ソルバーにより直ちに開かれる．例えば次の総称辞書型を考える：
class Dictionary<Key : Hashable, Value> {
// ...
}制約ソルバーが式 Dictionary() に遭遇すると，新しい型変数 T0 と T1 について型 Dictionary ーーこれは任意の総称引数と共に生成されないーーを開いて型 Dictionary<T0, T1> とし，制約 T0 conforms to Hashable を生成する．
これにより，式のコンテキストによって辞書の実際のキーの型と値の型を判別することができる．
第一級多相関数について上述したように，非結合総称型，つまり総称引数を指定していない総称型は総称引数が推測できる場所以外では使用できないため，直ちに開くことは有効である．
制約ソルバーの主な目的は，制約の集合を受け取り，制約システム内の各型変数に対し最も具体的な型の束縛を決定することである． この決定の一環として，制約ソルバーはオーバーロードの1つを選択することでオーバーロードされた宣言参照を解決する．
最悪の場合，Swiftが生成した制約システムを解くことが指数関数時間を要することがある． 古典的なHindley-Milner型推論アルゴリズムでさえ指数関数時間が必要であり，Swift型システムはさらなる複雑さ，特にオーバーロード解決を生じる． しかし，特定の式に関する問題のサイズは依然としてかなり小さく，制約ソルバーはパフォーマンス向上のために多くの小技を使用できる． パフォーマンス章では実装済みまたは計画されているいくつかの小技を紹介しているが，今後追加の小技を加えてソルバーを拡張する予定である．
本章では，ソルバーの設計の背後にある基本的な考え方と，それが適用される型ルールに焦点をあてる．
制約生成プロセスは，直接(解が明白で些細なため)またはいくつかの小さな制約に分割することで直ちに解くことのできる制約を多く導入している． 簡略化と呼ばれるこのプロセスは，constraint solvingののちの段階のために制約システムを正規化する． これは，制約ソルバーが(例えばオーバーロードの解決や型変数の束縛などで)推論を行うたびに再度呼び出される．そのような推測のたびに他の正規化が行われることが多いためである． 全ての型変数とオーバーロードが解決された時，充足しない単純な制約を検出するか(これは適切な解ではない)，制約集合から単純に充足される単純な制約へ削減することにより，正規化はconstraint solvingのプロセスを終了させる．
単純化プロセスは，制約をより簡単な制約に分解し，異なる各種類の制約はSwift型システムに基づく異なるルールによって処理される． 制約は5つのカテゴリに分類される： 関係制約，メンバー制約，型プロパティ，連言，選言． このうち最初の3種の制約のみが興味深く単純なルールを持っており，以下の章で説明する．
関係制約は2つの型間の関係を表す． このカテゴリーは，同一性，部分型，変換制約をカバーし，最も一般的な簡略化をもたらす． 関係制約の単純化では，追加の制約を生成するために2つの型の構造を比較しSwiftの型ルールを適用する． 関係制約の単純化は、2つのタイプの構造を比較し、Swift言語のタイピングルールを適用して追加の制約を生成することによって行われます。 例えば，制約が変換制約である場合：
A -> B <c C -> D
両方の型が関数型であり，関数型に関する変換ルールを適用することでこの制約をより小さい制約 C < A および B < D に分解できる．
同様に，言語の型ルールに基づき，より簡単な要件を生成するために様々な型コンストラクタ(タプル型，総称型の特殊化，左辺値型など)の全てを破棄することができる．
1つまたは両方の辺の型変数を含む関係制約は一般的には直接解くことができない．
むしろ，これらの制約は，可能な型束縛を与えることにより後で情報を与えるものであり，これは型変数束縛の章で説明する．
例外は2つの型変数間の同一性制約であり，例えば T0 == T1 がある．
例外は、2つの型変数間の等価制約、例えば T0 == T1です。
これらの制約は，制約が型変数の1つに対する束縛を決定するだけでよいように(他も同じ束縛を用いる)，(基本的な和集合探索アルゴリズムを用いて) T0 と T1 の同一クラスを統一することで単純化する．
Member constraints specify that a certain type has a member of a given
name and provide a binding for the type of that member. A member
constraint A.member == B can be simplified when the type of A
is determined to be a nominal or tuple type, in which case name lookup
can resolve the member name to an actual declaration. That declaration
has some type C, so the member constraint is simplified to the
exact equality constraint B := C.
The member name may refer to a set of overloaded declarations. In this
case, the type C is a fresh type variable (call it T0). A
disjunction constraint is introduced, each term of which new overload
set binds a different declaration's type to T0, as described in
the section on Overloading_.
The kind of member constraint---type or value---also affects the
declaration type C. A type constraint can only refer to member
types, and C will be the declared type of the named member. A
value constraint, on the other hand, can refer to either a type or a
value, and C is the type of a reference to that entity. For a
reference to a type, C will be a metatype of the declared type.
The basic approach to constraint solving is to simplify the constraints until they can no longer be simplified, then produce (and check) educated guesses about which declaration from an overload set should be selected or what concrete type should be bound to a given type variable. Each guess is tested as an assumption, possibly with other guesses, until the solver either arrives at a solution or concludes that the guess was incorrect.
Within the implementation, each guess is modeled as an assumption within a new solver scope. The solver scope inherits all of the constraints, overload selections, and type variable bindings of its parent solver scope, then adds one more guess. As such, the solution space explored by the solver can be viewed as a tree, where the top-most node is the constraint system generated directly from the expression. The leaves of the tree are either solutions to the type-checking problem (where all constraints have been simplified away) or represent sets of assumptions that do not lead to a solution.
The following sections describe the techniques used by the solver to produce derived constraint systems that explore the solution space.
Overload selection is the simplest way to make an assumption. For an
overload set that introduced a disjunction constraint
T0 := A1 or T0 := A2 or ... or T0 := AN into the constraint
system, each term in the disjunction will be visited separately. Each
solver state binds the type variable T0 and explores
whether the selected overload leads to a suitable solution.
A second way in which the solver makes assumptions is to guess at the concrete type to which a given type variable should be bound. That type binding is then introduced in a new, derived constraint system to determine if the binding is feasible.
The solver does not conjure concrete type bindings from nothing, nor does it perform an exhaustive search. Rather, it uses the constraints placed on that type variable to produce potential candidate types. There are several strategies employed by the solver.
A given type variable T0 often has relational constraints
placed on it that relate it to concrete types, e.g., T0 <c Int or
Float <c T0. In these cases, we can use the concrete types as a
starting point to make educated guesses for the type T0.
To determine an appropriate guess, the relational constraints placed
on the type variable are categorized. Given a relational constraint of the form
T0 <? A (where <? is one of <, <t, or <c), where
A is some concrete type, A is said to be "above"
T0. Similarly, given a constraint of the form B <? T0 for a
concrete type B, B is said to be "below" T0. The
above/below terminologies comes from a visualization of the lattice of
types formed by the conversion relationship, e.g., there is an edge
A -> B in the latter if A is convertible to B. B would
therefore be higher in the lattice than A, and the topmost element
of the lattice is the element to which all types can be converted,
Any (often called "top").
The concrete types "above" and "below" a given type variable provide bounds on the possible concrete types that can be assigned to that type variable. The solver computes [#]_ the join of the types "below" the type variable, i.e., the most specific (lowest) type to which all of the types "below" can be converted, and uses that join as a starting guess.
The join of the "below" types computed as a starting point may be too
specific, due to constraints that involve the type variable but
weren't simple enough to consider as part of the join. To cope with
such cases, if no solution can be found with the join of the "below"
types, the solver creates a new set of derived constraint systems with
weaker assumptions, corresponding to each of the types that the join
is directly convertible to. For example, if the join was some class
Derived, the supertype fallback would then try the class Base
from which Derived directly inherits. This fallback process
continues until the types produced are no longer convertible to the
meet of types "above" the type variable, i.e., the least specific
(highest) type from which all of the types "above" the type variable
can be converted [#]_.
If a type variable is bound by a conformance constraint to one of the
literal protocols, "T0 conforms to ExpressibleByIntegerLiteral",
then the constraint solver will guess that the type variable can be
bound to the default literal type for that protocol. For example,
T0 would get the default integer literal type Int, allowing
one to type-check expressions with too little type information to
determine the types of these literals, e.g., -1.
The solver explores a potentially large solution space, and it is possible that it will find multiple solutions to the constraint system as given. Such cases are not necessarily ambiguities, because the solver can then compare the solutions to determine whether one of the solutions is better than all of the others. To do so, it computes a "score" for each solution based on a number of factors:
- How many user-defined conversions were applied.
- How many non-trivial function conversions were applied.
- How many literals were given "non-default" types.
Solutions with smaller scores are considered better solutions. When two solutions have the same score, the type variables and overload choices of the two systems are compared to produce a relative score:
-
If the two solutions have selected different type variable bindings for a type variable where a "more specific" type variable is a better match, and one of the type variable bindings is a subtype of the other, the solution with the subtype earns +1.
-
If an overload set has different selected overloads in the two solutions, the overloads are compared. If the type of the overload picked in one solution is a subtype of the type of the overload picked in the other solution, then first solution earns +1.
The solution with the greater relative score is considered to be better than the other solution.
Once the solver has produced a solution to the constraint system, that solution must be applied to the original expression to produce a fully type-checked expression that makes all implicit conversions and resolved overloads explicit. This application process walks the expression tree from the leaves to the root, rewriting each expression node based on the kind of expression:
Declaration references
Declaration references are rewritten with the precise type of the
declaration as referenced. For overloaded declaration references, the
Overload*Expr node is replaced with a simple declaration
reference expression. For references to polymorphic functions or
members of generic types, a SpecializeExpr node is introduced to
provide substitutions for all of the generic parameters.
Member references References to members are similar to declaration references. However, they have the added constraint that the base expression needs to be a reference. Therefore, an rvalue of non-reference type will be materialized to produce the necessary reference.
Literals Literals are converted to the appropriate literal type, which typically involves introducing calls to the witnesses for the appropriate literal protocols.
Closures Since the closure has acquired a complete function type, the body of the closure is type-checked with that complete function type.
The solution application step cannot fail for any type checking rule modeled by the constraint system. However, there are some failures that are intentionally left to the solution application phase, such as a postfix '!' applied to a non-optional type.
During constraint generation and solving, numerous constraints are created, broken apart, and solved. During constraint application as well as during diagnostics emission, it is important to track the relationship between the constraints and the actual expressions from which they originally came. For example, consider the following type checking problem::
struct X { // user-defined conversions func [conversion] __conversion () -> String { /* ... / } func [conversion] __conversion () -> Int { / ... */ } }
func f(_ i : Int, s : String) { }
var x : X f(10.5, x)
This constraint system generates the constraints "T(f) ==Fn T0 -> T1" (for fresh variables T0 and T1), "(T2, X) <c T0" (for fresh variable T2) and "T2 conforms to
ExpressibleByFloatLiteral". As part of the solution, after T0 is
replaced with (i : Int, s : String), the second of
these constraints is broken down into "T2 <c Int" and "X <c String". These two constraints are interesting for different
reasons: the first will fail, because Int does not conform to
ExpressibleByFloatLiteral. The second will succeed by selecting one
of the (overloaded) conversion functions.
In both of these cases, we need to map the actual constraint of
interest back to the expressions they refer to. In the first case, we
want to report not only that the failure occurred because Int is
not ExpressibleByFloatLiteral, but we also want to point out where
the Int type actually came from, i.e., in the parameter. In the
second case, we want to determine which of the overloaded conversion
functions was selected to perform the conversion, so that conversion
function can be called by constraint application if all else succeeds.
Locators address both issues by tracking the location and derivation
of constraints. Each locator is anchored at a specific expression,
i.e., the function application f(10.5, x), and contains a path of
zero or more derivation steps from that anchor. For example, the
"T(f) ==Fn T0 -> T1" constraint has a locator that is
anchored at the function application and a path with the "apply
function" derivation step, meaning that this is the function being
applied. Similarly, the "(T2, X) <c T0 constraint has a
locator anchored at the function application and a path with the
"apply argument" derivation step, meaning that this is the argument
to the function.
When constraints are simplified, the resulting constraints have
locators with longer paths. For example, when a conversion constraint between two
tuples is simplified conversion constraints between the corresponding
tuple elements, the resulting locators refer to specific elements. For
example, the T2 <c Int constraint will be anchored at the function
application (still), and have two derivation steps in its path: the
"apply function" derivation step from its parent constraint followed
by the "tuple element 0" constraint that refers to this specific tuple
element. Similarly, the X <c String constraint will have the same
locator, but with "tuple element 1" rather than "tuple element 0". The
ConstraintLocator type in the constraint solver has a number of
different derivation step kinds (called "path elements" in the source)
that describe the various ways in which larger constraints can be
broken down into smaller ones.
Whenever the solver creates a new overload set, that overload set is
associated with a particular locator. Continuing the example from the
parent section, the solver will create an overload set containing the
two user-defined conversions. This overload set is created while
simplifying the constraint X <c String, so it uses the locator
from that constraint extended by a "conversion member" derivation
step. The complete locator for this overload set is, therefore::
function application -> apply argument -> tuple element #1 -> conversion member
When the solver selects a particular overload from the overload set, it records the selected overload based on the locator of the overload set. When it comes time to perform constraint application, the locator is recreated based on context (as the bottom-up traversal walks the expressions to rewrite them with their final types) and used to find the appropriate conversion to call. The same mechanism is used to select the appropriate overload when an expression refers directly to an overloaded function. Additionally, when comparing two solutions to the same constraint system, overload sets present in both solutions can be found by comparing the locators for each of the overload choices made in each solution. Naturally, all of these operations require locators to be unique, which occurs in the constraint system itself.
Locators provide the derivation of location information that follows
the path of the solver, and can be used to query and recover the
important decisions made by the solver. However, the locators
determined by the solver may not directly refer to the most specific
expression for the purposes of identifying the corresponding source
location. For example, the failed constraint "Int conforms to
ExpressibleByFloatLiteral" can most specifically by centered on the
floating-point literal 10.5, but its locator is::
function application -> apply argument -> tuple element #0
The process of locator simplification maps a locator to its most
specific expression. Essentially, it starts at the anchor of the
locator (in this case, the application f(10.5, x)) and then walks
the path, matching derivation steps to subexpressions. The "function
application" derivation step extracts the argument ((10.5, x)). Then, the "tuple element #0" derivation extracts the tuple
element 0 subexpression, 10.5, at which point we have traversed
the entire path and now have the most specific expression for
source-location purposes.
Simplification does not always exhaust the complete path. For example,
consider a slight modification to our example, so that the argument to
f is provided by another call, we get a different result
entirely::
func f(_ i : Int, s : String) { } func g() -> (f : Float, x : X) { }
f(g())
Here, the failing constraint is Float <c Int, with the same
locator::
function application -> apply argument -> tuple element #0
When we simplify this locator, we start with f(g()). The "apply
argument" derivation step takes us to the argument expression
g(). Here, however, there is no subexpression for the first tuple
element of g(), because it's simple part of the tuple returned
from g. At this point, simplification ceases, and creates the
simplified locator::
function application of g -> tuple element #0
The performance of the type checker is dependent on a number of factors, but the chief concerns are the size of the solution space (which is exponential in the worst case) and the effectiveness of the solver in exploring that solution space. This section describes some of the techniques used to improve solver performance, many of which can doubtless be improved.
The constraint graph describes the relationships among type variables in the constraint system. Each vertex in the constraint graph corresponds to a single type variable. The edges of the graph correspond to constraints in the constraint system, relating sets of type variables together. Technically, this makes the constraint graph a multigraph, although the internal representation is more akin to a graph with multiple kinds of edges: each vertex (node) tracks the set of constraints that mention the given type variable as well as the set of type variables that are adjacent to this type variable. A vertex also includes information about the equivalence class corresponding to a given type variable (when type variables have been merged) or the binding of a type variable to a specific type.
The constraint graph is critical to a number of solver optimizations. For example, it is used to compute the connected components within the constraint graph, so that each connected component can be solved independently. The partial results from all of the connected components are then combined into a complete solution. Additionally, the constraint graph is used to direct simplification, described below.
When the solver has attempted a type variable binding, that binding often leads to additional simplifications in the constraint system. The solver will query the constraint graph to determine which constraints mention the type variable and will place those constraints onto the simplification worklist. If those constraints can be simplified further, it may lead to additional type variable bindings, which in turn adds more constraints to the worklist. Once the worklist is exhausted, simplification has completed. The use of the worklist eliminates the need to reprocess constraints that could not have changed because the type variables they mention have not changed.
The solver proceeds through the solution space in a depth-first manner. Whenever the solver is about to make a guess---such as a speculative type variable binding or the selection of a term from a disjunction---it introduces a new solver scope to capture the results of that assumption. Subsequent solver scopes are nested as the solver builds up a set of assumptions, eventually leading to either a solution or an error. When a solution is found, the stack of solver scopes contains all of the assumptions needed to produce that solution, and is saved in a separate solution data structure.
The solver scopes themselves are designed to be fairly cheap to create and destroy. To support this, all of the major data structures used by the constraint solver have reversible operations, allowing the solver to easily backtrack. For example, the addition of a constraint to the constraint graph can be reversed by removing that same constraint. The constraint graph tracks all such additions in a stack: pushing a new solver scope stores a marker to the current top of the stack, and popping that solver scope reverses all of the operations on that stack until it hits the marker.
As the solver evaluates potential solutions, it keeps track of the score of the current solution and of the best complete solution found thus far. If the score of the current solution is ever greater than that of the best complete solution, it abandons the current solution and backtracks to continue its search.
The solver makes some attempt at evaluating cheaper solutions before more expensive solutions. For example, it will prefer to try normal conversions before user-defined conversions, prefer the "default" literal types over other literal types, and prefer cheaper conversions to more expensive conversions. However, some of the rules are fairly ad hoc, and could benefit from more study.
Each constraint system introduces its own memory allocation arena,
making allocations cheap and deallocation essentially free. The
allocation arena extends all the way into the AST context, so that
types composed of type variables (e.g., T0 -> T1) will be
allocated within the constraint system's arena rather than the
permanent arena. Most data structures involved in constraint solving
use this same arena.
The diagnostics produced by the type checker are currently terrible. We plan to do something about this, eventually. We also believe that we can implement some heroics, such as spell-checking that takes into account the surrounding expression to only provide well-typed suggestions.
.. [#] It is possible that both overloads will result in a solution,
in which case the solutions will be ranked based on the rules
discussed in the section Comparing Solutions_.
.. [#] As of the time of this writing, the type rules of Swift have
not specifically been documented outside of the source code. The
constraints-based type checker contains a function matchTypes
that documents and implements each of these rules. A future revision
of this document will provide a more readily-accessible version.
.. [#] More accurately, as of this writing, "will compute". The solver doesn't current compute meets and joins properly. Rather, it arbitrarily picks one of the constraints "below" to start with.
.. [#] Again, as of this writing, the solver doesn't actually compute meets and joins, so the solver continues until it runs out of supertypes to enumerate.