型理論 - pogi-log

型理論

型理論(かたりろん、type theory)

プログラミング言語の型自体とは何かを学ぶには型理論を学ぶ必要がある

ラッセルあたりで単純型理論、分岐型理論が出てきた

最近の型理論はMartin-Löf型理論(MLTT)を基に作られてそう

Martin--Löf型理論では、型が可述的(階層的？)に構成されているのでラッセルのパラドックスのような自分自身が含まれる型という矛盾が起きないようになっている

ホモトピー理論と型理論を組み合わせて作られたHomotopy Type Theory(HoTT)というものもある

構成されるもの

項(term)

型(type)

判断(judgement)

推論規則(inference rule)

プログラミング言語での定義？

型は値の名前付き集合

値は値集合の要素