ボトム型とは - わかりやすく解説 Weblio辞書 (original) (raw)

ボトム型（ボトムがた、英: Bottom type）とは、型理論や数理論理学において値を持たない型のことである。ゼロ型または空型とも呼ばれ、アップタック記号（⊥）で表記される。戻り値の型がボトム型である関数は、いかなる値も返さない。カリー＝ハワード同型対応ではボトム型は偽に対応する。

計算機科学への応用

部分型付けシステムにおいて、ボトム型はすべての型の部分型である[1] 。（ただしその逆は成り立たない。つまり、すべて型の部分型が必ずしもボトム型であるとはいえない。）値を返さない関数（例えば無限ループや例外の送出、プログラムの終了など）の戻り値の型を表すのに使われる。

ボトム型は正常な返却ではないことを示すために使用されるので、普通は一切の値を持たない。これとは対照的にトップ型はシステム上可能なすべての値におよび、また、ユニット型はただ1つの値を持つ。ボトム型はいわゆるVoid型と混同されることがあるが、Void型に対してどんな操作も定義されないとはいえ、Void型は実際にはユニット型である。

ボトム型は次のような目的でよく使用される。

プログラミング言語での使用

一般的に使用される多くのプログラミング言語は空の型を明示的に表す手段を持たないが、いくつかの例外もある。

Haskellは空のデータ型をサポートしていない。しかし、GHCでは-XEmptyDataDeclsフラグによってdata Emptyを（コンストラクタなしで）定義できるようになる。Empty型は非終端プログラムおよび定数undefinedを含むため、完全に空というわけではない。 一般的にundefinedは何かが空の型を持ってほしいときに使用される。なぜならundefinedはどんな型にもマッチし（つまりすべての型の部分型）、undefinedを評価しようとするとプログラムの中止を引き起こし、それゆえ永久に応答を返さないからである。

Common Lispではシンボル NILが値を持たない型である。これはトップ型のTと対をなす。NILはしばしばNULLと混同されることがあるが、NULLはただ1つの値すなわちNILを持つ型である。

Scalaではボトム型はNothingで表される。例外をスローしたり正常に戻らない関数で使われるのに加え、共変なパラメタ化された型でも使用される。 例としてScalaのリストは共変なので、全ての型AについてList[Nothing]はList[A]の部分型である。そのため、Scalaであらゆる型のリストの終端を表すNilはList[Nothing]型である。

Rustではボトム型は!で表されていた。Rust 2018エディションからは、識別子の最後に!が置かれているならばマクロと見做し、引数などとともにマクロ展開を行う演算子となった。

Ceylonのボトム型はNothingである[2] 。これはScalaのNothingに似ており、他の全ての型の交差型を表し、また空の集合を表す。

脚注

  1. ^ Pierce, Benjamin C. (1997). Bounded Quantification with Bottom.
  2. ^ “Chapter 3. Type system — 3.2.5. The bottom type”. The Ceylon Language. Red Hat, Inc.. 2017年2月19日閲覧。

参考文献

関連項目

表話編歴データ型
ビット列 ビット トリット ニブル オクテット バイト ワード ダブルワード（英）
数値 整数型 符号付整数型 十進型（英語版） 有理数型（英語版） 実数型 複素数型 固定小数点型 浮動小数点型 半精度 単精度 倍精度 四倍精度 八倍精度（英語版） 拡張倍精度 ミニフロート bf16
プリミティブ 論理型 数値型 キャラクタ型 ストリング型 ヌル終端 列挙型
コンポジット 配列 可変長配列 連想配列 構造体 レコード 共用体 タグ共用体（英語版） タプル コンテナ リスト キュー スタック セット マップ ラッパー ツリー 代数的データ型 抽象データ型 再帰データ型 Option型
ポインタ 物理アドレス型 論理アドレス型（英語版） 仮想アドレス型（英語版） 参照型
その他 void型 null型 トップ型（英語版） ボトム型 関数の型（英語版） 動的束縛型 不透明型（英語版） 抽象型 シンボル型（英語版）
カテゴリ