ボトム型

ボトム型とは

ボトム型（Bottom type）とは、型理論や数理論理学において、値を持たない型のことです。ゼロ型または空型とも呼ばれ、記号「⊥」で表されます。ボトム型は、関数が値を返さない状況を表すために使用され、カリー＝ハワード同型対応においては「偽」に対応します。

計算機科学における応用

ボトム型は、計算機科学において様々な場面で応用されています。特に重要なのは、以下の点です。

部分型付けシステム: ボトム型は、すべての型の部分型となります。これは、値を返さない関数が、どのような型を期待される場所にも代入できることを意味します。ただし、すべての型の部分型がボトム型であるわけではありません。
値を返さない関数の表現: 無限ループ、例外のスロー、プログラムの終了など、値を返さない関数の戻り値の型として使用されます。
正常な返却ではないことの表現: ボトム型は、関数が正常に値を返さないことを示すために使用されます。対照的に、トップ型はシステム上で可能なすべての値を表し、ユニット型はただ1つの値を持ちます。
Void型との違い: ボトム型は、void型と混同されることがありますが、void型は実際にはユニット型であり、ボトム型とは異なります。

ボトム型の具体的な使用例

ボトム型は、主に以下の目的で使用されます。

1. 関数の発散: 関数や計算が結果を返さずに発散することを示すために使用されます。これは、プログラムが必ずしもエラーで終了するわけではなく、サブルーチンが呼び出し元に戻らずに終了する場合や、継続などの別の手段で脱出する場合も含まれます。
2. エラーの表現: エラーを区別する必要がない場合、エラーを示すために使用されます。ただし、実用的なプログラミング言語では、オプション型や例外処理など、より高度な手法が一般的に使用されます。

プログラミング言語におけるボトム型

多くのプログラミング言語はボトム型を明示的にサポートしていませんが、一部の言語ではボトム型を表現する手段があります。

Haskell: Haskellは空のデータ型を明示的にはサポートしていませんが、GHCでは `-XEmptyDataDecls` フラグを使用することで、`data Empty` というコンストラクタを持たない空の型を定義できます。この `Empty` 型は、非終端プログラムや `undefined` を含んでいるため、完全に空というわけではありません。`undefined` は、型が期待されるが値が存在しない場合に使用され、どの型にもマッチし、評価するとプログラムが中止されるため、結果を返しません。
Common Lisp: Common Lispでは、シンボル `NIL` が値を持たない型として扱われます。これは、すべての値を表すトップ型 `T` と対をなします。`NIL` は、単一の値である `NIL` を持つ `NULL` 型とは異なります。
Scala: Scalaでは、ボトム型は `Nothing` で表されます。`Nothing` は、例外をスローしたり、正常に戻らない関数で使用されるだけでなく、共変なパラメータ化された型でも使用されます。例えば、`List[Nothing]` はすべての型 `A` に対して `List[A]` の部分型となります。これにより、リストの終端を表す `Nil` は `List[Nothing]` 型となります。
Rust: Rustでは、以前は `!` がボトム型を表していましたが、Rust 2018エディションからはマクロとして扱われるようになりました。マクロは引数などとともに展開されるため、ボトム型を直接表す記号としては使用されなくなりました。
Ceylon: Ceylonでは、ボトム型は `Nothing` で表されます。Scalaと同様に、`Nothing` は他のすべての型の交差型であり、空集合を表します。

まとめ

ボトム型は、値を持たない型であり、計算機科学において重要な概念です。関数の発散やエラーの表現に使用され、特に型理論やプログラミング言語の設計において、正確な型の表現を可能にするために不可欠です。また、プログラミング言語ごとのボトム型の扱い方を理解することは、より深い型システムの理解につながります。

参考資料

Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 0-262-16209-1

関連項目

Void
Null
NaN
Nil
* Haskellの表示的意味論

もう一度検索