型理論
型理論(かたりろん、type theory)
プログラミング言語の型自体とは何かを学ぶには型理論を学ぶ必要がある
単純型理論はラッセルではないかも…？
Martin--Löf型理論では、型が可述的(階層的？)に構成されているのでラッセルのパラドックスのような自分自身が含まれる型という矛盾が起きないようになっている 構成されるもの
項(term)
型(type)
推論規則(inference rule)
プログラミング言語での定義？
型は値の名前付き集合
値は値集合の要素
関連リソース
関連
参考