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

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