Category
Menu
型の理論と論理
これまで、関数型プログラミングでは、型から型への矢印として関数が存在する、そして、そのカーリハワード対応として、論理式から論理式への矢印としての推論が存在するということを学んできた。今度は、この論理系自体を論理的に扱いたい。そこで、集合と写像、項と関数、そして、論理式と推論自体を表す数学的構造を作る。これは圏と呼ばれる。
ここで、型や論理式を対象(object)と呼ぶ。関数や推論を射(arrow)と呼ぶ。対象は型なので集合。aからbへの射の集合をHom a bと呼ぶ。射は集合aから集合b への写像(mapping)でもある。ある型aから、ある型bへの関数はたくさん存在する。関数fは、その一つである。つまり、型aから型bへの関数全体の集合の要素になる。
この時に、
型aから型aへの恒等射(id a)がある
型a,b,cと、二つの射 f: a ->b, g: b-> c があった時、その合成 g ○ f がある
id a ○ f ≡ f と f ○ id a ≡ f が成り立つ
関数の合成○に関する結合法則 f ○ (g ○ h) ≡ (f ○ g) ○ h が成立
が成立するなら、この対象と射の組を圏(Category)と呼ぶ。
Cの対象の集合を Obj C と書く
Cのaからbへの射の集合を Hom C a bと書く
ここで出てきた等号は、Agdaで使ったもので、
f = f (反射律 refl )
f = g → g = f (対象律 sym )
f = g → g = h → f = h (推移律 trans )
射から射への関数 h がある時に、
f = g → h g = h f (合同律 cong )
を使うことがある。
record を使った圏の定義
Agda では数学的構造を record で作ることができる。必要とされるもの(input)
構造で提供されるもの(output)
構造が満たす論理式 (axiom)
axiom を別な record として用意することにより、この三つを構文的に区別できる。
stdalone-kleisli.agda Categoryというmoduleは既に用意されていたりするので、ここでは別な名前を使う。
record Category {l : Level} : Set (suc (suc l)) where
field
Obj : Set (suc l)
Hom : Obj → Obj → Set l
_o_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c
id : ( a : Obj ) → Hom a a
isCategory : IsCategory Obj Hom _o_ id
ここで対象(Obj)と射(Hom)、そして、射の合成(f o g)、恒等射idが型として定義されている。
isCategory には圏が満たす公理を記述する。
record IsCategory {l : Level} ( Obj : Set (suc l) ) (Hom : Obj → Obj → Set l )
( _o_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c )
( id : ( a : Obj ) → Hom a a )
: Set (suc l) where
field
idL : { a b : Obj } { f : Hom a b } → ( id b o f ) ≡ f
idR : { a b : Obj } { f : Hom a b } → ( f o id a ) ≡ f
assoc : { a b c d : Obj } { f : Hom c d }{ g : Hom b c }{ h : Hom a b } → f o ( g o h ) ≡ ( f o g ) o h
ここではAgadの _≡_ をそのまま使っているが、これ以外の関係を集合として導入する場合もある。
集合と写像ののCategory
恒等写像は、
id : {A : Set} -> A -> A
id x = x
と書くことができる。
射には等式が入っていて、≡ を data で定義(あるいは import Relation.Binary.Core すれば) f ≡ f、f ≡ g -> g ≡ f 、f ≡ g -> g ≡ h -> f ≡ h が成立している。
写像がすべての入力に対して値が等しい時に写像自体が等しいというのは Agda 自体では証明できないので仮定する必要がある。仮定には postulate を使う。
{A : Set c₁ } {B : Set c₂ } → { f g : A → B } → (x : A ) → f x ≡ g x → f ≡ g
これは前もって定義されているので、それを使う。
postulate extensionality : { c₁ c₂ : Level} → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
射の合成は、
_○_ : { A B C : Set} -> ( g : B -> C ) -> ( f : A -> B ) -> A -> C
g ○ f = \x -> g ( f x )
と定義する。
f ○ ( g ○ h ) ≡ ( f ○ g ) ○ h
を自分で証明する。これで圏を作ることができた。
Sets : Category
Sets = record {
Obj = Set
; Hom = λ a b → a → b
; _o_ = λ f g x → f ( g x )
; id = λ A x → x
; isCategory = record {
idL = ?
; idR = ?
; assoc = ?
}
}
実際に、圏のrecord を構成することにより、集合と写像が圏を構成することがわかった。
圏を導入する時には、record Category を作る。作る時に、idL や assoc の証明を与える必要がある(Introduction)。
逆に record Category を仮定すれば、idL とか assoc とかは自由に使える。(Elimination)。
問題 5.1
(f ○ g ) ○ h ≡ f ○ ( g ○ h )
などを Agda で証明して、上の Sets の ? をすべて埋めよ。
Category の例としての Monoid
Monoid は、集合T 上の結合律を満たす演算* と単位元1 からなる。
a * (b * c) = (a * b ) * c
1 * a = a
a * 1 = a
となる。このような演算を持つ T を Monoid と言う。
Monoidは対象が一つしかない圏である。
Haskell だったら、
class Monoid a where
mempty :: a -- 単位元 1
mappend :: a -> a -> a -- 演算 *
となる。
data MyList a = Nil
| Cons a (MyList a)
deriving (Show, Eq)
myAppend Nil t = t
myAppend (Cons h t ) t1 = Cons h ( myAppend t t1 )
instance Monoid MyList a where
mempty = Nil
mappend = myAppend
Haskell での Monoid
Monoid は対象が要素一つの集合な圏である。List がMonoid として圏を作ることを示そう。まず、Agda で List を定義する。
data List {l : Level} (A : Set l ) : Set l where
[] : List A
_::_ : A → List A → List A
data One {l : Level} : Set l where
* : One
append : { A : Set } → List A → List A → List A
append [] x = x
append (x :: y ) z = x :: append y z
次に Category の record を作ろう。
open import Relation.Binary.PropositionalEquality hiding ([_])
-- cong : {l l' : Level} {A : Set l} {B : Set l'} { x y : A } ( f : A → B ) → x ≡ y → f x ≡ f y
-- cong _ refl = refl
ListMonoid : (A : Set) → Category
ListMonoid A = record {
Obj = One
; Hom = λ a b → List A
; _o_ = λ f g → append f g
; id = λ A → []
; isCategory = record {
idL = ?
; idR = λ {a} {b} {f} → idR {a} {b} f
; assoc = λ {a} {b} {c} {d} {f} {g} {h} → assoc {a} {b} {c} {d} f g h
}
} where
idR : {a b : One {suc zero}} (f : List A) → append f [] ≡ f
idR [] = ?
idR {a} {b} (x :: y ) = ?
assoc : {a b c d : One {suc zero} } (f g h : List A) →
append f (append g h) ≡ append (append f g) h
assoc [] x y = ?
assoc {a} {b} {c} {d} (h :: t ) x y = ?
右単位元と左単位元、そして結合法則を証明して、上の定義を完成させよう。
関手 (Functor)
Haskell に出てくるFunctorは、圏から圏への射として定義される。Haskell では、以下のように定義されていた。
class Functor f where
fmap :: (a->b) -> f a -> f b
data Nodes a = Node a (Nodes a) (Nodes a)
| Leaf a
deriving (Show)
instance Functor Nodes where
fmap f (Leaf a ) = Leaf (f a)
fmap f (Node v a b ) = Node (f v) (fmap f a) (fmap f b)
データ構造、例えば Lias a で、 A の対象a, b に対して関数 f : a -> b があるとき、
fmap : ( a → b ) → List a → List b
が定義されているのが functor だった。 a → b は Hom Sets a b であり、 List a → List b は Hom Sets (List a) (List b) である。
圏には対象と射があるから、圏から圏への射は二つの写像を持つ。さらに、 単位元の保存、
fmap id = id
と、分配法則、
fmap (f ○ g ) = (fmap f ) ○ (fmap g)
を要求しよう。
T はFunctor で、対象aの行き先をTaと書く。射fの行き先をTfと書く。この時にTの二つの写像を同じTを使って表すようである。これはプログラム言語での多相関数(polymorphic function)と同じである。
F(f)
F(a) ------------> F(b)
record で記述すると、
record Functor {l : Level} (domain codomain : Category {l} )
: Set (suc l) where
field
FObj : Obj domain → Obj codomain
FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B)
isFunctor : IsFunctor domain codomain FObj FMap
のようになる。関数の入力の集合を domain 、出力の集合を codomain と呼ぶ。関手が満たす規則は以下のようになる。ここで、複数の圏の演算を区別しなければならないので、
_[_o_] : {l : Level} (C : Category {l} ) → {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
C [ f o g ] = Category._o_ C f g
を使う。
record IsFunctor {l : Level} (C D : Category {l} )
(FObj : Obj C → Obj D)
(FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B))
: Set (suc l ) where
field
identity : {A : Obj C} → FMap (id C A) ≡ id D (FObj A)
distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
→ FMap ( C [ g o f ]) ≡ (D [ FMap g o FMap f ] )
例えば、
fmap : {a b : Set} -> ( a -> b ) -> List -> List b
fmap _ [] = []
fmap f (x :: y) = (f x ) :: (fmap f y )
として定義すると、fmap {a} {b} は、f : a -> b から、List a -> List b の関数を生成している。
ここで、F(a) は、List a に対応する。F(f) は、fmap f を表す。F(a) と F(f) は違う関数であるが、圏論の本では同じ記号を使うのが普通なようである。(polymorphism)
単位元の保存、分配法則が成立しているかどうかを確かめて Functor の reocord を作ろう。
ListFunctor : Functor Sets Sets
ListFunctor = record {
FObj = λ x → List x
; FMap = fmap
; isFunctor = record {
identity = extensionality {zero} {zero} ( λ x → identity x )
; distr = λ {a} {b} {c} {f} {g} → extensionality {zero} {zero} ( λ x → distr x )
}
} where
fmap : {A B : Obj Sets} → Hom Sets A B → Hom Sets (List A) (List B)
fmap f [] = []
fmap f (x :: y) = ( f x ) :: fmap f y
identity : {A : Obj Sets} → ( x : List A ) → fmap (id Sets A) x ≡ id Sets (List A) x
identity {A} [] = refl
identity {A} (h :: t) = ?
distr : {a b c : Obj Sets} {f : Hom Sets a b} {g : Hom Sets b c} → (x : List a) → fmap (Sets [ g o f ]) x ≡ (Sets [ fmap g o fmap f ]) x
distr [] = ?
distr {a} {b} {c} {f} {g} (h :: t ) = let open ≡-Reasoning in begin
fmap (Sets [ g o f ]) (h :: t)
≡⟨ ? ⟩
(Sets [ fmap g o fmap f ]) (h :: t)
∎
関手は FObj が決まると、FMap が自然にただ一つ決まるという性質がある。これはFree Theoremから証明されるが Free Theorem は Agda では証明できない。
問題5.2
上の ? を埋めて、ListFunctor の定義を完成させよ。
Cat
Functor は圏から圏への矢印であり、恒等射と結合法則を満たす。
idFunctor : {l : Level } { C : Category {l} } → Functor C C
idFunctor = record {
FObj = λ x → x
; FMap = λ f → f
; isFunctor = record {
identity = refl
; distr = refl
}
}
Functor の合成は以下のように作ることができる。
_●_ : {l : Level} { A B C : Category {l} } → ( S : Functor B C ) ( T : Functor A B ) → Functor A C
_●_ {l} {A} {B} {C} S T = record {
FObj = λ x → FObj S ( FObj T x )
; FMap = λ f → FMap S ( FMap T f )
; isFunctor = record {
identity = λ {a} → identity a
; distr = λ {a} {b} {c} {f} {g} → distr
}
} where
identity : (a : Obj A) → FMap S (FMap T (id A a)) ≡ id C (FObj S (FObj T a))
identity a = let open ≡-Reasoning in begin
FMap S (FMap T (id A a))
≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.identity (isFunctor T ) ) ⟩
FMap S (id B (FObj T a) )
≡⟨ IsFunctor.identity (isFunctor S ) ⟩
id C (FObj S (FObj T a))
∎
distr : {a b c : Obj A} { f : Hom A a b } { g : Hom A b c } → FMap S (FMap T (A [ g o f ])) ≡ (C [ FMap S (FMap T g) o FMap S (FMap T f) ])
distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin
FMap S (FMap T (A [ g o f ]))
≡⟨ cong ( λ z → FMap S z ) ( IsFunctor.distr (isFunctor T ) ) ⟩
FMap S ( B [ FMap T g o FMap T f ] )
≡⟨ IsFunctor.distr (isFunctor S ) ⟩
C [ FMap S (FMap T g) o FMap S (FMap T f) ]
∎
すると、圏を対象とし、Functorを射とする圏の圏を作ることができる。これをCatという。
残念ながら、射の等しさを ≡ で定義すると、Functor の等しさを示すのが複雑になる。なので恒等射と結合則を示すことはしない。等式の定義に別な方法を使うと Cat を定義することができる。
Natural Transformation 自然変換
A から B へのFunctor F,G があるとする。ここでは、Functor は List や Node の constructor だと思って良い。
a -> Node a
data Nodes a = Node (Nodes a) (Nodes a)
| Leaf a
deriving (Show)
ここでは、Tree a から List a への変換を考える。例えば、
flatten n = case n of
Node v s t -> (flatten s)++[v]++(flatten t)
Leaf v -> [v]
これは、Treeを平坦なListに展開する。
同じ型から Functor がF,G と二つ定義されていた時に、F(a) の型から G(a) の型への射 t(a) があって、元の型上の射、関数 f: a->b があった時に、以下の可換図が成立するとする。
その時に、t を F から G への自然変換(natural transformation) という。F(b) から G(b) への射は複数あったり、なかったりするが、その中の一つを取ると一つ自然変換が決まる。
record NTrans {l : Level} {domain codomain : Category {l} } (F G : Functor domain codomain )
: Set (suc l) where
field
TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
isNTrans : IsNTrans domain codomain F G TMap
record IsNTrans { l : Level } (D C : Category {l} ) ( F G : Functor D C )
(TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
: Set (suc l) where
field
commute : {a b : Obj D} {f : Hom D a b}
→ C [ ( FMap G f ) o ( TMap a ) ] ≡ C [ (TMap b ) o (FMap F f) ]
List から Nodes への自然変換
flatten は、Nodes を List へ変換する。show は Integer から String への変換である。
fmap show ( flatten x )
と
flatten ( fmap show x )
は同じ結果を与える。
ここで、flatten の型は、型変数によって、
flatten : Nodes Integer -> List Integer
flatten : Nodes String -> List String
のに種類になっている。
show 以外の任意の関数でも、flatten 型が対応して同じ等式がなりたつ。
問題5.3
data Tree (A : Set ) : Set where
Leaf : A → Tree A
Node : A → Tree A → Tree A → Tree A
に対して、既に定義されているTreeFunctor に対して、
flatten : {A : Set} → Tree A → List A
flatten ( Leaf a ) = a :: []
flatten ( Node a left right ) = append (flatten left ) ( append ( a :: [] ) (flatten right ))
が自然変換であることを record NTrans を作ることにより示せ。
Tree→List : NTrans TreeFunctor ListFunctor
Tree→List = record {
TMap = λ a x → flatten {a} x
; isNTrans = record {
commute = extensionality {zero} ( λ x → commute x )
}
} where
commute : {a b : Obj Sets} {f : Hom Sets a b} ( x : Tree a )
→ (Sets [ FMap ListFunctor f o flatten ]) x ≡ (Sets [ flatten o FMap TreeFunctor f ]) x
commute = ?
いろんな自然変換
片方が1の場合。1 というは、a の上の恒等射。つまり、a から a へ変換する関手 idFunctor である。
T -> 1 の場合。これは、データ型から要素を取り出す操作に対応する。
NTrans T idFunctor
である。
List の先頭要素を返す head を考えよう。Integer 上の fmap は fmap f x = f x と考えれば良い。
fmap show ( head x ) = head ( fmap show x )
これは、head : 1_Integer -> List String という自然変換になっている。( x が [] の時には、どう考えれば良いか? )
1 -> T の場合。これはデータ型を作る Constructor に相当する。
同じ要素を n 個並べた List を作る関数 nlist を考えよう。
fmap show ( nlist 5 x ) = nlist 5 ( fmap show x )
TT -> T の場合
これは同じ型が入れ子になっているものの入れ子を解消するものになっている。TT(a) は T(T(a)) のこと。
NTrans (T ● T) T
である。
List ( List Integer ) を考えよう。flatten は、自然変換になっている。この場合、TT(f) は Nest した List のみに働く必要がある。
T(f) => fmap f
TT(f) => fmap (fmap f)
行列の行列式を求める関数は、どのような Functor の自然変換になっているか考えよう。可能な射fは行列の線形変換に限定する必要がある。
natural transformation であることを証明する
Agda を用いて、nlist が natural transformation であることを示そう。
fmap f ( nlist h n ) ≡ nlist ( f h ) nを示せば良い。
関手と自然変換の結合
T : A → A な関手、η : 1 → T な自然変換を考えよう。ここでAの対象は型だが、T a という型も含んでいるとする。T を List だとすると、 η(Integer)は、Integer の List を返す関数。例えば、1 を [1] にする。TT は、List の List になる。
Tηは、T(η(a)) で、η(a) は射。ここでの T は射の写像を表す。それは List の fmap だった。これは、T から TT への自然変換になる。
Tη : T → TT
ηが nlist だったら、
Tη = fmap (nlist)
になる。これは、自然変換になっている。つまり、
が成立する。
TT(f)Tη(a) = fmap (fmap f) ( fmap nlist )
Tη(b)T(f) = fmap nlist ( fmap f )
ηT
η : T → 1T は、η(T(a)) で、T(a) はAの対象になる。η(T(a)) は a 上の射になる。
ηT : TT → T
ηが head だったら、
ηT = λ ( x : List ( List a ) ) → head x
になる。これは自然変換で、
が成立する。
T(f) η(T(a)) = λ (x : TT ) → fmap f (head x )
ηT(b)TT(f) = λ (x : TT ) → head (fmap (fmap f) x)
まとめ
圏は、関数とその型の性質だけと取り出したもの。あるいは、推論規則と式の性質を取り出したもの。
Functor (関手) は、型変数を持つデータ構造、fmap がある。
Functor (関手) は、
型変数aからデータ構造F(a) を作る写像(constructor)
f : a -> b を F(a) -> F(b) に対応させる写像 (fmap)
の二つの写像からなる。
Functor は圏から圏への射になっていて、圏の集まりは圏(Cat)になる
自然変換t は、Functor : A -> F からFunctor : A -> G への写像、つまりデータ構造からデータ構造への変換である。
自然変換には可換性が要求されている。
自然変換とFunctorの組み合わせは自然変換になる。