先日「ジェネリクス勉強会」なるものが開催されていたようで地方エンジニア勢の自分にとってには羨ましい限りだったのですが、ニコニコ動画で一部の発表をみたりTwitterのハッシュタグを眺めていると**「存在型」**が紹介されていたみたいで、自分のTwitterの観測範囲のSwiftエンジニアの間でもちょっと盛り上がっているように見えました。
この記事では、型システム入門 −プログラミング言語と型の理論− (以下、TaPL)を片手に存在型の理論をSwiftでのコードに結びつけて説明してみようと思います！
TaPLではSystem Fに存在型を加えたものが説明されていますが、この記事ではSwiftでの雰囲気を掴んでもらえるようにするため、一部Swiftっぽい型の表記を使って説明します。
また自分自身も「TaPLを頑張って読んでみようとしている」くらいのレベル感なので、もし間違いや適切でない記述があったらコメントや編集リクエストで指摘してもらえればと思います。。。
Swiftにおける存在型(Existential Type)とは？
存在型がどんなものなのかの説明は一旦後回しにして、実際のSwiftでは何が存在型にあたるのかを先に覗いてみます。
SwiftではProtocol型の値(の型)が「存在型」になります。
protocol Animal { }
// animalは存在型を持つ。
let animal: Animal = ...
このことはdocs/Generics.rstにも書かれています。
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.
普段Swiftを使っているエンジニアの方でも、これを「存在型」だと意識して使っている方は少ないのではないかなぁと思っています。
(少なくとも自分はそんなこと全然考えていませんでした。。)
型システムにおける存在型とは？
TaPLでは、存在型は{ ∃X, T } と表記されています。
馴染みのない方もいるかもしれないので一応先に$\exists$ ← この記号についてちょっとだけ説明します。
$\exists$の記号は存在量化子と呼ばれるもので、「ある〜が存在して」「ある〜について」とか読みます。
似たような記号で「すべての〜」「任意の〜」を表す全称量化子$\forall$がありますね！
X, T はそれぞれ型を表しています。
つまり { ∃X, T } は「ある型X」と「Xを使った型」のペアを表しています。
{ ある型X, なにかXを使った型 }
たとえば、
-
{ ∃X, X -> String }- 「ある型Xについて、
X -> Stringとなる型」を表す存在型
- 「ある型Xについて、
-
{ ∃X, (X, Int) }- 「ある型Xについて、
(X, Int)(タプル)となる型」を表す存在型
- 「ある型Xについて、
みたいなイメージです。1
ではこの型の値についてはどうなるでしょう？
TaPLでは、存在型の値は { *S, t } as { ∃X, T } と表記されています。
-
Sは 「ある型X」の具体的な型- 隠蔽表現型とか証人型(witness type) 2とか呼ばれます
-
tはT中のXをSに置き換えた型をもつ項です。
言葉だけだと分かり辛いと思うので例をあげます。
上で挙げた存在型 { ∃X, (X, Int) } の具体的な値の例を挙げると
{ *Bool, (false, 1) } as { ∃X, (X, Int) }{ *Bool, (true, 1000 + 200) } as { ∃X, (X, Int) }{ *Int, (1, 2) } as { ∃X, (X, Int) }{ *String, ("hello", 123) } as { ∃X, (X, Int) }{ *User, (user, 123) } as { ∃X, (X, Int) }
たとえば一番上の例では、Xが Boolで、(Bool, Int) 型の値として、(false, 1)を持つみたいな感じです。
*簡単に言えば、{ S, t }は具体的な型と項のペアです。
ちなみにas { ∃X, (X, Int) } をつけているのは、そうしないとどんな存在型なのかわからなくなるためです。
たとえば { *Int, (1, 2) } だけだと { ∃X, (X, Int) } 型なのか { ∃X, (X, X) } 型なのか区別が付きません。
(false, 1) とか ("hello", 123) とか全然違う型を持つものが、一つの { ∃X, (X, Int) } という型にまとめられるという点も面白いですね！ 3
以下では、この書き方を使ってSwiftにおける存在型について考えてみます。
SwiftでのProtocol型の値を、存在型を持つ値として見てみる
では、またSwiftに戻ってさっき上でちょこっと書いた「Protocol型の値(の型)が存在型になる」という話を、改めていま説明した記法を使って説明してみたいと思います。
例えばこんなAnimal protocolと、それを実装した Dog や Cat があるとします。
protocol Animal { }
struct Dog: Animal { }
struct Cat: Animal { }
もちろん、それらはAnimal型の変数に格納できます。
let animal1: Animal = Dog()
let animal2: Animal = Cat()
SwiftのコードにおけるAnimal型の値には実際には具体的な型が存在していて、それはDogだったりCatだったりするわけです。
つまり存在型だということを意識して、先程の記法を使ってみると
let dog = Dog()
// Animal型は、 { ∃X where X: Animal, X } みたいなイメージ
// 値は { *Dog, dog } as { ∃X where X: Animal, X }
let animal: Animal = dog
のような感じに書けるのかなと思います。
また、 Any についても(Swift3ではprotocolではありませんが)、同様に存在型として考えられそうです。
// { ∃X, X } という存在型
let any: Any = ...
AppleのこのドキュメントではAnyObjectやAnyClassについても存在型として紹介されていますね！
関数の引数の場合を例に、全称型(Generics)と見比べてみる
Animalprotocolに加えて HasName protocolを用意してみます。
protocol Animal { }
protocol HasName {
var name: String { get }
}
struct Dog: Animal, HasName {
let name: String
}
このとき、Animal と HasName の両方に準拠する型の値を受け取って、名前をprintする関数はどう書けるでしょうか？
2パターン考えられます。
// Generics(全称型)を使う場合
func printAnimalName1<T: Animal & HasName>(animal: T) {
print(animal.name)
}
// protocol型の値、つまり存在型を使う場合
func printAnimalName2(animal: Animal & HasName) {
print(animal.name)
}
もちろん両方きちんと動きますし、両方コンパイルも通ります。
ですが、実行時キャストと組み合わせると、使うときに問題が起こります。
// DogはAnimalにもHasNameにも準拠している
let unknownData: Any = Dog(name: "pochi")
if let namedAnimal = unknownData as? Animal & HasName {
// Genericsの方はエラーになる
// printAnimalName1(animal: namedAnimal)
// こっちはOK
printAnimalName2(animal: namedAnimal)
}
これも存在型という視点で考えてみると、namedAnimal は存在型を持っていることがわかります。
// namedAnimalは { ∃X where X: Animal & HasName, X } こんな型
if let namedAnimal = unknownData as? Animal & HasName {
それぞれの関数も全称型・存在型視点で型をみてみると、printAnimalName1がだめで2が使える理由がみえてきますね！！
// TaPLの表記っぽく書くと、
// (∀X where X: Animal & HasName). X
func printAnimalName1<T: Animal & HasName>(animal: T)
// { ∃X where X: Animal & HasName, X -> Void }
func printAnimalName2(animal: Animal & HasName)
protocolにおける Self について存在型視点でみてみる
存在型視点でprotocolのSelfについて考察してみたいと思います。
protocol SomeProtocol {
var value: Self { get }
}
Swift3の時点では Self や associatedtype をもつprotocol型の変数を作ることはできませんが、Generics Manifestoの存在型のところ には今後の作れるようになるみたいなことが書いてあるので、Selfを持つprotocol型の変数を作れるようになったときの妄想をしてみます。
let some: SomeProtocol = ... //作れるとする
そのとき、Selfが使われている some.value の型はどうなるでしょうか？？
some.value // どんな型？
まず、some自体は存在型の値になるので、こんな感じで考えられます。
// { ∃X where X: SomeProtocol, X } みたいな存在型
let some: SomeProtocol = ...
するとSelfを持つ値の型は X を使って表せます。
つまりSelf は存在型 { ∃X, T } のT を使うための仕組みだったんですね！！
some.value // X型になる。具体的な型Sは実行時に決まる。
(逆に考えるとsome.valueのように実行時まで決まらない型を静的に型チェックするとかいうことになってしまう可能性があるからSelfをもつprotocl型の変数は作れない、ということなのでしょうかね。。。)
存在型の除去構文とEquatableの例
さて、また少しTaPLから理論の話を持ってきます。
存在型の値は、「具体的な型と項のペア」でした。
{ *S, t } as { ∃X, T }
TaPLの存在型の章では、それぞれを取り出して使う(除去する、Openする)構文が用意されています。
// p1は存在型を持つ項
p1: { ∃X, T }
// let で存在型から「ある型」や「T型の項」を取り出す
// もちろん具体的にどんな型であるかはわからない。
let { X, x } = p1 in (xやXを使った計算)
// もしくはこういう構文も一般的に使われる(と書いてある)
open p1 as { X, x } in (xやXを使った計算)
現在のSwiftではそれを扱うための構文はありませんが、Generics ManifestoにOpening existentials として紹介されています。
Equatableを例に、現在の問題点と、それを解決するためにまさに↑のopen~asに近い構文が考えられています。
(詳しくは読んでみてみてください)
if let storedInE1 = e1 openas T {
if let storedInE2 = e2 as? T {
if storedInE1 == storedInE2 { ... }
}
}
associatedtype を存在型視点からみてみる
ここまでくると associatedtypeを持っている場合も気になるので、考えてみましょう。
まず、associatedtype自体が「ある型(associatedtype)が存在して〜」みたいに存在型の∃X の部分の役割を果たしているように考えられます。
// ある型Yが存在して〜
protocol P {
associatedtype Y
}
つまり、∃がついた型が増えただけですね！！
もちろん現在のSwiftではassociatedtypeを持つprotocol型の変数は作れませんが、作れるようになったときの妄想をしてP型の変数を作ってみて型を考えると、たぶんこんな感じになるのかなと思います。(自信はあまりないです...)
// ※ コメントを受けて修正をしました。ありがとうございます！
// { ∃X where X: P, { ∃ Y, X.Y } }
let p: P = ...
Generalized existentialsについて
Generics ManifestoにはGeneralized existentialsとしてこんな構文が紹介されています。
let strings: Any<Sequence where .Iterator.Element == String> = ["a", "b", "c"]
どんなものかはみればなんとなくわかりそうな気がするので、詳細に知りたい方はリンク先を読んでみてください。
Sequenceは要はassociatedTypeを持つprotocolなので、いままではAnySequenceみたいな Type Erasureと呼ばれるワークアラウンドを使わないと変数が作れなかったのですが、この構文によってAnySequence的なものを作らずに済みます。
また、一つ前の例の通り、もしSequence型の変数が作れたとすると、 { ∃X where X: P, { ∃ Y, X.Y } } みたいになるのでした。
では Any<Sequence where .Iterator.Element == String> はどうでしょう？
{ ∃X where X: Sequence where X.Iterator.Element == String, X }
まぁそのままですが、associatedtype によって導入された存在量化されたYを取り除くための構文という感じでしょうか！
おわりに
TaPLでの説明を参考にして、存在型の値について、{ *S, t } as { ∃X, T }のように、「型と項のペア」であるという考え方を元に、Swiftにおける存在型をそれっぽく説明してみました。
普段存在型を意識して書くことはないかとは思いますが、未来のSwiftでは Opening existentials や Generalized existentials のような存在型のための構文が入る可能性があるので、覚えておくとあとでいいことあるかもしれません！