algebra-checkers: Model and test API surfaces algebraically

[ bsd3, library, model ] [ Propose Tags ]

Please see the README on GitHub at https://github.com/isovector/algebra-checkers#readme


[Skip to Readme]
Versions [faq] 0.1.0.0
Change log ChangeLog.md
Dependencies ansi-terminal (>=0.10.3), base (>=4.7 && <5), checkers (>=0.5.5), containers (>=0.5.10.2), groups (>=0.4.1.0), mtl (>=2.2.2 && <3), pretty (>=1.1.3.3 && <2), QuickCheck (>=2.10.1 && <3), syb (>=0.7), template-haskell (>=2.12.0.0 && <3), th-instance-reification (>=0.1.5), transformers (>=0.5.2.0) [details]
License BSD-3-Clause
Copyright 2020 Sandy Maguire
Author Sandy Maguire
Maintainer sandy@sandymaguire.me
Category Model
Home page https://github.com/isovector/algebra-checkers#readme
Bug tracker https://github.com/isovector/algebra-checkers/issues
Source repo head: git clone https://github.com/isovector/algebra-checkers
Uploaded by isovector at Thu Mar 19 22:07:45 UTC 2020
Distributions NixOS:0.1.0.0
Downloads 33 total (33 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2020-03-20 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for algebra-checkers-0.1.0.0

[back to package description]

algebra-checkers

Build Status

Dedication

"Any fool can make a rule, and any fool will mind it."

Henry David Thoreau

Overview

algebra-checkers is a little library for testing algebraic laws. For example, imagine we're writing an ADT:

data Foo a
instance Semigroup (Foo a)
instance Monoid (Foo a)

data Key


get :: Key -> Foo a -> a
get = undefined

set :: Key -> a -> Foo a -> Foo a
set = undefined

Let's say we expect the lens laws to hold for get and set, as well for set to be a monoid homomorphism. We can express those facts to algebra-checkers and have it generate tests for us:

lawTests :: [Property]
lawTests = $(testModel [e| do

law "set/set"
    (set i x' (set i x s) == set i x' s)

law "set/get"
    (set i (get i s) s == s)

law "get/set"
    (get i (set i x s) == x)

homo @Monoid
    (\s -> set i x s)

|])

Furthermore, algebra-checkers will generate tests to show that these laws are confluent. We can run these tests via quickCheck lawTests.

If we use the theoremsOf function instead of testModel, algebra-checkers will dump out all the additional theorems it has proven about our algebra. This serves as a good sanity check:

Theorems:

• set i x' (set i x s) = set i x' s (definition of "set/set")
• set i (get i s) s = s (definition of "set/get")
• get i (set i x s) = x (definition of "get/set")
• set i x mempty = mempty (definition of "set:Monoid:mempty")
• set i x (s1 <> s2) = set i x s1 <> set i x s2
    (definition of "set:Monoid:<>")
• set i1 (get i1 (set i1 x1 s1)) s1 = set i1 x1 s1
    (implied by "set/get" and "set/set")
• set i1 (get i1 (s12 <> s22)) s12 <> set i1 (get i1 (s12 <> s22)) s22
        = s12 <> s22
    (implied by "set/get" and "set:Monoid:<>")
• set i1 x'2 (set i1 x1 s11 <> set i1 x1 s21)
        = set i1 x'2 (s11 <> s21)
    (implied by "set/set" and "set:Monoid:<>")
• get i1 (set i1 x1 s11 <> set i1 x1 s21) = x1
    (implied by "get/set" and "set:Monoid:<>")


Contradictions:

• get i1 mempty = x1
    the variable x1 is undetermined
    (implied by "get/set" and "set:Monoid:mempty")

Uh oh! Look at that! This contradiction is clearly a bogus theorem, which lets us know that "get/set" and "set mempty" are nonconfluent with one another!