Write to LOG.md about laws

tweag · Sep 21, 2018 · 7f45927 · 7f45927
1 parent 2b18ba5
commit 7f45927
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/LOG.md b/LOG.md
@@ -0,0 +1,16 @@
+# 2018.09.21
+
+## Capability type-class laws
+
+The capabilities `HasReader`, `HasState`, and `HasWriter` provide the same
+interface as the corresponding Mtl type classes, apart from the tags.
+Unfortunately, neither the Mtl documentation, nor the transformers documentation
+specify any laws for these type classes. A discussion about this can be
+found on the [mtl issue tracker](https://github.com/haskell/mtl/issues/5).
+
+This library does define laws for the capability classes based on the above
+mentioned mtl issue. At this point these are not definitive.
+A detailed discussion of the state laws, and formal proofs written in Agda
+can be found can be found in
+[this](http://gallium.inria.fr/blog/lawvere-theories-and-monads/)
+blog post by Pierre Dagand.