2013-06-21 Functors as Types 圏一般論 プログラム意味論 型の意味は関手で、項の意味は自然変換だと考える。型である関手の定義域は、「スキーマ、シェープ、指標」などと呼ばれる。型の定義域の全体はまた圏で、スキーマ圏、シェープ圏、指標圏などと呼ぶ。インスティチューションや導来子との類似性がある。 導来子の図式の圏 → スキーマ圏、シェープ圏、指標圏 導来子の値 → 指標に対するモデル圏 導来子の単位圏での値 → モデルのアンビエント圏 おそらく、総称(多相)の説明になるだろう。