全称型？存在型？ ‥‥？？ - 檜山正幸のキマイラ飼育記 (はてなBlog)

「多相関数を表す全称記号がしゃくに障るワケ」において、多相関数や依存型を表すときに使う全称記号を話題にしました。僕は全称記号反対派ですが、実際には全称記号が使われています。

さてところで、「全称限量された型〈universally-quantified type〉」、「存在限量された型〈existentially-quantified types〉」という言葉を見かけました。型の話に論理の限量子を持ち出すのはやめて欲しいと思っているので、イヤな感じがしました。

とりあえず検索して、解説（らしきもの）を斜め読みしたのですが、現時点では困惑しております*1。$`\newcommand{\mrm}[1]{\mathrm{#1} }`$

内容：

全称型と存在型（表面的な定義）
集合族の共通部分と合併（なの？）
存在型は指標に関わる？
指標とモデル
存在型は指標のモデル？
結局

関連記事：

全称型と存在型（表面的な定義）

とりあえず、全称型／存在型の表面的な意味（ほとんど無意味だが）を説明します。

$`\alpha`$ を型変数として、$`\alpha`$ を含む型項〈type term〉（型を表す記号的表現）を $`\mathscr{E}`$ とします。$`\mathscr{E}`$ の例は：

$`\alpha`$
$`[\alpha, \alpha]`$ （ブラケットは指数型〈関数型〉）
$`\alpha \times \alpha`$ （掛け算記号は直積型〈ペア型〉）
$`[\alpha\times \alpha, \alpha]`$ （二項演算の型）
$`[\alpha, [\alpha, \alpha] ]`$ （カリー化した二項演算の型）
$`[\alpha, \mrm{Bool}]`$ （述語の型）
$`[\mrm{List}(\alpha), \mrm{Int}]`$ （リストの長さ $`\mrm{length}`$ が所属する型）

「$`\alpha`$ を含む」と書きましたが、$`\mathscr{E}`$ に $`\alpha`$ が現れなくてもかまいません。例えば：

$`\mrm{Bool}`$
$`\mrm{Bool}\times \mrm{Bool}`$
$`[\mrm{Int}, \mrm{Bool}]`$
$`\mrm{List}(\mrm{Int})`$

型項 $`\mathscr{E}`$ を、全称限量子〈全称量化子〉により限量〈量化〉した形を全称限量された型〈universally-quantified type〉、あるいは短く全称型〈universal type〉と呼びます。

$`\quad \forall \alpha.\mathscr{E} \:\:(\text{universally-quantified type})
`$

同様に、型項 $`\mathscr{E}`$ を、存在限量子〈存在量化子〉により限量〈量化〉した形を存在限量された型〈existentially-quantified types〉、あるいは短く存在型〈existential typee〉と呼びます。

$`\quad \exists \alpha.\mathscr{E} \:\:(\text{existentially-quantified type})
`$

以上の定義は、書き方／書かれた形に名前を付けただけで、内容的には何も定義してないことに注意してください。全称限量子／存在限量子により書かれた形は、いったいナニモノを指しているのか？が問題です。

僕は、全称型／存在型について知らなかったので、以下に検索で引っかかった資料を引用して説明します。現時点では、色々と違った定義(?)があるので、「合意された内容的定義がないのかも知れない」という印象です。

集合族の共通部分と合併（なの？）

まずは以下の解説記事：

Haskell/存在量化された型（翻訳）
Haskell/Existentially quantified types （英語原文）

引用は、現時点（2022年10月末）での日本語版から引用します。まず、型とは何か？について：

型についての考え方として、その型の値の集合だと考えることができる。たとえば、Bool は集合 {True, False, ⊥} (ボトム ⊥ はいかなる型のメンバでもあることを思い出そう！)

基本的には Sets-as-Types の立場ですが、ボトムを入れているので OrderedSet-as-Types ですね。もっと精密化して Lattices-as-Types になるのかも知れません。型を順序集合とみなすことは、先日90歳をむかえられたデイナ・スコット〈Dana Scotto〉を開祖とする正統的解釈です。

そして、forall の説明：

forall はこれらの集合の共通集合を与える。たとえば、forall a. a はすべての型の共通部分であり、{⊥} のはずである。これは値(つまり要素)がボトムだけであるような型(つまり集合だ)である。...[snip]... ボトムはすべての型に共通する唯一の値だ。

次のことを主張しています。

$`\quad \forall \alpha. \mathscr{E} = \bigcap_\alpha \mathscr{E}`$

$`\mathscr{E}`$ は、$`\alpha`$ でインデックスされた集合（順序集合の台集合）族と考えます。特別な場合として：

$`\quad \forall \alpha. \alpha = \bigcap_\alpha \alpha = \{\bot\}`$

これは、パイ型を全称限量子で表す用法とは違いますね。例えば、多相な恒等関数はパイ型の要素として書けます。

$`\quad \mrm{id} \in \Pi\, \alpha. [\alpha, \alpha]`$

しかし、多相な恒等関数とみなせる要素は、集合族の共通部分のなかには存在しません。

$`\quad \mrm{id} \not\in \bigcap_\alpha [\alpha, \alpha]`$

記事「Haskell/存在量化された型」では、同じ論法で存在型〈存在量化された型〉を導入しています。

この 'exists' キーワード(これは Haskell には存在しない)は推測されるように型の和集合であり、そして [exists a. a] はすべての要素がどんな型も取れる(かつ異なる要素は同じ型である必要はない)リストの型なのである。

Haskellに exists というキーワードはないけども、もしあるならば、その意味は次のようだと：

$`\quad \exists \alpha. \mathscr{E} = \bigcup_\alpha \mathscr{E}`$

存在型は指標に関わる？

今度は Rust の存在型の（全称型も書いてある）記事を覗いてみます。

Existential types in Rust

全称型に関しては：

The type ∀ T. (T, T) is a universally-quantified type that takes a type argument T and produces a type of pairs of that type, (T, T). You can think of ∀ T. S as a function taking a type T and returning a type S.
型 ∀ T. (T, T) は全称限量された型である。これは、型引数 T を受け取って、その型のペア型 (T, T) を作る。∀ T. S は、型 T を渡すと型 S を返す関数だと考えるといいだろう。

この説明だと、全称記号 $`\forall`$ は、型に関するラムダ抽象記号の代用ですね。つまり、全称型は、型項 $`\mathscr{E}`$ で定義される型関数である、と。

$`\quad \forall \alpha.\mathscr{E} = \lambda\, \alpha. \mathscr{E}`$

Sets-as-Types の立場なら、型関数は集合族のことです。前節の解釈は、集合族の共通部分をとって全称型としたのですが、今回の全称型は集合族に何もしないで、集合族そのものが全称型だという解釈です。

存在型はどうでしょう：

∃ T. T: Trait is the logical notation for some type T such that T implements the trait Trait. For example, ∃ T. T: IntoIterator<Item = S> could be satisfied with the type Vec<S> or HashSet<S>, or so on.
∃ T. T: Trait は、トレイト Trait を実装しているとある型 T を示す論理的記法である。例えば ∃ T. T: IntoIterator<Item = S> は、型 Vec<S> や型 HashSet<S> によって（論理的条件が）満たされる

トレイトというのは、インターフェイス／指標のようなものですよね。となると、単なる集合というよりは構造が載った集合を型とみなし、構造の定義に指標を使うことが前提のようです。

指標とモデル

前節で「指標〈signature〉」という言葉を出したので、ごく手短に事例で説明しておきます。次は、スタックの指標です。

signature Stack {
  sort S
  sort V
  operation push : S×V → V
  operation pop : S → S
  operation top : S → V
}

S がスタック状態の型（ソートともいう）、V がスタックに積む値の型、push, pop, top はお馴染みの関数／メソッド（オペレーションともいう）です。この指標では、pop は状態遷移を引き起こすだけでトップの値を返しません。また、pop がエラー／例外を起こすことも無視しています。

スタックの指標の別な例は：

signature Stack2 {
  sort S
  sort V
  operation emp : 1 → S
  operation push : S×V → V
  operation pop : S → S×Option(V)
}

emp は空スタックを生成する初期化関数です。pop はトップの値も返しますが、トップの値がないときもあるので、Option（あるいは Maybe）をかぶせて未定義値も許します。

スタックに積む値の型 V を型パラメータにすると：

signature Stack3 <sort V>{
  sort S
  operation emp : 1 → S
  operation push : S×V → V
  operation pop : S → S×Option(V)
}

Stack3 <Int> は整数値を積むスタックの仕様／インターフェイスになります。

指標（仕様／インターフェイス）のモデル〈model〉とは、その仕様／インターフェイスを実現する実装のことです。ただし、プログラミング言語による実装というよりは概念的な実装です。例えば、指標 Stack のモデルは、次のモノから構成されます。

ソート記号 S に対する集合
ソート記号 V に対する集合
オペレーション記号 push に対する写像
オペレーション記号 pop に対する写像
オペレーション記号 top に対する写像

これらの集合・写像をひとまとめにした構造がモデルです。

存在型は指標のモデル？

次なる資料は：

An Introduction to Existential Types

上記の記事では、ML風の擬似コードで事例が書かれています。

全称型〈universal type〉に関しては、総称型〈generics〉と同義語の扱いです。型でパラメトライズされた型が全称型なので、「全称型は型関数」の立場です。

存在型の例として、自然数型〈natural numbers〉の定義が挙げられています。

type natNums = exists t. { zero: t, succ: t -> t }

波括弧内は指標ですよね。次のように書いても同じでしょう。

signature NatNums <sort T> {
  operation zero : 1 → T
  operation succ : T → T
}

指標のモデルを型とみなすことはよくあるのですが、それを存在記号（対応するキーワードは exists）で表すことは知りませんでした。

ここから圏論の言葉を使いますが、指標 $`S`$ があると、その指標のモデルの全体は自動的に圏になります。その圏を $`\mrm{Model}(S)`$ と書くことにしましょう。上の例なら、$`\mrm{Model}(\text{NatNums})`$ という圏ができます。この圏の対象は、なんらかの集合と、オペレーション記号 zero, succ に対する写像の組です。

今この文脈における存在型は、どうやら指標のモデル（モデルの圏の対象）のようです。しかし、モデルはひとつではない（圏 $`\mrm{Model}(\text{NatNums})`$ の対象はイッパイある）ので、どのモデルを意味するかハッキリしません。可能性としては：

すべてのモデル〈任意のモデル〉を意味している。
固有特定のひとつのモデルを意味している。

固有特定だとして、それはどんなモデルでしょう。圏の対象を特定するためによく使われる方法は、「始対象を選ぶ」というものです*2。この選び方を採用するなら：

モデルの圏の始対象を意味している。

うるさいことを言えば、始対象も一意には決まりませんが、同型を無視すれば一意なので「始対象は（もし在るなら）ひとつ在る」と言ってもいいでしょう。

記事 "An Introduction to Existential Types" の事例は、我々がよく知っている $`{\bf N}`$ を定義したいという動機から始まっているので、おそらく、存在限量子記号で「モデルの圏の始対象」を取り出しているのでしょう。

しかし、記事 "Existential types in Rust" では、some type T such that ... と書いているので、始対象を特定している感じはしません。ひょっとして、「固有特定のモデルだが、始対象とは限らず、超越的に選択された（神様が気まぐれで選択した）モデル」という意味かも知れません。

なお、記事 "An Introduction to Existential Types" には、前節の指標 Stack3 に対する存在型の例も載っています。ただし、スタック状態の型がスタックに積む値の型から構成できる、という前提です。

type stack = exists 'a t. { emp: 'a t, push: 'a t * 'a -> 'a t, pop: 'a t -> 'a t * 'a option }

結局

斜め読みした記事達では、意見の相違があるようです。

全称型とは集合族の共通部分であり、存在型とは集合族の合併である。
全称型とは型関数であり、存在型とは指標のモデルである。

指標のモデルだとしても、次のような可能性があります。

すべてのモデル〈任意のモデル〉を意味している。
始対象を意味している。
超越的に選択された特定のモデルを意味している。

冒頭で述べたように、単に「全称限量子を使う、存在限量子を使う」という書き方だけで言うなら、次の解釈もありそうです。

全称型とはパイ型であり、存在型とはシグマ型である。

結局、ナンダカワカリマセン！

続き：アハハハハ（ちからない笑い）：全称型／存在型

*1:型理論に関わる用語法は、むちゃくちゃなのが伝統なのかも知れません。「型理論ってば」参照。

*2:余代数意味論なら、終対象が選ばれます。