Skip to content

Instantly share code, notes, and snippets.

@atacratic
Created May 3, 2020 10:38
Show Gist options
  • Save atacratic/65b7eae9fb397f6bc68752955bd81ad9 to your computer and use it in GitHub Desktop.
Save atacratic/65b7eae9fb397f6bc68752955bd81ad9 to your computer and use it in GitHub Desktop.
Sketch of algebraic laws property testing, using explicit encoding for typeclass instances
-- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment