aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/monoid.lux
blob: 815cf8c4dabd64a3422e79449fd811ea7aa78a81 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
(.using
 [library
  [lux "*"
   ["_" test {"+" Test}]
   [abstract
    [monad {"+" do}]]
   [math
    ["[0]" random {"+" Random}]]]]
 [\\library
  ["[0]" /
   [//
    [equivalence {"+" Equivalence}]]]])

(def: .public (spec (open "_#[0]") (open "_#[0]") gen_sample)
  (All (_ a) (-> (Equivalence a) (/.Monoid a) (Random a) Test))
  (do random.monad
    [sample gen_sample
     left gen_sample
     mid gen_sample
     right gen_sample]
    (<| (_.for [/.Monoid])
        (all _.and
             (_.property "Left identity."
               (_#= sample
                    (_#composite _#identity sample)))
             (_.property "Right identity."
               (_#= sample
                    (_#composite sample _#identity)))
             (_.property "Associativity."
               (_#= (_#composite left (_#composite mid right))
                    (_#composite (_#composite left mid) right)))
             ))))