３．２ 集合の要素を射に
集合の世界は要素を中心に考えるが、圏論の世界は射を中心に考える。そこで、集合を考えるとき、その要素を射に変えるものが必要となる。
その役割を果たしてくれるのが、一つだけの要素からなる集合である。この集合はシングルトンと呼ばれる。Haskellではデータ型()として用意している。
確認してみよう。まず、()のデータ型を調べるてみよう。
Prelude> :i () data () = () -- Defined in ‘GHC.Tuple’ instance Bounded () -- Defined in ‘GHC.Enum’ instance Enum () -- Defined in ‘GHC.Enum’ instance Eq () -- Defined in ‘GHC.Classes’ instance Ord () -- Defined in ‘GHC.Classes’ instance Read () -- Defined in ‘GHC.Read’ instance Show () -- Defined in ‘GHC.Show’ instance Monoid () -- Defined in ‘GHC.Base’
ちなみに、\(Int\)と\(Bool\)のデータ型を調べると次のようになっている。
Prelude> :i Int data Int = GHC.Types.I# GHC.Prim.Int# -- Defined in ‘GHC.Types’ instance Bounded Int -- Defined in ‘GHC.Enum’ instance Enum Int -- Defined in ‘GHC.Enum’ instance Eq Int -- Defined in ‘GHC.Classes’ instance Integral Int -- Defined in ‘GHC.Real’ instance Num Int -- Defined in ‘GHC.Num’ instance Ord Int -- Defined in ‘GHC.Classes’ instance Read Int -- Defined in ‘GHC.Read’ instance Real Int -- Defined in ‘GHC.Real’ instance Show Int -- Defined in ‘GHC.Show’ Prelude> :i Bool data Bool = False | True -- Defined in ‘GHC.Types’ instance Bounded Bool -- Defined in ‘GHC.Enum’ instance Enum Bool -- Defined in ‘GHC.Enum’ instance Eq Bool -- Defined in ‘GHC.Classes’ instance Ord Bool -- Defined in ‘GHC.Classes’ instance Read Bool -- Defined in ‘GHC.Read・f instance Show Bool -- Defined in ‘GHC.Show’
データ型\(Bool\)は\(data \ Bool = False | True\)となっているので、\(False\)と\(True\)二つの要素を取ることが分かる。また、\(Int\)については、その要素はGHC.Typesで定義されていることが分かる。
遡って、シングルトンは、\(Data () = ()\)となっていたので、要素も()であることが分かる。確認してみよう。
Prelude> :t () () :: ()
である。::の左側は要素の()で、右側はデータ型の()である。
シングルトンを用いると、集合の要素を射に変えることができる。それは、シングルトンから集合の要素\(a\)へ向かう矢印\(f_a\)を用意することで実現できる。下図は、自然数の集合の各要素を射で表したものである。この場合、射の数は無数になる(但し、数え上げることはできる)。
シングルトンは要素の数が一つだけの集合である。それでは、要素の数がゼロの集合はあるのだろうか。これは、数の議論に似ている。建物で、地面に接している階を、日本では1階にしているが、海外に行くと0階(あるいはGround)となっていることに戸惑った人は多いことだろう。普段の癖で思わず1階のボタンを押してしまい、エレベータのドアーが空いたときそこがロビーでないことにビックリした経験を誰しも持っているのではないだろうか。
数学の世界では、要素の数がゼロの集合が存在する。これは空集合と呼ばれる。前の記事で述べたが、Haskellの世界では\(Void\)として用意している(但し、これを用いるときは、Data.Voidというモジュールをインポートする必要がある)。それでは確認してみよう。
Prelude> import Data.Void Prelude Data.Void> :i Void data Void -- Defined in ‘Data.Void’ instance [safe] Eq Void -- Defined in ‘Data.Void’ instance [safe] Ord Void -- Defined in ‘Data.Void’ instance [safe] Read Void -- Defined in ‘Data.Void’ instance [safe] Show Void -- Defined in ‘Data.Void’
\(Void\)と呼ばれるデータ型があることが分かる。
\(Void\)は要素が何もないので、真空の状態と見なすことができる。宇宙が真空の状態から埋めれたように、空から有が生じると考えることができる。あるいは、論理の世界では、\(Void\)は偽(\(false\))、シングルトンは真(\(true\))と見なす。論理の世界では、嘘の上にどのようなことを述べたとしても正しいと考えるので、偽からはどのような事でも生みだせると考える（ここでは生み出すものはデータ型）。その役割をしているのが\(absurd\)という関数である。確認してみよう。
Prelude Data.Void> :t absurd absurd :: Void -> a
\(absurd\)という関数は、任意のデータ型を出力していることが確認できた。\(absurd\)の意味は、常識に反した、理屈に反する、非条理ななどだ。このようなわけで、この関数は用意してあるだけで使うことはまずない。ここでは、それぞれのデータ型はこれから生み出されたと考えておくことにしよう。
要素の数が0と1の集合について話したので、ついでに要素数が2である集合は何であろうか。勿論、偽と真の値を有するブール集合である。Haskellではデータ型\(Bool\)として用意しているが、有用性が高いことは言うまでもない。
