Types and Programming Languages

Types and Programming Languages

Types and Programming Languages

卒研のためにTAPLをチビチビ読み進めてます。と言ってもすべての内容が必要なわけでもなさそうなので、まぁ半分くらいは趣味の範疇なのかな。

非常に面白い。Curry-Howard correspondenceとか。論理学と型の間にこんな蜜月関係があったとは!ここにあるように、「"aではない" は "aを受け取る継続" という型に対応する」なんて意外過ぎ。その他、「そんなとこまで型の守備範囲なのね」っていう話題が続いていくようで、興味は尽きません。型いいよ型。