空型
#Fleeting_Notes
空型(empty type)、absurd type、ボトム型(bottom type)
値を持たない型
論理学の偽(⊥)が型理論でのボトム型$ 0
特定のプログラミング言語だと、
TypeScriptのnever型
$ 0 : \mathcal{U}
$ \lnot P \equiv (P \to 0)
確認用
Q. 空型(empty type)とは
関連
unit type
メモ
The Empty Type
『Introduction to Homotopy Type Theory』 Chapter 4 More inductive types 4.3 The empty type
『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 1 Type theory 1.7 Coproduct types
有限余積 -- ホモトピー型理論
ボトム型 - Wikipedia
調査用
Google.icon 空型(日)
Google.icon Empty type(英)
Wikipedia.icon
空型 - Wikipedia(日)
空型(検索) - Wikipedia(日)
Wikipedia.icon
Empty type - Wikipedia(英)
Empty type(検索) - Wikipedia(英)
#ボトム型 #bottom_type