引き続きcategory theory for programmersを読んでいるので続き。

代数的データ型

a, bが型だとして、(a, b)という直積の型を考える。これは、集合の圏の世界で、productになっているのだった。 同様に、a | bあるいはhaskel風に書くならEither a bという直和型を考える。これは、集合の圏の世界で、coproductになっている。 で、productは名前の通り、「積」のように振る舞い、coproductは「和」のように振る舞う。

さらに、Void=値を1個も持たない型(=要素を1個も持たない集合)が、coproductの単位元0のように振る舞い、 Unit=値を1個だけ持つ型が、productの単位元1のように振る舞う。 〜のように振る舞うというのを、もう少し具体的に言うと、任意の型aに対して、Voidとの積を考えると、Voidとisomorphicになるということである。(a, Void)型の値というのは、a型の値とVoid型の値のペアだが、Void型の値というものはないので、結果、(a, Void)型の値というものも作れない。よって、Voidと同じ構造とみなせる。

こんな調子で、たとえば数であれば分配則a * (b + c) = a * b + a * cが成り立つわけだが、同じように、型の世界でも、(a, Either b c)とEither (a, b) (a, c)は同じ構造とみなせるというようなことが書いてある。同じ構造とみなせるつうのは、つまり、isomophicだっつうこと。それは圏論の言葉で言うと、両者の間に、f . g = id, g. f = idとなるような射(関数)が存在するということ。

で、数の演算との対応関係だけでなくて、bool代数のand, orとの対応関係(こいつらも積と和みたいなもんだったね)も考えることができて、それを深ぼってくと、論理学と型理論との対応関係になるんだとか。Curry-Howard isomorphismというらしい