**Monthly Downloads**: 45

**Programming language**: Haskell

**License**: BSD 3-clause "New" or "Revised" License

## algebra-checkers alternatives and similar packages

Based on the "Model" category

*Do you think we are missing an alternative of algebra-checkers or a related project?*

## README

## algebra-checkers

## 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!