読者です 読者をやめる 読者になる 読者になる

bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

集合から圏論へ:ミクロな世界からの宇宙への旅立ち(2)

プログラマーのための圏論 (圏論とHaskell)

3.2 集合の要素を射に

集合の世界は要素を中心に考えるが、圏論の世界は射を中心に考える。そこで、集合を考えるとき、その要素を射に変えるものが必要となる。
その役割を果たしてくれるのが、一つだけの要素からなる集合である。この集合はシングルトンと呼ばれる。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\)を用意することで実現できる。下図は、自然数の集合の各要素を射で表したものである。この場合、射の数は無数になる(但し、数え上げることはできる)。
f:id:bitterharvest:20161105091506p:plain

シングルトンは要素の数が一つだけの集合である。それでは、要素の数がゼロの集合はあるのだろうか。これは、数の議論に似ている。建物で、地面に接している階を、日本では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として用意しているが、有用性が高いことは言うまでもない。