Sketch of algebraic laws property testing, using explicit encoding for typeclass instances

laws-testing.u

-- Sketch of algebraic laws property testing, using explicit encoding for typeclass instances (Unison language)

type base.Monoid a = {
  mempty : a,
  mplus : a -> a -> a
}

type base.Monoid.Laws a = {
  leftIdentity : Monoid a -> a -> Boolean,
  rightIdentity : Monoid a -> a -> Boolean,
  associativity : Monoid a -> a -> a -> a -> Boolean
}

base.Monoid.laws : forall a . Monoid.Laws a
base.Monoid.laws =
  leftIdentity m a = (mplus m) (mempty m) a == a
  rightIdentity m a = (mplus m) a (mempty m) == a
  associativity m a b c = (mplus m) ((mplus m) a b) c == (mplus m) a ((mplus m) b c)
  Monoid.Laws leftIdentity rightIdentity associativity

base.monoid.laws.test : Weighted a -> Monoid a -> Monoid.Laws a -> [Test]
base.monoid.laws.test _ = todo "prop test using base.Monoid.laws"

-- example:

-- Note how the testing for each instance is just a single term, which is a one-liner
base.mything.tests.monoid = base.monoid.laws.test myweighted mything.interfaces.monoid

base.mything.interfaces.monoid = Monoid 0 (+)
myweighted = Weighted.nats