昨日・今日と、「全称型／存在型で困惑した」という話を書きました。
なんとなく情勢は見えてきたので、いったんまとめをしておきます。それと、存在型の一部の用法を解釈するには、Models-as-Types という立場をとるのが良さそうなので、Models-as-Types の説明もします。$`\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
%`$
内容：
全称型／存在型の2つの類型
色々な解釈・定義があっても、人が「全称型／存在型」という言葉を使いたくなる対象物や構造にはパターンがあるようです。僕が見た限りにおいてですが、そのパターンは二種類あるようです。
- 随伴トリプルで説明できる場合
- 指標のモデルとして説明できる場合
随伴トリプルについては、「多相関数を表す全称記号がしゃくに障るワケ」で説明しています。指標のモデルについては、事例を使った短い説明が「全称型？ 存在型？ ‥‥？？ // 指標とモデル」にあります。
上記の2つの類型〈パターン〉は、多くの資料を漁って抽出したわけではなくて、とても少数の資料から判断したものです。なので、他のパターンが抜けている可能性はあります。少数の資料とは以下です。
- Haskell/存在量化された型
Haskellに関する記事なので「Haskell記事」として参照します。 - Existential types in Rust
Rustに関する記事なので「Rust記事」として参照します。 - An Introduction to Existential Types
MLに関する記事ではないのですが、ML風擬似コードで書かれているので「ML記事」として参照します。 - Existential any in Swift explained with code examples
Swiftに関する記事なので「Swift記事」として参照します。
随伴トリプルで説明できる場合
$`P`$ を変数 $`x`$ を含む（かも知れない）論理式（値が真偽値である記号的表現）だとして、これを全称限量〈universal quantification〉、存在限量〈existential quantification〉できます。
- 全称限量： $`\forall x. P`$
- 存在限量： $`\exists x. P`$
限量された〈quantified〉論理式は、変数 $`x`$ の値に関わらずに全体として単一の真偽値を表します。
記号 $`\forall, \exists`$ は、論理式（が表現する述語）を、単一の真偽値へと変換するオペレータだと考えることができます。もうひとつのオペレータ $`\Delta`$ とトリプル〈トリオ〉を作ると、三者は密接な関係を持ちます。その関係性を次のような記法で表し、随伴トリプル〈adjoint triple〉と呼びます。
$`\quad \exists \dashv \Delta \dashv \forall`$
依存型理論においても随伴トリプルが現れます。$`\mathscr{E}`$ を型変数 $`\alpha`$ を含む（かも知れない）型項（値が型である記号的表現）だとして、これをパイ限量〈Pi quantification〉、シグマ限量〈Sigma quantification〉できます。
- パイ限量： $`\Pi\, \alpha. \mathscr{E}`$
- シグマ限量： $`\Sigma\, \alpha. \mathscr{E}`$
限量された〈quantified〉型項は、変数 $`\alpha`$ の値に関わらずに全体としての単一の型を表します。
記号 $`\Pi, \Sigma`$ は、型項（が表現する型構成子）を、単一の型へと変換するオペレータだと考えることができます。もうひとつのオペレータ $`\Delta`$ とトリプル〈トリオ〉を作ると、それは随伴トリプルになります。
$`\quad \Sigma \dashv \Delta \dashv \Pi`$
より詳細は次の記事を読んでください。
Haskell記事に出てきた、「全称型＝共通部分、存在型＝合併」という解釈も随伴トリプルによる解釈が可能です。集合族（パラメータを持つ型）の共通部分を作ること、合併を作ることを一種の限量〈quantification | 量化〉だとみなして、キャップ限量／カップ限量と言うことにして、限量子っぽい書き方を使うとします。
$`\mathscr{E}`$ を型変数 $`\alpha`$ を含む（かも知れない）型項（値が型である記号的表現）だとして、これをキャップ限量〈Cap quantification〉、カップ限量〈Cup quantification〉できます。
- キャップ限量： $`\bigcap\, \alpha. \mathscr{E}`$
- カップ限量： $`\bigcup\, \alpha. \mathscr{E}`$
限量された〈quantified〉型項は、変数 $`\alpha`$ の値に関わらずに全体としての単一の型を表します。
記号 $`\bigcap, \bigcup`$ は、型項（が表現する型構成子）を、単一の型へと変換するオペレータだと考えることができます。もうひとつのオペレータ $`\Delta`$ とトリプル〈トリオ〉を作ると、それは随伴トリプルになります。
$`\quad \bigcup \dashv \Delta \dashv \bigcap`$
以上、類似の構造を3つ挙げたわけですが、背後に随伴トリプルがあると、人はその類似性から全称記号／存在記号を使いたくなる、という習性があるのでしょう。しかし僕は、全称記号／存在記号の流用には反対です。なんか似てるけど実は違うものがゴッチャになる事態は、とてもタチが悪いからです。安易な記号の流用は、悪い事態を誘発します。
指標のモデルとして説明できる場合
ML記事から、自然数型の定義を引用します。
type natNums = exists t. { zero: t, succ: t -> t }
Swift記事から、existential any を使った変数宣言・初期化を引用します。キーワードは any だけど存在型と呼ばれています。
protocol Content { var id: UUID { get } var url: URL { get } } struct ImageContent: Content { let id = UUID() let url: URL } let content: any Content = ImageContent(...)
Rust記事には実例がないのですが、存在型を概念的に記述する記法が紹介されています。
(∃ T. T: Trait)
この記法の意味は：
- some type
Tsuch thatTimplements the traitTrait.
いずれも指標（プログラミング言語により、インターフェイス、型クラス、プロトコル、トレイト、コンセプトなど、呼び名は色々）が出てきています。
プログラミング言語に中立な形で自然数とContentの指標を書いておきます。必要なら、「全称型？ 存在型？ ‥‥？？ // 指標とモデル」を見返してください。
signature NatNums {
sort T
operation zero : 1 → T
operation succ : T → T
}
signature Content {
sort C
operation id : C → UUID
operation url : C → URL
}指標のモデル（実装、型インスタンス）を「型」とみなす立場を Models-as-Types と呼ぶことにします。Models-as-Types の立場では、指標は型ではありません。指標は、型の集まりを規定する仕様・約束事です。
$`\mathscr{X}`$ を指標（指標そのものでも、指標の名前でもよい）として、Rust記事と類似の次の記法を使います。
$`\quad \exists \gamma. \mathscr{X}`$
ここで、$`\gamma`$ は変数ではなくて、指標に出現するフィールド名〈構成素名 | 構成素ラベル〉です。指標のフィールド名は、例を挙げればすぐわかるでしょう。
- 指標 NatNums のフィールド名： T, zero, succ
- 指標 Content のフィールド名： C, id, url
ML記事の存在型の例と、Swift記事の存在型の例は、Rust記事風の記法で次のように書けます。
∃T. NatNums∃C. Content
'∃'に対応するキーワードは some だとすると：
some T. NatNumssome C. Content
ところが、ML記事の存在型の例とSwift記事の存在型の例では重大な違いがあります。
- ML記事： 指標 NatNums のモデルとして、我々がよく知っているアノ自然数型（$`{\bf N}`$）を定義したい。
- Swift記事： 指標 Content のモデルのひとつであることを指定したい。そのモデルが何であるかはどうでもいい。
目的が違うのに同じ記号／キーワードを使うのはダメです。ML記事の存在型のほうはキーワード ini とします。
ini T. NatNums： 指標 NatNums のモデルのなかで特定のもの。some C. Content： 指標 Content のモデルのなかの任意のひとつ。
キーワード some, ini について、次節でもう少し説明します。
始モデルと任意のモデル
$`\mathscr{X}`$ を指標として、そのモデルの集まりを $`\mrm{Model}(\mathscr{X})`$ とします。$`\mrm{Model}(\mathscr{X})`$ は単なる集まりではなくて圏に仕立てることができます。$`\cat{M} := \mrm{Model}(\mathscr{X})`$ とすると：
- $`\cat{M}`$ は圏である。
- 圏 $`\cat{M}`$ の対象は、指標 $`\mathscr{X}`$ のモデルである。
- 圏 $`\cat{M}`$ の射は、指標 $`\mathscr{X}`$ のモデルのあいだの準同型写像である。
圏のなかの特別な対象として始対象〈initial object〉があります。始対象があっても1個とは限りません。しかし、始対象がたくさんあっても“事実上1個”なので、the initial object と言っていいでしょう。
圏 $`\cat{M}`$ は、指標 $`\mathscr{X}`$ のモデルの圏だったので、その始対象は（指標 $`\mathscr{X}`$ の）始モデル〈initial model〉と呼びます。前節のキーワード ini は initial model に由来します。
モデルは単なる集合とは限らず、複数のフィールドを持つでしょう。例えば、NutNums のモデルは T, zero, succ の3つのフィールドを持ちます。特に、フィールド T の値を取り出すとそれは集合になります。
以上の準備のもとで、ini T. NatNums の意味は次のように書けます。
the T of the initial model of NatNums
the initial model of NatNums のところで、圏 $`\mrm{Model}(\text{NatNums})`$ の始対象を取り出しています。the T of のところは、始モデルのフィールド T の値（台集合）を取り出しています。したがって、次の型定義で、我々がよく知っているアノ自然数の集合 $`{\bf N}`$ を定義できます。
type natNums := ini T. NatNums
指標 NatNums をインライン〈その場〉で書くなる：
type natNums := ini T. signature {
sort T
operation zero : 1 → T
operation succ : T → T
}構造としての始モデルには、特定要素 zero とサクセッサ演算 succ が備わっているので、集合としての型 nutNums の要素に succ （の実装）を適用することができます。
Swift記事の some C. Content は、特定のモデルを指すわけではなくて、なんだかわからない“とあるモデル”を意味します。次のように書けるでしょう。
the C of some model of Content
なんだかわからない型を使った変数宣言（初期化はしてない）は次のように書けます。
let content: some C. Content
実際の型（構造や集合）が分からなくても、指標 Content のモデル／モデルの台集合であることは保証されているので、フィールド（の実装） id, url を使えます。
多くの場合、指標のなかで台集合を示すフィールドが1個だけなので、明示的なフィールド名を付けずに“無名のデフォルト・フィールド”のように扱います。そうすると、フィールド名 T, C は省略できて、次のように書けます。
type natNums := ini NatNums
let content: some Content
無名のデフォルト・フィールドにより、Models-as-Types と Sets-as-Types を暗黙に行ったり来たりしています。
ここまで説明したことが、Models-as-Type に基づく存在型です。しかし、もはや論理の存在限量子とはかけ離れた話です。それにも関わらず、ML記事ではキーワード exists を使っており、Swift記事では、Swift 特有の事情（「全称型／存在型 補遺」参照）から some が使えず any でした
用語や記法は、ときに極めて不適切で、人をたぶらかすことがあります。だから僕は、「全称／存在」という言葉や「∀／∃」という記号をやたらに流用することに反対です。
関連記事：
