
  0 | module Data.ComMonoid
  1 | 
  2 | %hide Prelude.Semigroup
  3 | %hide Prelude.Monoid
  4 | 
  5 | ||| Commutative monoid
  6 | ||| Not encoding the property of commutativity here
  7 | public export
  8 | record ComMonoid (a : Type) where
  9 |   constructor MkComMonoid
 10 |   plus : a -> a -> a
 11 |   neutral : a
 12 | 
 13 | %hint
 14 | public export
 15 | doubleIsMonoid : ComMonoid Double
 16 | doubleIsMonoid = MkComMonoid (+) 0
 17 | 
 18 | %hint
 19 | public export
 20 | unitIsMonoid : ComMonoid Unit
 21 | unitIsMonoid = MkComMonoid (\(), () => ()) ()
 22 | 
 23 | %hint
 24 | public export
 25 | numIsMonoid : Num a => ComMonoid a
 26 | numIsMonoid = MkComMonoid (+) 0
 27 | 
 28 | public export
 29 | listIsMonoid : ComMonoid (List a)
 30 | listIsMonoid = MkComMonoid (++) []
 31 | 
 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 | 
 42 | public export
 43 | sum : ComMonoid a => List a -> a
 44 | sum @{mon} = foldr (plus mon) (neutral mon)
 45 | 
 46 | 
 47 | namespace NotExposingType
 48 |   ||| Same as ComMonoid, but without exposing the underlying carrier in the type
 49 |   public export
 50 |   ComMonoid : Type
 51 |   ComMonoid = (t : Type ** ComMonoid t)
 52 | 
 53 |   public export
 54 |   record ComMonoidHomo (c, d : ComMonoid) where
 55 |     constructor MkComMonoidHomo
 56 |     underlyingMap : c.fst -> d.fst
 57 |     plusPreserve : (x, y : c.fst) ->
 58 |       underlyingMap (c.snd.plus x y) = d.snd.plus (underlyingMap x) (underlyingMap y)
 59 |     neutralPreserve : underlyingMap c.snd.neutral = d.snd.neutral
 60 |