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