空型
#Fleeting_Notes
空型(
empty type
)、absurd type、
ボトム型
(
bottom type
)
値を持たない型/要素を持たない型
論理学の偽(
⊥
)が型理論での空型
$ 0
特定のプログラミング言語だと、
TypeScript
の
never型
Lean 4だとEmtpy型
Haskellだと
Void
型？
$ 0 : \mathcal{U}
$ \lnot P \equiv (P \to 0)
対応するもの
(論理) false
(集合)
空集合
(圏論)
始対象
(型理論) 空型
確認用
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