Existential types
@Deprecated
Existential types
(集合論の)Unionは、
という定義だったが、型理論においては、このような型は作れず
という感じの定義(disjoint union)になっている。 をどこかから探してくれたりはしない。 Scalaでは、(disjointでない)union風の定義になっており、一般には を取り出せない。
Curry–Howard correspondence, カリー=ハワード同型対応
記号論理の命題として
が成立するが、記号を型間のものに変えてしまって
としても成立する。このような対応をCurry–Howard correspondenceという(と思う)。
特にこの場合、
について、
とすればよい。
Haskellのexistential types
Haskellにはexists
はなくて、上の命題を使ってforall
で表現する(らしい)。たとえば
data T = forall a. MkT a
について
Top type
全てのtermを含む型:
をtop typeといい
と書く。ScalaでいうところのAny
である。
参考文献
- 存在型を全称限量子と代数的データ型でエンコードする - maoeのブログ
- Haskell/Existentially quantified types - Wikibooks, open books for an open world
- Top type - Wikipedia, the free encyclopedia
*1:disjointでないとCurry-Howardが成立しないようだ