From 7f459279f38157852787a84726e21c46d7d5cd5d Mon Sep 17 00:00:00 2001 From: Andreas Herrmann Date: Fri, 21 Sep 2018 15:09:06 +0200 Subject: [PATCH] Write to LOG.md about laws --- LOG.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 LOG.md diff --git a/LOG.md b/LOG.md new file mode 100644 index 0000000..06a3f15 --- /dev/null +++ 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.