Chapter 23

5.2 終対象

さのたけと
さのたけと
2021.05.20に更新

単一の対象のパターンについて,今度は対象の順序付けの方法を変えて考えてみよう.対象 b から a への射がある場合に,ab よりも終であるとする(向きが始対象の時と逆であることに注意).圏の他のどの対象よりも終である対象を見つけよう.

終対象 (terminal object)は圏の全ての対象からの射を持つ対象である.

すぐに示すが,終対象は同型を除いて一意である.だが先にいくつかの例をみておこう.半順序集合では終対象はもし存在するならその最大要素である.集合のなす圏では,終対象は単集合である.これはC++ではvoid型に,Haskellでは単位型()に対応する.C++の方は暗に,Haskellの方は陽に()で示される一つの値のみを持つ型である.以前示したように,任意の型から単位型への純粋関数が唯一存在するので,単位型は終対象の全ての条件を満たす.

unit :: a -> ()
unit _ = ()

この例においては,全ての集合からの射を持つ他の集合(実は空集合以外の全ての集合がそのような性質を持つ)も存在するため,一意性の条件が不可欠であることに注意して欲しい.例えば,全ての型に対して定義されたブール値関数がそうである.

yes :: a -> Bool
yes _ = True

しかしBoolは終対象ではない.少なくとももう一つの,(Voidを除く)全ての型からBool値への関数が存在するため,これらの関数はabsurdである.

no :: a -> Bool
no _ = False

一意性によって終対象の定義を一つの型のみに絞ることができる.

(和訳:@dshin)