
  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 the property of 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 | 
 38 | public export
 39 | sum : ComMonoid a => Bag a -> a
 40 | sum @{mon} = foldr (plus mon) (neutral mon)
 41 | 
 42 | 
 43 | namespace NotExposingType
 44 |   ||| Same as ComMonoid, but without exposing the underlying carrier in the type
 45 |   public export
 46 |   ComMonoid : Type
 47 |   ComMonoid = (t : Type ** ComMonoid t)
 48 | 
 49 |   ||| Not encoding the rules for now
 50 |   public export
 51 |   ComMonoidHomo : ComMonoid -> ComMonoid -> Type
 52 |   ComMonoidHomo (t ** _) (t' ** _) = t -> t'
 53 | 
 54 |   -- public export
 55 |   -- record ComMonoidHomo (c, d : ComMonoid) where
 56 |   --   constructor MkComMonoidHomo
 57 |   --   underlyingMap : c.fst -> d.fst
 58 |   --   plusPreserve : (x, y : c.fst) ->
 59 |   --     underlyingMap (c.snd.plus x y) = d.snd.plus (underlyingMap x) (underlyingMap y)
 60 |   --   neutralPreserve : underlyingMap c.snd.neutral = d.snd.neutral
 61 |