依存型
依存型(いぞんがた、dependent type)
Martin-Löf型理論
、
依存型理論
で出てくるもの
値に依存する型
依存型が使えるプログラミング言語
$ A: \mathcal{U}
$ \mathcal{U}
: 型の成す
宇宙
ここでいう宇宙は
グロタンディーク宇宙
$ B : A \to \mathcal{U}
型
$ A
の項
$ x : A
に応じて変わる新しい型
$ B(x)
が依存型
確認用
Q. 依存型
Q. 値に依存する型とは
参考
『Homotopy Type Theory: Univalent Foundations of Mathematics』
メモ
https://ja.wikipedia.org/wiki/依存型?wprov=sfti1
依存型と総称型の圏論的解釈 - 檜山正幸のキマイラ飼育記 (はてなBlog)
依存型 Dependent Type: 最新の百科事典、ニュース、レビュー、研究
関連
(論理)
述語
(集合) 集合の族
(ホモトピー)
ファイブレーション
ATS2
Agda
Idris
Epigram
Martin-Löf型理論
デカルト閉圏(CCC)
直観主義論理
単純型付きラムダ計算
篩型
#依存型理論
#Fleeting_Notes