0 | module Data.ComMonoid
 1 |
 2 | import public Data.Num
 3 | import public Data.Bag
 4 |
 5 | %hide Prelude.Semigroup
 6 | %hide Prelude.Monoid
 7 |
 8 | ||| Commutative monoid
 9 | ||| Not encoding monoid laws, nor commutativity here
10 | public export
11 | record ComMonoid (a : Type) where
12 |   constructor MkComMonoid
13 |   plus : a -> a -> a
14 |   neutral : a
15 |
16 | ||| Every `Num` type is a commutative monoid under addition.
17 | ||| Deliberately `export` and not `public export`, as it complicates search
18 | ||| It spawns a witness for every `Const a` with numeric `a`
19 | %hint
20 | export
21 | numIsMonoid : Num a => ComMonoid a
22 | numIsMonoid = MkComMonoid (+) 0
23 |
24 | -- todo figure out a consistent strategy for when `%hint` is needed or not
25 | public export
26 | listIsMonoid : ComMonoid (List a)
27 | listIsMonoid = MkComMonoid (++) []
28 |
29 | public export
30 | bagIsMonoid : ComMonoid (Bag a)
31 | bagIsMonoid = MkComMonoid (++) (MkBag [])
32 |
33 | %hint
34 | public export
35 | pairIsMonoid : ComMonoid a => ComMonoid b => ComMonoid (a, b)
36 | pairIsMonoid @{MkComMonoid plusA neutralA} @{MkComMonoid plusB neutralB}
37 |   = MkComMonoid
38 |     (\(a, b), (a', b') => (plusA a a', plusB b b'))
39 |     (neutralA, neutralB)
40 |
41 | public export
42 | sum : ComMonoid a => Bag a -> a
43 | sum @{mon} = foldr (plus mon) (neutral mon)
44 |
45 | namespace NotExposingType
46 |   ||| Same as ComMonoid, but without exposing the underlying carrier in the type
47 |   public export
48 |   ComMonoid : Type
49 |   ComMonoid = (t : Type ** ComMonoid t)
50 |
51 |   ||| Forgetful functor
52 |   public export
53 |   uSet : ComMonoid -> Type
54 |   uSet = fst
55 |
56 |   ||| Not encoding the rules for now
57 |   ||| Not using pattern matching so it reduces
58 |   public export
59 |   ComMonoidHomo : ComMonoid -> ComMonoid -> Type
60 |   ComMonoidHomo m n = uSet m -> uSet n
61 |
62 |   ||| Hom object of commutative monoids 
63 |   ||| Notably, without commutativity this does not exist
64 |   public export
65 |   functionIsMonoid : {0 a : Type} -> ComMonoid b -> ComMonoid (a -> b)
66 |   functionIsMonoid m = MkComMonoid
67 |     (\f, g => \x => plus m (f x) (g x))
68 |     (\_ => neutral m)
69 |
70 |   ||| Natural numbers, the free commutative monoid on one generator.
71 |   public export
72 |   natMon : ComMonoid
73 |   natMon = (Nat ** numIsMonoid)
74 |
75 |   public export
76 |   Free : Type -> ComMonoid
77 |   Free a = (Bag a ** bagIsMonoid)
78 |
79 | ||| Hom-set isomorphism of the free-forgetful adjunction between ComMon and Set
80 | ||| A map on generators is extended to a homomorphism out of a free commtuative 
81 | ||| monoid on the generators
82 | public export
83 | fromGenerators : {0 a : Type} -> {y : ComMonoid} ->
84 |   (a -> uSet y) -> -- a map on generators
85 |   ComMonoidHomo (Free a) y
86 | fromGenerators f b = sum @{snd y} (f <$> b)
87 |
88 | ||| Canonical action of `Nat` on a commutative monoid
89 | ||| `scale n x` is the `n`-fold sum `x + ... + x`
90 | ||| Special case of `fromGenerators` whe `a=Unit`.
91 | public export
92 | scale : ComMonoid a => Nat -> a -> a
93 | scale @{mon} 0 a = neutral mon
94 | scale @{mon} (S k) a = plus mon a (scale k a)
95 |
96 |