ボトム型
| 型システム |
|---|
| 主要カテゴリ |
|
静的型付け 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に似ており、他の全ての型の交差型を表し、また空の集合を表す。
脚注
[編集]- ^ Pierce, Benjamin C. (1997). Bounded Quantification with Bottom.
- ^ “Chapter 3. Type system — 3.2.5. The bottom type”. The Ceylon Language. Red Hat, Inc.. 2017年2月19日閲覧。
参考文献
[編集]関連項目
[編集]- Void
- Null
- NaN
- Nil
- Haskellの表示的意味論
