「アハハハハ（ちからない笑い）： 全称型／存在型」で触れた Swift の existential any だけど； some というキーワードは既に使われていて、any にするしかなかった、という事情みたいです。
Swift では、キーワードを付ける付けないに関わらず、プロトコル（指標）に適合する型は存在型と呼んでいたようです。キーワード some は存在型を示す印なんですが、コンパイル時に型の正体が分かる存在型をマークする目的のキーワード、一方の any は実行時まで正体が分からない（プロトコルは分かっている）存在型を示す印、みたい。
Haskell の存在型がなんで forall なのかはまだ分かりません。単にキーワードを増やしたくなかった、とか、そんな理由かも知れません。ところで、「アハハハハ（ちからない笑い）： 全称型／存在型」に次のように書きました。
前の記事で紹介した記事「Haskell/存在量化された型」に、なぜ存在型に全称限量子なのか？ が説明されている（ように思える）のですが、ナニイッテルカワカランですね -- コジツケっぽい。
なぜコジツケっぽいかというと； forall a. MkT a と MkT (exists a. a) で定義される型は同じ（同型）だ書いてあるのですが、そんなことある？（いや、ない。） おそらく、forall, exists を文字通りの論理記号だと解釈して、次の論理的同値を根拠に説明しようとしているようです（説明にギャップがありすぎて、真意が読めないのですが）。
$`\quad \forall x.( p(x) \to q ) \equiv (\exists x.p(x)) \to q`$
$`q`$ に $`\bot`$（偽）を代入すると：
$`\quad \forall x.( p(x) \to \bot ) \equiv (\exists x.p(x)) \to \bot`$
偽との含意演算は否定することなので、これは、以下のド・モルガンの法則（限量子バージョン）になります。
$`\quad \forall x.( \lnot p(x) ) \equiv \lnot (\exists x.p(x))`$
依存型においても類似の同型が成立しています。
$`\quad \Pi\, \alpha.[\mathscr{E}, A] \cong [\Sigma\, \alpha. \mathscr{E}, A]`$
ここで、$`A`$ は何か決まった（型変数を含まない）型です。型項 $`\mathscr{E}`$ を $`\alpha`$ と置けば：
$`\quad \Pi\, \alpha.[\alpha, A] \cong [\Sigma\, \alpha. \alpha, A]`$
$`\mathrm{F} := \lambda\,\alpha .[\alpha, A]`$ と置くと：
$`\quad \Pi\, \alpha.\mathrm{F}(\alpha) \cong \mathrm{F}(\Sigma\, \alpha. \alpha)`$
この同型に次の置換を施します。
- $`\Pi`$ →
forall - $`\alpha`$ →
a - $`\mathrm{F}`$ →
MkT - $`\cong`$ →
= - $`\Sigma`$ →
exists
すると：
forall a. MkT a = MkT (exists a. a)
いや待て、MkT は渡された型をラップ〈ボクシング〉するだけの型関数〈型構築子〉だったはず。論理否定 $`\lnot`$ や $`\mathrm{F}`$ のように双対化〈dualize〉する能力はないだろうよ。
関連記事：
