
  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 | %hint
 17 | public export
 18 | numIsMonoid : Num a => ComMonoid a
 19 | numIsMonoid = MkComMonoid (+) 0
 20 | 
 21 | public export
 22 | listIsMonoid : ComMonoid (List a)
 23 | listIsMonoid = MkComMonoid (++) []
 24 | 
 25 | public export
 26 | bagIsMonoid : ComMonoid (Bag a)
 27 | bagIsMonoid = MkComMonoid (++) (MkBag [])
 28 | 
 29 | %hint
 30 | public export
 31 | pairIsMonoid : ComMonoid a => ComMonoid b => ComMonoid (a, b)
 32 | pairIsMonoid @{MkComMonoid plusA neutralA} @{MkComMonoid plusB neutralB}
 33 |   = MkComMonoid
 34 |     (\(a, b), (a', b') => (plusA a a', plusB b b'))
 35 |     (neutralA, neutralB)
 36 | 
 37 | public export
 38 | sum : ComMonoid a => Bag a -> a
 39 | sum @{mon} = foldr (plus mon) (neutral mon)
 40 | 
 41 | -- public export
 42 | -- ComMonoidHomo : {a, b : Type} -> ComMonoid a -> ComMonoid b -> Type
 43 | -- ComMonoidHomo _ _ = a -> b
 44 | 
 45 | 
 46 | namespace NotExposingType
 47 |   ||| Same as ComMonoid, but without exposing the underlying carrier in the type
 48 |   public export
 49 |   ComMonoid : Type
 50 |   ComMonoid = (t : Type ** ComMonoid t)
 51 | 
 52 |   public export
 53 |   uSet : ComMonoid -> Type
 54 |   uSet = fst
 55 | 
 56 |   ||| Not encoding the rules for now
 57 |   public export
 58 |   ComMonoidHomo : ComMonoid -> ComMonoid -> Type
 59 |   ComMonoidHomo (t ** _) (t' ** _) = t -> t'
 60 | 
 61 |   -- public export
 62 |   -- record ComMonoidHomo (c, d : ComMonoid) where
 63 |   --   constructor MkComMonoidHomo
 64 |   --   underlyingMap : c.fst -> d.fst
 65 |   --   plusPreserve : (x, y : c.fst) ->
 66 |   --     underlyingMap (c.snd.plus x y) = d.snd.plus (underlyingMap x) (underlyingMap y)
 67 |   --   neutralPreserve : underlyingMap c.snd.neutral = d.snd.neutral
 68 | 
 69 | ||| One way of the hom-set isomorphism of the free-forgetful adjunction. It 
 70 | ||| extends a map on generators to a homomorphism out of the free commutative
 71 | ||| monoid on those generators.
 72 | public export
 73 | fromGenerators : {0 a : Type} -> (mon : ComMonoid y) => (a -> y) ->
 74 |   ComMonoidHomo (Bag a ** bagIsMonoid {a}) (y ** mon)
 75 | fromGenerators h = sum . map h
 76 | 
 77 | ||| Canonical action of `Nat` on a commutative monoid
 78 | ||| `scale n x` is the `n`-fold sum `x + ... + x`
 79 | ||| The one-generator case of `fromGenerators`, with `Nat \cong Bag Unit`
 80 | public export
 81 | scale : ComMonoid a => Nat -> a -> a
 82 | scale @{mon} 0 a = neutral mon
 83 | scale @{mon} (S k) a = plus mon a (scale k a)
 84 | 
 85 |