Arantium Maestum

プログラミング、囲碁、読書の話題

型システムのカインドという概念についてのメモ

Types and Programming Languagesの最後のほうに「カインド」という概念が出てくる。 System Fをさらに拡張したSystem Fωという型システムが存在していて、その「拡張の方向」がカインドだということらしい。(ちなみにSystem FωはF-ing Modules論文のベース…

let多相と型制約と型推論

こういう(けっこう前の)記事があって面白かった: no-maddojp.hatenablog.com 大変面白かったのと、何故こうなるのかが微妙に理解し切れなかったのと、で少し自分でも調べてみた。 ちょっと例を簡略化すると let f x = x in f 1, f true は型検査を通るけ…