Swiftでprotocol型の値がそのprotocol自身にconformしていない理由

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

```swift
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つの暗黙的なルールがあります。

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

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

## 型としてのprotocolと存在型
まず第一に、**protocolそのものは型ではありません**。例えば上の例であれば`Animal`という型は存在しません。
これについてはkoherさんの [インタフェースと型クラス、どちらでもできること・どちらかでしかできないこと](https://qiita.com/koher/items/ee31222b7f9b0ead3de7)という記事が詳しいです。

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

```swift
let animal: Animal = ...
```

[docs/Generics.rst](https://github.com/apple/swift/blob/master/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になってしまったみたいなイメージをしてもらえればわかりやすいかなと思います。

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

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

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

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

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

<img width="600" alt="スクリーンショット 2017-12-15 16.37.03.png" src="https://qiita-image-store.s3.amazonaws.com/0/14846/04159994-945c-1055-6844-0e2bcf8f7930.png">
(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
```

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

```swift
// サブタイプ関係があるので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`というオプションで型推論の挙動を見てみます。

```swift: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
```

<img width="954" alt="スクリーンショット 2017-12-16 23.12.36.png" src="https://qiita-image-store.s3.amazonaws.com/0/14846/548ca952-9a00-a398-9443-c904efbf5f3d.png">


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

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

```cpp: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);
// (略)
}
```

```cpp: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](https://github.com/apple/swift/blob/master/docs/GenericsManifesto.md#generalized-existentials)がうまいこと導入されればこのパターン自体不要になります。
(このワークアラウンドがもたらした弊害については後述します)

## 存在型に対するメソッド呼び出しのセマンティクス
閑話休題、3つ目のルールについて確認しましょう。
すでに確認したとおり、`Animal`型の変数は以下のような存在型を表すのでした。

```
{ ∃X where X: Animal, X }
```

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

```swift
animal.bark() // OK
```

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

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

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

### ルール3. 

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

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

```swift: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`を追加しています。

```cpp: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` が挿入されていることが確認できます。


<img width="459" alt="スクリーンショット 2017-12-16 23.04.24.png" src="https://qiita-image-store.s3.amazonaws.com/0/14846/b0fe121b-99d9-b90e-f180-0202fbf25b8c.png">


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

## Opening existentialについて

上の例で`openas`という仮の構文を導入しましたが、実は[docs/GenericsManifesto.rst](https://github.com/apple/swift/blob/master/docs/GenericsManifesto.md#opening-existentials)に”Opening existential”という項目があり、実際に`openas`という構文の導入が検討されています。

```swift
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`に適用できるようになります。

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

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

## Generalized existentialとTypeErasureパターン
[Generalized existentials](https://github.com/apple/swift/blob/master/docs/GenericsManifesto.md#generalized-existentials)によれば、`Any<Protocol>`のような構文が導入され、より一般的に存在型が扱えるようになるようです。
これによって既存の`AnySequence`などのワークアラウンドは一掃できます。

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

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

<img width="923" alt="スクリーンショット 2017-12-16 23.40.11.png" src="https://qiita-image-store.s3.amazonaws.com/0/14846/900d3b97-9b3f-ace3-bb94-bbe8b8a88751.png">


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

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

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

<img width="881" alt="スクリーンショット 2017-12-16 23.41.57.png" src="https://qiita-image-store.s3.amazonaws.com/0/14846/3b3ec0dc-02fd-687a-7ef9-5b306fa3d6df.png">


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

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

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


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

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

+ [Discordが良い感じなので、ios-developers-japan サーバー を作ってみました( ´･‿･｀)](https://medium.com/swift-column/discord-ios-20d586e373c0)


## 参考文献
+ 型システム入門 プログラミング言語と型の理論
	+ 第24章 「存在型」
	+ 第15章 15.6「部分型付けに対する型強制意味論」

+ 存在型に関するサブタイピング規則について
	+ [CSSimplify.cpp](https://github.com/apple/swift/blob/fa63e6a5a0467bd2a7cdd30674ccf10163d84474/lib/Sema/CSSimplify.cpp#L4338-L4344)内のコメントにサブタイピング規則が書いてあります。
	+ 見つけたときは「マジかよ...」と思って`TypeChecker::isSubtypeOf`に対して[自分でユニットテストを書いて確認してみました](https://github.com/ukitaka/swift/blob/1d11896a28e70c3f494e3540b23b284d415853e3/unittests/Sema/SubTypeTests.cpp#L40-L56)が、本当でした。