-
Notifications
You must be signed in to change notification settings - Fork 1
/
P3Ch15b_CatsAsMonads.lhs
129 lines (104 loc) · 3.83 KB
/
P3Ch15b_CatsAsMonads.lhs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|Markdown version of this file: https://github.com/rpeszek/notes-milewski-ctfp-hs/wiki/N_P3Ch15b_CatsAsMonads
"So, all told, a category is just a monad in the bicategory of spans."
This note traces that statement using simple category `A->B=>C` from [N_P1Ch03b_FiniteCats (FC)](N_P1Ch03b_FiniteCats)
and Haskell.
> {-# LANGUAGE DataKinds
> , KindSignatures
> , GADTs
> #-}
> {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
>
> module CTNotes.P3Ch15b_CatsAsMonads where
> import qualified CTNotes.P1Ch03b_FiniteCats as FC
> import CTNotes.P1Ch03b_FiniteCats (Object(..))
> import CTNotes.P3Ch15a_Spans
> import Data.Proxy
Consider the category `A->B=>C` from [N_P1Ch03b_FiniteCats (FC)](N_P1Ch03b_FiniteCats) redefined here to follow
the notation from the book:
> type Ob = FC.Object
(Equivalently FC.ObjectRep could been used instead.)
Type `Ar` is isomorphic to `FC.HS` (to be precise, to the flattened version `HomSetFlat` shown below)
and marks domains and codomains using data constructors
> data Cod (a :: FC.Object) = CodA (FC.HS a 'A) | CodB (FC.HS a 'B) | CodC (FC.HS a 'C)
>
> data Ar = DomA (Cod 'A) | DomB (Cod 'B) | DomC (Cod 'C)
>
> decCod :: Cod a -> Ob
> decCod (CodA _) = FC.A
> decCod (CodB _) = FC.B
> decCod (CodC _) = FC.C
>
> dec :: Ar -> (Ob, Ob)
> dec (DomA x) = (FC.A, decCod x)
> dec (DomB x) = (FC.B, decCod x)
> dec (DomC x) = (FC.C, decCod x)
>
> dom :: Ar -> Ob
> dom = fst . dec
>
> cod :: Ar -> Ob
> cod = snd . dec
The book defines the 1-cell span `Ob <- Ar -> Ob` (monad `T`) as something that I would like to express as
> t :: Cell1 Ar Ob Ob
> t = Cell1 dom cod
and the 1-cell `I` as the identity cell
> i :: Cell1 Ob Ob Ob
> i = Cell1 id id
For `t` to be a monad I need to define two 2-cells
```
η :: I -> T
μ :: T ∘ T -> T
```
Translating this to the `data Cell2 x y a b = Cell2 (x -> y)` from [N_P3Ch15a_Spans](N_P3Ch15a_Spans)
```
η :: I -> T
Ob
/ | \
/id |η \id
/ | \
Ob <- Ar -> Ob
```
> eta :: Cell2 Ob Ar Ob Ob
> eta =
> let pickId :: Ob -> Ar
> pickId A = DomA (CodA (FC.MoId FC.ARep))
> pickId B = DomB (CodB (FC.MoId FC.BRep))
> pickId C = DomC (CodC (FC.MoId FC.CRep))
> in Cell2 pickId
2-cell `μ :: T ∘ T -> T` defines the composition and translates to
```
mu :: Pullback Ar Ar Ob -> Ar
```
Due to complexity of describing pullback in a programming language, [N_P3Ch15a_Spans](N_P3Ch15a_Spans)
has used existential type
```
data Pullback x y a = forall z . Pullback z (z -> x) (z -> y)
```
that is not trivial to work with.
However, for this simple example, I can just define pullback explicitly.
That type should consist of composable pairs of 1-cells.
> data PullbackForAr where
> OnA :: FC.HS 'A 'A -> FC.HS 'A a -> PullbackForAr
> OnB :: FC.HS a 'B -> FC.HS 'B c -> PullbackForAr
> OnC :: FC.HS a 'C -> FC.HS 'C 'C -> PullbackForAr
`mu :: PullbackForAr -> Ar` can be defined by repeating the definition of `FC.comp`.
However, I can do better and use GHC to check that `mu` is just the composition
in disguise:
> data HomSetFlat where
> HsFlat :: (FC.HS a b) -> HomSetFlat
>
> mu :: PullbackForAr -> Ar
> mu (OnA m1 m2) = iso . HsFlat $ m2 `FC.comp` m1
> mu (OnB m1 m2) = iso . HsFlat $ m2 `FC.comp` m1
> mu (OnC m1 m2) = iso . HsFlat $ m2 `FC.comp` m1
and the tedious part is the definition of `iso`
> iso :: HomSetFlat -> Ar
> iso (HsFlat (FC.MoId FC.ARep)) = DomA (CodA (FC.MoId FC.ARep))
> iso (HsFlat (FC.MoId FC.BRep)) = DomB (CodB (FC.MoId FC.BRep))
> iso (HsFlat (FC.MoId FC.CRep)) = DomC (CodC (FC.MoId FC.CRep))
> iso (HsFlat FC.MoAB) = DomA (CodB FC.MoAB)
> iso (HsFlat FC.MoBC1) = DomB (CodC FC.MoBC1)
> iso (HsFlat FC.MoBC2) = DomB (CodC FC.MoBC2)
> iso (HsFlat FC.MoAC1) = DomA (CodC FC.MoAC1)
> iso (HsFlat FC.MoAC2) = DomA (CodC FC.MoAC2)
"So, all told, a category is just a monad in the bicategory of spans." in Haskell!