Existential types

(集合論の)Unionは、

という定義だったが、型理論においては、このような型は作れず

$\exists\limits_{x} F(x) = \bigcup\limits_{x} \left{(x, p) | p \in F(x) \right}$ *1

という感じの定義(disjoint union)になっている。 $x$ をどこかから探してくれたりはしない。 Scalaでは、(disjointでない)union風の定義になっており、一般には $x$ を取り出せない。

記号論理の命題として

が成立するが、記号を型間のものに変えてしまって

$\forall\limits_x(F(x) \rightarrow A) \simeq (\exists\limits_x F(x) ) \rightarrow A$

としても成立する。このような対応をCurry–Howard correspondenceという(と思う)。

特にこの場合、

について、

とすればよい。

Haskellにはexistsはなくて、上の命題を使ってforallで表現する(らしい)。たとえば

data T = forall a. MkT a

について

- $\sim \text{MkT} \in \forall\limits_{a \in \mathbb{*}} (a \rightarrow T)$
- $\Leftrightarrow \text{\tilde{MkT}} \in (\exists\limits_{a \in \mathbb{*}} a) \rightarrow T$

全てのtermを含む型:

をtop typeといい

と書く。ScalaでいうところのAnyである。

*1:disjointでないとCurry-Howardが成立しないようだ