algebra-checkers
algebra-checkers copied to clipboard
isovector
checkers for algebra driven design
Right now confluence laws will generate things like `[a] = pure a`, which just waste test cycles. We can refine the tests by ensuring that at least one function or...
It should only emit type sigs that have a corresponding mu binding
The following fails to typecheck: ```haskell type System w μ System w = Id -> Maybe w type Id μ Id = Int delEntity :: Id -> System w ->...
If you don't add any `mu` mappings, you get a big chain of TH errors: ``` • The type signature for ‘delEntity’ lacks an accompanying binding (The type signature must...
Right now it won't compile if you don't explicitly depend on `template-haskell`. boo
```haskell do law "mempty/Just" $ mempty == Just (Any True) law "mempty/Just" $ mempty @(Maybe Any) == Nothing ``` ==> ``` • Nothing == Just (Any True) @(Maybe Any) (implied...