Haskell の存在型というのは一体どういう意味なのだろうか。文字列型や整数型なら意味がわかる。しかし、存在型の存在という言葉にどんな意味がこめられているのか見当もつかない。 探し回っていたら、GHCのマニュアルの 7.4. Extensions to data types and type synonyms というページを見つけた。このページの 7.4.5. Existentially quantified data constructors に存在型の説明が書いてあった。これを読んだら疑問が氷解した。どうも存在型 (Existetial type) の「存在 (Existential) 」というのは、述語論理学の存在量化子の「存在」らしい。たとえば、「ある自然数 n について、n * n は２５である」という命題を述語論理学の記号で書くと下のようになる。 ∃n (n ∈ N, n *
