ボトム型

ボトム型（ボトムがた、）とは、型理論や数理論理学において値を持たない型のことである。ゼロ型または空型とも呼ばれ、アップタック記号（⊥）で表記される。戻り値の型がボトム型である関数は、いかなる値も返さない。カリー＝ハワード同型対応ではボトム型は偽に対応する。
計算機科学への応用.
部分型付けシステムにおいて、ボトム型はすべての型の部分型である 。（ただしその逆は成り立たない。つまり、すべて型の部分型が必ずしもボトム型であるとはいえない。）値を返さない関数（例えば無限ループや例外の送出、プログラムの終了など）の戻り値の型を表すのに使われる。
ボトム型は正常な返却ではないことを示すために使用されるので、普通は一切の値を持たない。これとは対照的にトップ型はシステム上可能なすべての値におよび、また、ユニット型はただ1つの値を持つ。ボトム型はいわゆるVoid型と混同されることがあるが、Void型に対してどんな操作も定義されないとはいえ、Void型は実際にはユニット型である。
ボトム型は次のような目的でよく使用される。
プログラミング言語での使用.
一般的に使用される多くのプログラミング言語は空の型を明示的に表す手段を持たないが、いくつかの例外もある。
Haskellは空のデータ型をサポートしていない。しかし、GHCではcodice_1フラグによってcodice_2を（コンストラクタなしで）定義できるようになる。codice_3型は非終端プログラムおよび定数codice_4を含むため、完全に空というわけではない。 一般的にcodice_4は何かが空の型を持ってほしいときに使用される。なぜならcodice_4はどんな型にもマッチし（つまりすべての型の部分型）、codice_4を評価しようとするとプログラムの中止を引き起こし、それゆえ永久に応答を返さないからである。
Common Lispではシンボル codice_8が値を持たない型である。これはトップ型のcodice_9と対をなす。codice_8はしばしばcodice_11と混同されることがあるが、codice_11はただ1つの値すなわちcodice_8を持つ型である。
Scalaではボトム型はcodice_14で表される。例外をスローしたり正常に戻らない関数で使われるのに加え、共変なパラメタ化された型でも使用される。 例としてScalaのリストは共変なので、全ての型codice_15についてcodice_16はcodice_17の部分型である。そのため、Scalaであらゆる型のリストの終端を表すcodice_18はcodice_16型である。
Rustではボトム型はcodice_20で表されていた。Rust 2018エディションからは、識別子の最後にcodice_20が置かれているならばマクロと見做し、引数などとともにマクロ展開を行う演算子となった。
Ceylonのボトム型はcodice_14である 。これはScalaのcodice_14に似ており、他の全ての型の交差型を表し、また空の集合を表す。