Press n or j to go to the next uncovered block, b, p or k for the previous block.
| 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 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 | 1x 1x 1x 1x 1x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 13x 1x 1x 13x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x 26x | import {Law} from '#law'
import {Boolean as BO, Equivalence as EQ} from 'effect'
import type {OrderTypeLambda} from 'effect/Order'
import {
greaterThan,
greaterThanOrEqualTo,
lessThan,
lessThanOrEqualTo,
} from 'effect/Order'
import fc from 'fast-check'
import type {BuildConcrete} from './given.js'
import {defineConcreteLaws} from './given.js'
/**
* Build typeclass laws for `Order`.
* @category typeclass laws
*/
export const orderLaws: BuildConcrete<OrderTypeLambda> = ({
F,
a,
equalsA,
suffix,
}) => {
const build = buildLaws(a, equalsA),
[lt, gt, lte, gte] = [
lessThan(F),
greaterThan(F),
lessThanOrEqualTo(F),
greaterThanOrEqualTo(F),
]
const consistencyLaw = Law(
'order equals consistency',
`∀a,b ∈ T: a≤b ∧ b≥a ⇒ a=c`,
a,
a,
)((a, b) => BO.implies(lte(a, b) && gte(a, b), equalsA(a, b)))
return defineConcreteLaws('Order', consistencyLaw)(
suffix,
build('≤', lte, gt),
build('≥', gte, lt),
)
}
const buildLaws =
<A>(a: fc.Arbitrary<A>, equalsA: EQ.Equivalence<A>) =>
(
sym: string,
op: (a: A, b: A) => boolean,
complement: (a: A, b: A) => boolean,
) =>
defineConcreteLaws(
'Order',
Law(
'transitivity',
`a${sym}b ∧ b${sym}c ⇒ a${sym}c`,
a,
a,
a,
)((a, b, c) => BO.implies(op(a, b) && op(b, c), op(a, c))),
Law(
'antisymmetry',
`a${sym}b ∧ b${sym}a ⇒ a=b`,
a,
a,
)((a, b) => BO.implies(op(a, b) && op(b, a), equalsA(a, b))),
Law('reflexivity', `a${sym}a`, a)((a: A) => op(a, a)),
Law(
'connectivity',
`a${sym}b ∨ b${sym}a`,
a,
a,
)((a, b) => op(a, b) || op(b, a)),
Law(
'complement consistency',
`∀a,b ∈ T: a${sym}b ⇒ a${sym === '≤' ? '≯' : '≮'}b`,
a,
a,
)((a, b) => BO.implies(op(a, b), !complement(a, b))),
)(sym)
declare module './given.js' {
interface ConcreteLambdas {
Order: OrderTypeLambda
}
}
|