Loading article…
数理論理学における理論である型理論では、型システムの底辺型は他のすべての型のサブタイプとなる型である。[1]
このようなタイプが存在する場合、アップタック(⊥) 記号で表されることがよくあります。
空型との関係
ボトム型がuninhabitedの場合、戻り型が bottom である関数は、unit 型の唯一の値でさえも、いかなる値も返すことができません。したがって、このような言語では、ボトム型は、カリー-ハワード対応では偽に対応する 、ゼロ、never、または空の型として知られています。
ただし、一番下の型に人が住んでいる場合は、空いている型とは異なります。
コンピュータサイエンスの応用
サブタイピングシステムでは、ボトムタイプはすべてのタイプのサブタイプです。[1]これは、システム内のすべての可能な値をカバーする トップタイプと双対です。
型システムが健全な場合、ボトム タイプは空であり、ボトム タイプという用語は論理的な矛盾を表します。このようなシステムでは、通常、ボトム タイプと空のタイプの間に区別はなく、用語は同じ意味で使用できます。
一番下の型が占有されている場合、その用語は通常、未定義の動作、無限再帰、回復不能なエラーなどのエラー状態に対応します。
Bounded Quantification with Bottom [1]の中で、ピアスは「ボット」には多くの用途があると述べています。
- 例外のある言語では、 raise 構造の自然な型はraise ∈ exception -> Botであり、他の制御構造でも同様です。直感的に、ここでの Bot は答えを返さない計算の型です。
- Bot は、多態的なデータ構造の「リーフ ノード」を型指定する場合に便利です。たとえば、List(Bot) は nil に適した型です。
- ボトムは、 Javaなどの言語の「ヌルポインタ」値（どのオブジェクトも指していないポインタ）の自然な型です。Javaでは、ヌル型は参照型のユニバーサルサブタイプです。はヌル型の唯一の値であり、任意の参照型にキャストできます。[2]ただし、ヌル型は上記のようにボトム型ではなく、およびその他のプリミティブ型のサブタイプでもありません。
nullint - Top と Bot の両方を含む型システムは、型推論の自然なターゲットであると思われます。これにより、省略された型パラメータの制約を境界のペアで捕捉できます。S<:X<:T と記述すると、「X の値は S と T の間のどこかにある必要があります」という意味になります。このようなスキームでは、完全に制約のないパラメータは、下側が Bot、上側が Top で境界付けされます。
プログラミング言語では
最も一般的に使用される言語には、ボトムタイプを示す方法がありません。ただし、注目すべき例外がいくつかあります。
Haskellでは、ボトム型は と呼ばれますVoid。[3]
Common Lispでは、型 はNIL値を含まず、あらゆる型のサブタイプです。[4]という名前の型は、シンボル自体という1つの値を持つ というNIL名前の型と混同されることがあります。
NULLNIL
Scalaでは、ボトムの型は と表記されますNothing。例外をスローする関数や正常に返さない関数に使用されるほか、共変の パラメータ化された型にも使用されます。たとえば、Scala の List は共変の型コンストラクタであるため、すべての型 A の のList[Nothing]サブタイプです。したがって、任意の型のリストの終わりを示すオブジェクトである Scala の は、型 に属します。
List[A]NilList[Nothing]
Rustでは、ボトム型はnever型と呼ばれ、 で表されます。これは、呼び出しやループを永遠に繰り返す!など、決して戻らないことが保証されている関数の型シグネチャに存在します。また、値を生成しないが式として使用できる、やなどの特定の制御フローキーワードの型でもあります。 [5]panic!()breakreturn
Ceylonでは、一番下の型は ですNothing。[6]これはNothingScalaの に相当し、他のすべての型の積集合と空集合を表します。
Juliaでは、下型は であるUnion{}。[7]
TypeScriptでは、ボトムタイプはですnever。[8] [9]
Closure Compilerアノテーションを使用したJavaScriptでは、ボトム タイプは(文字通り、ユニット タイプの null 以外のメンバー) です。
!NullNull
PHPでは、一番下の型は ですnever。
Pythonのオプションの静的型注釈では、一般的なボトム型はtyping.Never(バージョン 3.11 で導入)です。 [10 ]一方、 typing.NoReturn(バージョン 3.5 で導入) は、特に戻り値のない関数の戻り値の型として使用できます ( が導入される前は、一般的なボトム型としても使用されていましたNever)。[11]
Kotlinでは、ボトムタイプはですNothing。[12]
Dでは、下のタイプはであるnoreturn。[13]
Dartでは、バージョン2.12のサウンドヌルセーフティアップデート以降、Never型はボトム型として導入されました。それ以前は、ボトム型は でしたNull。[14] [15]
参照
参考文献
- ^ abc Pierce, Benjamin C. (1997). 「Bounded Quantification with Bottom」インディアナ大学 CSCI 技術レポート(492): 1.
- ^ 「セクション 4.1: 型と値の種類」。Java言語仕様(第 3 版)。
- ^ “Data.Void”. Hackage . 2023年9月20日閲覧。
- ^ 「Type NIL」。Common Lisp HyperSpec 。 2022年10月25日閲覧。
- ^ 「プリミティブ型 never」。Rust標準ライブラリのドキュメント。2020年 9 月 24 日閲覧。
- ^ 「第3章 型システム — 3.2.5 ボトム型」。The Ceylon Language。Red Hat, Inc. 2017年2月19日閲覧。
- ^ 「エッセンシャル - Julia 言語」、Julia プログラミング言語ドキュメント、 2021 年 8 月 13 日取得
- ^ never 型、TypeScript 2.0 リリース ノート、Microsoft、2016-10-06、2019-11-01取得
- ^ never 型、TypeScript 2.0 リリース ノート、ソース コード、Microsoft、2016-10-06、2019-11-01取得
- ^ 「typing — 型ヒントのサポート — Python 3.12.0a0 ドキュメント」。docs.python.org 。 2024年3月2日閲覧。
- ^ entering.NoReturn、typing — 型ヒントのサポート、Python ドキュメント、Python Software Foundation 、 2024-03-02取得
- ^ Nothing 、 2020年5月15日閲覧
- ^ 「Types - Dプログラミング言語」dlang.org . 2022年10月20日閲覧。
- ^ ヌル安全性を理解する - 上部と下部、2022-04-13取得
- ^ ヌル安全性を理解する - 到達不能コードには絶対に使用しない、2022-04-13取得
さらに読む
- ピアス、ベンジャミン C. (2002)。型とプログラミング言語。MITプレス。ISBN 0-262-16209-1。