aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/monoid.lux
blob: c3857dbbb229d65871f591e7a8db58040ca2387c (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])
        ($_ _.and
            (_.test "Left identity."
                    (_#= sample
                         (_#composite _#identity sample)))
            (_.test "Right identity."
                    (_#= sample
                         (_#composite sample _#identity)))
            (_.test "Associativity."
                    (_#= (_#composite left (_#composite mid right))
                         (_#composite (_#composite left mid) right)))
            ))))