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