aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/monoid.lux
blob: fe69e9f6b5d19032f44b5b3fd74b1c1a2f5eca56 (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
33
(.require
 [library
  [lux (.except)
   [abstract
    [monad (.only do)]]
   [math
    ["[0]" random (.only Random)]]
   [test
    ["_" property (.only Test)]]]]
 [\\library
  ["[0]" / (.only)
   [//
    [equivalence (.only 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
             (_.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)))
             ))))