ボトム型

出典: フリー百科事典『ウィキペディア(Wikipedia)』
ナビゲーションに移動 検索に移動

ボトム型: 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であらゆる型のリストの終端を表すNilList[Nothing]型である。

Rustではボトム型は!で表される。これは決して戻ることがない関数、例えばpanic!()を呼び出していたり無限ループを実行するような関数の型シグネチャで見られる。

Ceylonのボトム型はNotingである[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日閲覧。

参考文献[編集]