北陸オフ会 - カノニカルな日々。IT戦記の中の方による北陸で新年オフ会やります！ に行って来ました。 こういう集まりは初めてだったのですが、なかなかどうして色々と面白いお話が聞けてとても面白かったです。自分の現状及び方向性がわかったのがよかった。でも、やはりいろいろな方に出会えたことというのが一番の収穫でした。 加えて、最近ちょっと気になっていたカインド（型の型）の話が思いがけず聞けたのがよかった。カインドとは型の型というのはその説明のとおり、型の型推論計算に関与しない情報を抽象したものらしい。すなわち、ラッセルの型理論ぽく表現すると、型よりも一階層上の類がカインド。
