ボトム型
From Wikipedia, the free encyclopedia
| 型システム |
|---|
| 主要カテゴリ |
|
静的型付け vs 動的型付け 強い vs 弱い 明示的 vs 型推論 名前的 vs 構造的 ダックタイピング |
| マイナーカテゴリ |
|
部分型 再帰型 部分構造型 依存型 漸進的型付け フロータイピング 潜在的型付け |
| 型理論のコンセプト |
|
直積型 - 直和型 交差型 - 共用型 単一型 - 選択型 帰納型 - 精製型 トップ型 - ボトム型 函数型 - 商型 全称型 - 存在型 一意型 - 線形型 |
ボトム型(ボトムがた、英: 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に似ており、他の全ての型の交差型を表し、また空の集合を表す。