Milestone 0.2 documents this law but deliberately leaves systematic law - * verification to milestone 0.3.
- * * @param the value type */ @FunctionalInterface diff --git a/src/main/java/io/codeswarm/typeclasses/examples/EqExample.java b/src/main/java/io/codeswarm/typeclasses/examples/EqExample.java index a09b1e7..a54445e 100644 --- a/src/main/java/io/codeswarm/typeclasses/examples/EqExample.java +++ b/src/main/java/io/codeswarm/typeclasses/examples/EqExample.java @@ -16,7 +16,7 @@ private EqExample() { static void main() { final var alice30 = new Person("Alice", 30); final var alice40 = new Person("ALICE", 40); - System.out.println(EqFunctions.equal(alice30, alice40, PersonInstances.BY_ALL_FIELDS)); - System.out.println(EqFunctions.equal(alice30, alice40, PersonInstances.BY_NAME)); + System.out.println(EqFunctions.equal(alice30, alice40, PersonInstances.EQ_ALL_FIELDS)); + System.out.println(EqFunctions.equal(alice30, alice40, PersonInstances.EQ_NAME)); } } diff --git a/src/main/java/io/codeswarm/typeclasses/examples/OrdExample.java b/src/main/java/io/codeswarm/typeclasses/examples/OrdExample.java index cd5ab17..d4605e7 100644 --- a/src/main/java/io/codeswarm/typeclasses/examples/OrdExample.java +++ b/src/main/java/io/codeswarm/typeclasses/examples/OrdExample.java @@ -16,7 +16,7 @@ private OrdExample() { static void main() { final var alice = new Person("Alice", 35); final var bob = new Person("Bob", 27); - System.out.println(OrdFunctions.min(alice, bob, PersonInstances.BY_AGE)); - System.out.println(OrdFunctions.min(alice, bob, PersonInstances.BY_NAME_ORDER)); + System.out.println(OrdFunctions.min(alice, bob, PersonInstances.ORD_AGE)); + System.out.println(OrdFunctions.min(alice, bob, PersonInstances.ORD_NAME)); } } diff --git a/src/main/java/io/codeswarm/typeclasses/examples/PersonInstances.java b/src/main/java/io/codeswarm/typeclasses/examples/PersonInstances.java index 4a91d90..6fe5937 100644 --- a/src/main/java/io/codeswarm/typeclasses/examples/PersonInstances.java +++ b/src/main/java/io/codeswarm/typeclasses/examples/PersonInstances.java @@ -14,26 +14,26 @@ public final class PersonInstances { /** Compact representation containing only the person's name. */ - public static final ShowThe helpers return booleans so they can be used from both example-based + * JUnit tests and property-based jqwik tests without coupling the law model to + * a specific assertion library.
+ */ +public final class EqLaws { + + private EqLaws() { + throw new AssertionError("Law utility must not be instantiated"); + } + + /** + * Checks reflexivity: {@code a ~ a}. + * + * @param value tested value + * @param eq equality instance + * @param value type + * @return {@code true} when reflexivity holds for the supplied value + */ + public static boolean reflexive(final A value, final Eq eq) { + return eq.eqv(value, value); + } + + /** + * Checks symmetry: {@code a ~ b} iff {@code b ~ a}. + * + * @param left left value + * @param right right value + * @param eq equality instance + * @param value type + * @return {@code true} when symmetry holds for the supplied pair + */ + public static boolean symmetric(final A left, final A right, final Eq eq) { + return eq.eqv(left, right) == eq.eqv(right, left); + } + + /** + * Checks transitivity: when {@code a ~ b} and {@code b ~ c}, then + * {@code a ~ c} must also hold. + * + * @param first first value + * @param second second value + * @param third third value + * @param eq equality instance + * @param value type + * @return {@code true} when the transitivity implication holds + */ + public static boolean transitive( + final A first, + final A second, + final A third, + final Eq eq) { + return !(eq.eqv(first, second) && eq.eqv(second, third)) || eq.eqv(first, third); + } +} diff --git a/src/test/java/io/codeswarm/typeclasses/laws/MonoidLaws.java b/src/test/java/io/codeswarm/typeclasses/laws/MonoidLaws.java new file mode 100644 index 0000000..e4489e3 --- /dev/null +++ b/src/test/java/io/codeswarm/typeclasses/laws/MonoidLaws.java @@ -0,0 +1,66 @@ +package io.codeswarm.typeclasses.laws; + +import io.codeswarm.typeclasses.algebra.Monoid; +import io.codeswarm.typeclasses.core.Eq; + +/** + * Reusable executable laws for {@link Monoid} instances. + */ +public final class MonoidLaws { + + private MonoidLaws() { + throw new AssertionError("Law utility must not be instantiated"); + } + + /** + * Checks the inherited semigroup associativity law. + * + * @param first first value + * @param second second value + * @param third third value + * @param monoid monoid instance + * @param eq equality used to compare results + * @param value type + * @return {@code true} when associativity holds + */ + public static boolean associative( + final A first, + final A second, + final A third, + final Monoid monoid, + final Eq eq) { + return SemigroupLaws.associative(first, second, third, monoid, eq); + } + + /** + * Checks the left identity law: {@code empty <> a == a}. + * + * @param value tested value + * @param monoid monoid instance + * @param eq equality used to compare results + * @param value type + * @return {@code true} when left identity holds + */ + public static boolean leftIdentity( + final A value, + final Monoid monoid, + final Eq eq) { + return eq.eqv(monoid.combine(monoid.empty(), value), value); + } + + /** + * Checks the right identity law: {@code a <> empty == a}. + * + * @param value tested value + * @param monoid monoid instance + * @param eq equality used to compare results + * @param value type + * @return {@code true} when right identity holds + */ + public static boolean rightIdentity( + final A value, + final Monoid monoid, + final Eq eq) { + return eq.eqv(monoid.combine(value, monoid.empty()), value); + } +} diff --git a/src/test/java/io/codeswarm/typeclasses/laws/OrdLaws.java b/src/test/java/io/codeswarm/typeclasses/laws/OrdLaws.java new file mode 100644 index 0000000..889f758 --- /dev/null +++ b/src/test/java/io/codeswarm/typeclasses/laws/OrdLaws.java @@ -0,0 +1,77 @@ +package io.codeswarm.typeclasses.laws; + +import io.codeswarm.typeclasses.core.Ord; + +/** + * Reusable executable laws for {@link Ord} instances. + */ +public final class OrdLaws { + + private OrdLaws() { + throw new AssertionError("Law utility must not be instantiated"); + } + + /** + * Checks reflexivity of ordering: comparing a value with itself yields zero. + * + * @param value tested value + * @param ord ordering instance + * @param value type + * @return {@code true} when reflexivity holds + */ + public static boolean reflexive(final A value, final Ord ord) { + return ord.compare(value, value) == 0; + } + + /** + * Checks sign antisymmetry of comparison results. + * + * @param left left value + * @param right right value + * @param ord ordering instance + * @param value type + * @return {@code true} when reversing arguments reverses the comparison sign + */ + public static boolean signAntisymmetric( + final A left, + final A right, + final Ord ord) { + return Integer.signum(ord.compare(left, right)) == -Integer.signum(ord.compare(right, left)); + } + + /** + * Checks transitivity of the less-than-or-equal relation. + * + * @param first first value + * @param second second value + * @param third third value + * @param ord ordering instance + * @param value type + * @return {@code true} when the transitivity implication holds + */ + public static boolean transitive( + final A first, + final A second, + final A third, + final Ord ord) { + final boolean firstBeforeSecond = ord.compare(first, second) <= 0; + final boolean secondBeforeThird = ord.compare(second, third) <= 0; + return !(firstBeforeSecond && secondBeforeThird) || ord.compare(first, third) <= 0; + } + + /** + * Checks that {@link Ord#eqv(Object, Object)} agrees with zero comparison. + * + * @param left left value + * @param right right value + * @param ord ordering instance + * @param value type + * @return {@code true} when equality and comparison agree + */ + public static boolean consistentWithEquality( + final A left, + final A right, + final Ord ord) { + return ord.eqv(left, right) == (ord.compare(left, right) == 0); + } +} diff --git a/src/test/java/io/codeswarm/typeclasses/laws/SemigroupLaws.java b/src/test/java/io/codeswarm/typeclasses/laws/SemigroupLaws.java new file mode 100644 index 0000000..34fb691 --- /dev/null +++ b/src/test/java/io/codeswarm/typeclasses/laws/SemigroupLaws.java @@ -0,0 +1,36 @@ +package io.codeswarm.typeclasses.laws; + +import io.codeswarm.typeclasses.algebra.Semigroup; +import io.codeswarm.typeclasses.core.Eq; + +/** + * Reusable executable laws for {@link Semigroup} instances. + */ +public final class SemigroupLaws { + + private SemigroupLaws() { + throw new AssertionError("Law utility must not be instantiated"); + } + + /** + * Checks associativity of a semigroup operation. + * + * @param first first value + * @param second second value + * @param third third value + * @param semigroup semigroup instance + * @param eq equality used to compare both association results + * @param value type + * @return {@code true} when associativity holds for the supplied values + */ + public static boolean associative( + final A first, + final A second, + final A third, + final Semigroup semigroup, + final Eq eq) { + final A leftAssociated = semigroup.combine(semigroup.combine(first, second), third); + final A rightAssociated = semigroup.combine(first, semigroup.combine(second, third)); + return eq.eqv(leftAssociated, rightAssociated); + } +} diff --git a/src/test/java/io/codeswarm/typeclasses/laws/UnlawfulInstancesTest.java b/src/test/java/io/codeswarm/typeclasses/laws/UnlawfulInstancesTest.java new file mode 100644 index 0000000..23e0a01 --- /dev/null +++ b/src/test/java/io/codeswarm/typeclasses/laws/UnlawfulInstancesTest.java @@ -0,0 +1,30 @@ +package io.codeswarm.typeclasses.laws; + +import io.codeswarm.typeclasses.algebra.Semigroup; +import io.codeswarm.typeclasses.instances.IntegerInstances; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertFalse; + +/** + * Demonstrates that implementing a typeclass interface does not automatically + * make an instance lawful. + */ +class UnlawfulInstancesTest { + + /** + * Shows that integer subtraction is not associative and therefore cannot be + * a lawful {@link Semigroup} operation. + */ + @Test + void subtractionShouldFailAssociativity() { + final Semigroup