Haskellの型と直観論理 - 朝日ネット 技術者ブログ

開発部のxgotoです。Haskellの初級・中級者向けのトピックを取り上げたいと思います。 今回は型(Type)についてです。型はHaskellの入門書でも必ず最初のほうに説明されるもので、手元の本によれば、 型とは、互いに関連する値の集合である。 ---- 『プログラミングHaskell』 Graham Hutton 著 / 山本和彦 訳 だとか、 値の世界は型と呼ばれる系統的な集まりへと分割される。 ---- 『関数プログラミング入門 Haskellで学ぶ原理と技法』 Richard Bird 著 / 山下伸夫 訳 などのように書かれています。たとえば Bool は True と False の2つの値からなる集合だし、Intは整数の集合というように、型は値の集合というふうにみることができます。それならば型などと呼ばずに集合と呼べばいいと思いますが、「異なるものには異なる名前をつけろ

[kmizushima]

カリー＝ハワード対応の話、ふつーにもっと広まるといいよね

[namakin]

カリー＝ハワード同型対応はもっと知られるべきだと思う。これを知ると知らないとでは、型というものに対する認識が全く変わってくる。

[hamamuratakuo]

"1934年、カリーはA -> Bという関数の型が「AならばB」という命題として読み替えることができるという興味深い事実を発見しました。さらにA -> B型の式（つまり関数）がこの命題の証明と対応することにも気づきました。"

[igrep]

たのしい

[h-hirai]

ああぁCoqの本も積んでる……。