昨日「まとめ」もしたので、この話題も一段落ですが、僕が言いたいことは； 「全称／存在」という言葉、「∀／∃」という記号を、型理論のなかで使うのはやめたほうがいいよ、ってことです。何も得することがなくて、弊害があります。
「全称／存在」「∀／∃」を使わなくて済むように、この記事で代替案を述べます。$`\newcommand{\mrm}[1]{\mathrm{#1} }`$
内容：
パイ型、シグマ型、型関数
$`\alpha`$ を型変数として、$`\mathscr{E}`$ を型変数 $`\alpha`$ を含む（かも知れない）型項（値が型である記号的表現）だとします。パイ型は $`\Pi`$（または総積記号 $`\prod`$）を使って書きましょう。
$`\quad \Pi\,\alpha. \mathscr{E}`$
曖昧な全称記号を使う理由はありません。使わないことにしましょう。シグマ型はもちろん $`\Sigma`$（または総和記号 $`\sum`$）を使って書きます。
$`\quad \Sigma\,\alpha. \mathscr{E}`$
多相関数と、多相関数が所属する型〈集合〉は次のように書けます。
$`\quad \text{id} \in \Pi\, \alpha. [\alpha, \alpha]\\
\quad \text{length} \in \Pi\, \alpha. [\mrm{List}(\alpha), \mrm{Int}]\\
\quad \text{twice} \in \Pi\, \alpha. [ [\alpha, \alpha], [\alpha, \alpha]]
`$
ここで $`\text{twice}`$ は次のように定義されます。
$`\quad \text{twice} := \lambda\, f\in [\alpha, \alpha].(\, f\circ f \; \in [\alpha, \alpha]\,)`$
型変数が動く領域である“すべての型の集合”を $`{\bf T}`$ として、型に型を対応させる関数〈型関数 | 型構成子〉を書きたいなら、ラムダ記法を使いましょう。
$`\quad \lambda\, \alpha. [\alpha, \alpha] \;: {\bf T} \to {\bf T}\\
\quad \lambda\, \alpha. [\mrm{List}(\alpha), \mrm{Int}] \;: {\bf T} \to {\bf T}\\
\quad \lambda\, \alpha. [ [\alpha, \alpha], [\alpha, \alpha]] \;: {\bf T} \to {\bf T}\\
\quad \lambda\, \alpha, \beta, \gamma. [\alpha, \beta]\times[ \alpha , \gamma ] \;: {\bf T}^3 \to {\bf T}\\
\quad \lambda\, \alpha, \beta. [\mrm{Lit}(\alpha)\times \mrm{List}(\beta), \mrm{List}(\alpha\times \beta)] \;: {\bf T}^2 \to {\bf T}
`$
値のラムダ計算とどうしても区別したいなら、例えば大文字の $`\Lambda`$ を使うとか。ラムダ抽象に全称記号を使うのはやめましょう。
型関数（型レベルの関数）の呼び名は、型構成子、多相型、型パラメータを持つ型、総称型など、既にいっぱいあるのに、さらに全称型なんて呼んだら混乱が増すばかりです -- やめましょう。
指標のモデル型
指標を書くときに、構造の台集合〈underlying set | carrier〉となる構成素〈フィールド〉を、キーワード carrier でマークすることにします。
signature Content {
carrier C
operation id : C → UUID
operation url : C → URL
}
signature NatNums {
carrier T
operation zero : 1 → T
operation succ : T → T
}
signature ZeroOneAutomaton {
carrier S
operation tran : S×{0, 1} → S
operation init : 1 → S
}指標のモデルの圏から対象（モデル）を取り出すには、次のキーワードを使います。
some： とあるモデルini： 始モデル（モデルの圏の始対象）fin： 終モデル（モデルの圏の終対象）
例えば、
some Content： 指標 Content のとあるモデルini NatNums： 指標 NatNums の始モデルfin ZeroOneAutomaton： 指標 ZeroOneAutomaton の終モデル
Models-as-Types の立場なら、some, ini, fin を前置した指標は型になります。
モデル（を表す記号的表現）の前にキーワード carrier を付けると台集合を取り出せるとします。台集合は集合なので要素〈値〉を持ち、変数の型宣言に使えます。このときの変数の型は Sets-as-Types の意味の型です。
// c は、Content のとあるモデルの台集合の要素 let c : carrier some Content // n は、NatNums の始モデルの台集合の要素 let n : carrier ini NatNums // s は、ZeroOneAutomaton の終モデルの台集合の要素 let s : carrier fin ZeroOneAutomaton
some や ini、あるいはそれに carrier を付けた形の代わりに存在記号 ∃ やキーワード exists を使うメリットはありません -- やめましょう。
関連記事：
