Loading article…
数理論理学における型理論では、型システムの最下位型とは、他のすべての型のサブタイプである型のことである。 [ 1 ]
そのようなタイプが存在する場合、それはしばしば上向きタック（⊥）記号で表されます。
ボトム型が空の場合、戻り値の型がボトムである関数は、単位型の唯一の値であっても、いかなる値も返すことができません。このような言語では、ボトム型はゼロ、ネバー、または空型として知られており、カリー・ハワード対応では偽に対応します。
しかし、底部の区画に人が居住している場合は、空室の場合とは異なる。
型システムが健全である場合、最下位型は空であり、最下位型の項は論理的矛盾を表します。このようなシステムでは、通常、最下位型と空型は区別されず、これらの用語は互換的に使用できます。
サブタイピングシステムでは、ボトムタイプはすべてのタイプのサブタイプです。[ 1 ]これは、システム内のすべての可能な値を網羅するトップタイプと双対です。
最下層の型が占有されている場合、その項は通常、未定義動作、無限再帰、回復不能なエラーなどのエラー状態に対応します。
『Bot と Bottom による限定量化』[ 1 ]の中で、Pierce は「Bot には多くの用途がある」と述べています。
nullは null 型の唯一の値であり、任意の参照型にキャストできます。[ 2 ]intただし、null 型は上記のようにボトム型ではなく、やその他のプリミティブ型のサブタイプではありません。一般的に使われている言語のほとんどには、ボトムタイプを表す方法がありません。ただし、いくつか注目すべき例外があります。
Void。[ 3 ]NIL値を含まず、すべての型のサブタイプです。[ 4 ]という名前の型は、1 つの値、つまりシンボル自体を持つNILという名前の型と混同されることがあります。NULLNILNothing。 は、例外をスローするだけの関数や、通常どおり値を返さない関数に使用されるほか、共変パラメータ型にも使用されます。たとえば、Scala の List は共変型コンストラクタなので、 はすべての型 AList[Nothing]の のサブタイプです。したがって、任意の型のリストの末尾を示すオブジェクトである Scala の は、型 に属します。List[A]NilList[Nothing]!。これは、例えばを呼び出したり、永久にループしたりすることで、決して戻り値を返さないことが保証されている関数の型シグネチャに存在します。また、値を生成しないものの式として使用できる、やpanic!()などの特定の制御フローキーワードの型でもあります。 [ 5 ]breakreturn[[noreturn]]voidNothing。[ 7 ]これはNothingScala の に相当し、他のすべての型の共通部分と空集合を表します。Union{}。[ 8 ]never。[ 9 ] [ 10 ]!NullNullnever。typing.Never(バージョン 3.11 で導入) であり、[ 11 ]一方typing.NoReturn(バージョン 3.5 で導入) は、特に戻り値を返さない関数の戻り値の型として使用できます ( が導入される前は一般的なボトム型としても使用されていましたNever)。[ 12 ]Nothing。[ 13 ]noreturn。[ 14 ]Never型がボトム型として導入されました。それ以前は、ボトム型は でしたNull。[ 15 ] [ 16 ]