iOSのDiscordで定期的にあがる話題として「protocol型の値がそのprotocol自身にconformしていないのはなぜ？」というものがあります。
例えば以下のようなコードです。

protocol Animal {
	func bark()
}
struct Dog: Animal { 
	func bark() {
		print("わんわん")
	}
}

func f<A: Animal>(_ animal: A) { ... }

// これはOK
let dog: Dog = Dog()
f(dog)

// こっちはNG
// error: cannot invoke 'f' with an argument list of type '(Animal)'
let animal: Animal = Dog()
f(animal)

毎度話題に上がるたびに「で、なんでなんだっけ？」となってしまうので、備忘録を兼ねてQiitaに投稿しておきます！

「存在型というものの存在自体は聞いたことがあって、それがSwiftで使われていることもなんとなく知っている」くらいの方を想定して説明を行います。

Swiftの存在型をややこしくしている3つの暗黙的なルール

Swiftではprotocol型の値が存在型を持ち、基本的にはユーザにそれを意識させず直感的にプログラムが書けるような言語設計になっているのですが、それは多くの暗黙的な変換ルールによって支えられているため、時に上記の例のような混乱を生みがちです。

具体的には以下の3つの暗黙的なルールがあります。

型のポジションに現れるprotocol名Pは、{ ∃X where X: P, X } という存在型を表す。
T: P なTについて、T <: { ∃X where X: P, X } というサブタイピング規則が存在して、そのセマンティクスとして「存在型へのパッケージ化(erase)」という型強制がある。
存在型に対する .(ドット)によるメソッド呼び出し構文は「存在型をアンパッケージ化(open)してからメソッドを呼び出す」というセマンティクスを持つ。

この記事ではまずルール1の説明を通して「protocol型の値がそのprotocol自身にconformしていないのはなぜか？」を解説します。
そしてルール2, 3を元に「どう辻褄を合わせているのか？」について説明します。

型としてのprotocolと存在型

まず第一に、protocolそのものは型ではありません。例えば上の例であればAnimalという型は存在しません。
これについてはkoherさんのインタフェースと型クラス、どちらでもできること・どちらかでしかできないことという記事が詳しいです。

しかし実際にはprotocol名が型のポジションに出現しています。
どういうことでしょう？

let animal: Animal = ...

docs/Generics.rstによると、型のポジションに現れたprotocol名は存在型を表すことが確認できます。

In Swift, we consider protocols to be types. A value of protocol type has an existential type, meaning that we don't know the concrete type until run-time (and even then it varies), but we know that the type conforms to the given protocol.

TaPLの表記を借りると型のポジションに現れたAnimalは以下のような存在型を表します。

{ ∃X where X: Animal, X }

ルール1.

型のポジションに現れるprotocol名Pは、{ ∃X where X: P, X } という存在型を表す。

少しだけ意味を説明をすると存在型は{ ある型, その型を使った型 }というペアで表現されています。{ ∃X where X: Animal, X }を日本語で書いてみるとこんな感じでしょうか。

「あるAnimalプロトコルにconformした型Xが存在して、そのX」を表す型

「その型を使った型」がそのまま「X」になっているのでこの例だとちょっとわかりづらいですが、例えば一般的な存在型であればこんなことも可能です。

{ ∃X where X: Animal, (X, X) -> Bool }

「あるAnimalプロトコルにconformした型Xが存在して、そのペア(X, X)を受け取ってBoolを返す関数」を表す型

もちろんSwiftではそんなことはできませんが、「ある型」と「その型を使った型」のペアであるイメージが持ってもらえれば十分です！
「ペア」であるということからもわかる通り、Dogなどのシンプルな型とは全然違う型であることがイメージできるでしょうか？

{ ∃X where X: Animal, X }

Dogの場合はもちろんDog自身がAnimalプロトコルにconformしていますが、存在型の場合Animalにconformしているのは「ある型X」であり、{ ∃X where X: Animal, X }がAnimalプロトコルにconformしているわけではないのです。

Dog は is-a Animalですが、存在型ではhas-a Animalになってしまったみたいなイメージをしてもらえればわかりやすいかなと思います。

これがこの記事のタイトルに対するシンプルな答えではあるのですが、これだけではなんだかモヤモヤが残ります。
だって違う型なのであれば、そもそも以下のようなコードは成立しませんよね？？

// Dog と { ∃X where X: Animal, X } は
// 全然違う型なのに、なぜ代入できるの？
let animal: Animal = Dog()

// なぜメソッド呼び出しできるの？
// Animalプロトコルにconformしていないならメソッドもないはず。
// やっぱりAnimalプロトコルにconformしているのでは？
animal.bark()

ごもっともなツッコミです。
ここからは残りのルールを見つつこれがどう動いているのか、実際のコンパイラの動きも見ながら確認していきましょう。

存在型の「パッケージ化」「アンパッケージ化」

残りのルールの解説をする前に、TaPLを参考にしながら直接的に存在型を扱うための構文を通してSwiftが暗黙的に行なっている存在型の「パッケージ化」「アンパッケージ化」の概念を説明します。

(TaPLの24章から引用)

小難しい規則はおいておいて、注目して欲しいのは左上の「パッケージ化」「アンパッケージ化」の部分です。

パッケージ化 = 存在型のオブジェクトを作ること。eraseとも言う。
アンパッケージ化 = 存在型のオブジェクトをバラすこと。openとも言う。

ここで理解して欲しいことは「存在型を作ったりバラしたりする操作は本来は明示的に必要で、それらはパッケージ化・アンパッケージ化と呼ばれている」ということだけです。
しかし存在型を扱っているのにも関わらず、現在のSwiftにはこのような操作をするための構文は存在しません。
なぜならこれらの操作をコンパイラが勝手にやってくれているからです。

存在型に関するサブタイピングと型強制

まず存在型を作る「パッケージ化」について説明します。
上のTaPLの構文を使えば、Dog型のdogから存在型{ ∃X where X: Animal, X }のオブジェクトを作るためにはこんな操作が必要なはずです。

{ *Dog, dog } as { ∃X where X: Animal, X }

しかしそんな構文はどこにもありません。どういうことでしょう？

まずはじめに、実はSwiftは存在型について以下のようなサブタイプ関係があります。

T <: { ∃X where X: P, X } if T: P

このサブタイピング規則によって代入などの型チェックが通るわけです。

// サブタイプ関係があるのでOK
let animal: Animal = Dog()

しかし型チェックは通ったとしてもDog型と存在型としてのAnimalではメモリレイアウトは全然違いますし、パッケージ化の処理を挟み込まなければ成立しません。

実はSwiftの型システムはサブタイピングついて「coercion semantics(型強制意味論)」というものを採用しています。詳しくはTaPLの15章を読んでもらうとして、理解しておいて欲しいのは**「サブタイピングは実行時の型強制に置き換えられる」**ということです。

ルール2.

T: P なTについて、T <: { ∃X where X: P, X } というサブタイピング規則が存在して、そのセマンティクスとして「存在型へのパッケージ化(erase)」という型強制がある。

「型強制(coercion)」という言葉が出てきましたが、よく暗黙変換などと呼ばれているものの正体がこれです。
「Optional型への暗黙変換」などと呼んでいるものも正確にはA <: Optional<A>というサブタイピング規則に基づいた型強制です。

この型強制によりパッケージ化の処理が行われていたわけです。
実際にコンパイラの挙動を確認してみましょう！

まずは-debug-constraintsというオプションで型推論の挙動を見てみます。

sub.swift

protocol Animal { }
struct Dog: Animal { }

let animal: Animal = Dog()

% swift -frontend -typecheck -debug-constraints sub.swift

色々出力がでますが、見るべきポイントは以下の部分です。

Constraint restrictions:
  Dog to Animal is [existential]

Constraint restrictionsは推論時に使ったサブタイプ関係等を記録するもので、今回はexistentialと出ておりまさに上で紹介した規則が使われているのが確認できます。

型検査が終わったあとのAST(抽象構文木)の状態を出力してみます。

% swift -frontend -dump-ast sub.swift

erasure_exprが挿入されているのがわかるでしょうか？
これがまさに型強制によってパッケージ化が挿入されている様子です。

型強制をしている部分の実装を少し覗いてみると、推論時に記録したConstraint restrictionsを元に型強制が行われているのが確認できます。

CSApply.cpp

// 型強制(coercion)のためのエントリーポイント
Expr *ExprRewriter::coerceToType(Expr *expr, Type toType,
                                 ConstraintLocatorBuilder locator,
                                 Optional<Pattern*> typeFromPattern) {
// (略)
    case ConversionRestrictionKind::Existential:
    case ConversionRestrictionKind::MetatypeToExistentialMetatype:
      return coerceExistential(expr, toType, locator);
// (略)
}

CSApply.cpp

Expr *ExprRewriter::coerceExistential(Expr *expr, Type toType,
                                      ConstraintLocatorBuilder locator) {
  // (略)
  return cs.cacheType(new (ctx) ErasureExpr(expr, toType, conformances));
}

余談:「type-erasure」について

上で存在型へパッケージするという意味でerasure_exprが挿入されました。
また、Swiftにも公式ワークアラウンドとしてAnySequenceなどの「型消し(Type erasure)」パターンが使われています。
名前が共通していることからお察しの通り、これらは本質的には同じものを指しています。

存在型に関する文脈での「type erase」は「具体的な型を消して、存在型へパッケージ化する」ことを指します。このことから分かる通りtype-erasureは「存在型」のことです。

もちろんSwiftで使われているAnySequenceなどはあくまでも存在型の代用品です。Generalized existentialsがうまいこと導入されればこのパターン自体不要になります。
(このワークアラウンドがもたらした弊害については後述します)

存在型に対するメソッド呼び出しのセマンティクス

閑話休題、3つ目のルールについて確認しましょう。
すでに確認したとおり、Animal型の変数は以下のような存在型を表すのでした。

{ ∃X where X: Animal, X }

ルール1のときの説明によれば、この型はAnimalprotocolにconformしていないのでbark()メソッドを持たないはずです。
しかし実際にはメソッドが呼び出せてしまいます。どういうことでしょう？

animal.bark() // OK

実際にAnimalprotocolにconformしているのは存在量化されたXという型です。なんとかこのXを取り出せればメソッド呼び出しが行えそうです。

// 存在型 { ∃X where X: Animal, X } の
// XをAという名前で取り出すopenasという仮の構文。
// aはAという型を持つ。
let a = animal openas A
a.bark() // OK

このaやAを取り出す操作こそアンパッケージ化と呼ばれる操作で、Swiftコンパイラは存在型に対するメソッド呼び出し時にアンパッケージ化を自動で挿入します。

ルール3.

存在型に対する .(ドット)によるメソッド呼び出し構文は「存在型をアンパッケージ化(open)してからメソッドを呼び出す」というセマンティクスを持つ。

先程と同様にコンパイラの動きを確認してみます。

sub.swift

protocol Animal {
	func bark()
}

struct Dog: Animal {
	func bark() { print("わんわん") }
}

let animal: Animal = Dog()
animal.bark()

まず-debug-constraintsで型推論の挙動を見てみると「存在型に対してメソッド呼び出し」があった場合は、その旨がConstraintSystemのOpenedExistentialTypesに記録されていることがわかります。

% swift -frontend -typecheck -debug-constraints sub.swift

Opened existential types:
  locator@0x7fa4e78210a8 [UnresolvedDot@sub.swift:10:8 -> member] opens to Animal

これを元に、ExprRewriter::buildMemberRefでメソッド呼び出しに関するExpr書き換えが行われます。
最終的にExprRewriter::finishApplyで以下のようにDeclTypeCheckingSemantics::OpenExistentialの場合はOpenExistentialExprを追加しています。

CSApply.cpp

case DeclTypeCheckingSemantics::OpenExistential: {
  // (略)
  auto replacement = new (tc.Context)
    OpenExistentialExpr(existential, opaqueValue, callSubExpr,
                        resultTy);
  cs.setType(replacement, resultTy);
  return replacement;
}

-dump-astでASTを確認してみると確かにopen_existential_expr が挿入されていることが確認できます。

この「Openしてからメソッド呼び出し」ルールこそが「protocol型の値もそのprotocolにconformしている」と勘違いさせてしまう最大の原因かもしれないですね。

Opening existentialについて

上の例でopenasという仮の構文を導入しましたが、実はdocs/GenericsManifesto.rstに”Opening existential”という項目があり、実際にopenasという構文の導入が検討されています。

if let storedInE1 = e1 openas T {     // T is a the type of storedInE1, a copy of the value stored in e1
  if let storedInE2 = e2 as? T {      // is e2 also a T?
    if storedInE1 == storedInE2 { ... } // okay: storedInT1 and storedInE2 are both of type T, which we know is Equatable
  }
}

(openasは失敗しなさそうですが、なぜかif let になっています。。なんでだろう)

もしこの構文が入れば最初の例において、openasでアンパッケージ化することでfに適用できるようになります。

let animal: Animal = Dog()
f(animal) // NG 

let a = animal openas A
f(a) // OK

Generalized existentialとTypeErasureパターン

Generalized existentialsによれば、Any<Protocol>のような構文が導入され、より一般的に存在型が扱えるようになるようです。
これによって既存のAnySequenceなどのワークアラウンドは一掃できます。

typealias AnySequence<Element> = Any<Sequence where .Iterator.Element == Element>
let strings: AnySequence<String> = ["a", "b", "c"]

しかし、これまでのAnySequenceとの互換性に関しての問題点をkoherさんが指摘されていました。

要はいままでのAnySequenceは存在型に対するメソッド呼び出しの挙動(存在型に対してメソッドを直接呼び出せる)に合わせるためにAnySequence: Sequenceという定義になっていたため、T: Sequence に適用できてしまっていたのです。

しかしAnySequenceが本物の存在型で表される(Any<Sequence ... >によって定義される)ようになると、この記事で説明したようにAnySequenceはSequenceにconformしていないことになります。

どういう対応がされるのかはわかりませんが互換性を維持するのであれば関数の引数として渡す際にもアンパッケージ化が入り、T: Sequenceなところに適用できるような対応がなされるのではないかと(自分は)考えています。

ただ実現可能なのかは不明ですし、また暗黙的なルールが増えてしまうので、個人的には互換性を捨てるというのも手かなと思っています。

AnySequence: Sequenceという定義も、「protocol型の値もそのprotocolにconformしている」と勘違いさせてしまう原因の一つだったかなと思います。(もちろん仕方なかったのですが...)

まとめ

長くなってしまいましたが、protocol型の値がそのprotocol自身にconformしていない理由を、型システムの理論・Swiftコンパイラが裏で行なっていることもふまえて説明してみました。もっと詳しく知りたい方はぜひTaPLやSwiftコンパイラを読んでみてください。

構文に直接出てこない分、裏側で暗黙的に起こっている動きはOptional関連のそれよりも凶悪感はありますが、存在型というなんだか難しそうなものを直接的に扱わせないことによって文法的な複雑さを減らし、Swiftユーザに負担をかけないための良い言語設計ではあると思います。

iOSのDiscordではこんな言語のコアの話も頻繁にされていています、興味がある方はぜひjoinしてみてください！

Discordが良い感じなので、ios-developers-japan サーバーを作ってみました( ´･‿･｀)

参考文献

型システム入門プログラミング言語と型の理論
- 第24章「存在型」
- 第15章 15.6「部分型付けに対する型強制意味論」
存在型に関するサブタイピング規則について
- CSSimplify.cpp内のコメントにサブタイピング規則が書いてあります。
- 見つけたときは「マジかよ...」と思ってTypeChecker::isSubtypeOfに対して自分でユニットテストを書いて確認してみましたが、本当でした。