/
Semiring.purs
76 lines (57 loc) · 2.37 KB
/
Semiring.purs
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
module Test.QuickCheck.Laws.Data.Semiring where
import Prelude
import Effect (Effect)
import Effect.Console (log)
import Test.QuickCheck (quickCheck')
import Test.QuickCheck.Arbitrary (class Arbitrary)
import Type.Proxy (Proxy)
-- | - Commutative monoid under addition:
-- | - Associativity: `(a + b) + c = a + (b + c)`
-- | - Identity: `zero + a = a + zero = a`
-- | - Commutative: `a + b = b + a`
-- | - Monoid under multiplication:
-- | - Associativity: `(a * b) * c = a * (b * c)`
-- | - Identity: `one * a = a * one = a`
-- | - Multiplication distributes over addition:
-- | - Left distributivity: `a * (b + c) = (a * b) + (a * c)`
-- | - Right distributivity: `(a + b) * c = (a * c) + (b * c)`
-- | - Annihiliation: `zero * a = a * zero = zero`
checkSemiring
∷ ∀ a
. Semiring a
⇒ Arbitrary a
⇒ Eq a
⇒ Proxy a
→ Effect Unit
checkSemiring _ = do
log "Checking 'Associativity' law for Semiring addition"
quickCheck' 1000 associativeAddition
log "Checking 'Identity' law for Semiring addition"
quickCheck' 1000 identityAddition
log "Checking 'Commutative' law for Semiring addition"
quickCheck' 1000 commutativeAddition
log "Checking 'Associativity' law for Semiring multiplication"
quickCheck' 1000 associativeMultiplication
log "Checking 'Identity' law for Semiring multiplication"
quickCheck' 1000 identityMultiplication
log "Checking 'Left distribution' law for Semiring"
quickCheck' 1000 leftDistribution
log "Checking 'Right distribution' law for Semiring"
quickCheck' 1000 rightDistribution
where
associativeAddition ∷ a → a → a → Boolean
associativeAddition a b c = (a + b) + c == a + (b + c)
identityAddition ∷ a → Boolean
identityAddition a = (zero + a == a) && (a + zero == a)
commutativeAddition ∷ a → a → Boolean
commutativeAddition a b = a + b == b + a
associativeMultiplication ∷ a → a → a → Boolean
associativeMultiplication a b c = (a * b) * c == a * (b * c)
identityMultiplication ∷ a → Boolean
identityMultiplication a = (one * a == a) && (a * one == a)
leftDistribution ∷ a → a → a → Boolean
leftDistribution a b c = a * (b + c) == (a * b) + (a * c)
rightDistribution ∷ a → a → a → Boolean
rightDistribution a b c = (a + b) * c == (a * c) + (b * c)
annihiliation ∷ a → Boolean
annihiliation a = (a * zero == zero) && (zero * a == zero)