MonadLaws are commented out about coq-ext-lib HOT 20 CLOSED

It needs porting. When making things universe polymorphic there were issues with the XxxLaws classes. Do you have any interest in updating them?

from coq-ext-lib.

Yes, I have an interest in updating them. I must admit, I am not very experience with universe polymorphism yet, but if you can provide some guidance I will be glad to help.

from coq-ext-lib.

Thinking a little bit more about this, I think the bigger problem is that the equivalence here should not be =, it should be some equivalence relation defined by the monad. So we would really want something like:

Class MonadLaws (m : Type -> Type) (meq : forall a, relation a -> relation (m a)) : Type :=
{ bind_ret : forall a (c : m a), meq (bind c ret) c
; ..
}.

Without this generaliztion, monads such as Reader and State are not monads because Coq without HoTT doesn't provide functional extensionality.

from coq-ext-lib.

Dealing with quotients also introduces a few other issues because we don't want to just use = in various places and if we don't use = then it can be difficult to prove some of the theorems.

from coq-ext-lib.

Here is an example of how I tried to implement Reader comonad. I guess I've specified Leibnitz equality via type_libniz.

https://gist.github.com/vzaliva/74a7ba21b36f0092d29feee4d7276625

So I guess we want to use the same equality as w_type in monad laws instance?

from coq-ext-lib.

This works because the writer monad doesn't have a quotient. If your monad co rains a function type or you want to have a quotient on the monoid in the writer, then things will start to fall apart.

If I recall correctly, this was a big problem when I tried to use the monad laws before.

from coq-ext-lib.

I am sorry, somehow I've confused the two discussions we had and thought you are talking about equivalence wrt CoMonadLaws. Hence my previous comment. Sorry about this.

This might be a naive suggestion, but could not we just specify the equivalence for both monads as well as underlying type via a type class? Similar to Equiv and Equivalence type classes in math-classes library?

from coq-ext-lib.

from coq-ext-lib.

I have a suggestion. Before doing this for MonadLaws, perhaps we can try this first for CoMonadLaws I've proposed (assuming this approach is also applicable there). This is the much simpler case and we can use it to test the approach before doing bigger changes for MoandLaws which might cascade to other places like ReaderMonadLaws.

On the other hand, if you think the changes are local to MonadLaws along and will not require significant rework of other parts of the library we can try it right there.

Either way, I am willing to help.

from coq-ext-lib.

from coq-ext-lib.

OK. I have created a branch where I will experiment with it: https://github.com/vzaliva/coq-ext-lib/tree/comonad-equality Once it is working I will merge it up and it will appear the pull request I've submitted.

from coq-ext-lib.

Sorry, I am not familiar with Delay comonad. What comes to mind is something like:

Inductive Delay (T:Type): Type :=
  delayed (x:T) : Delay T.

Definition undelay {T:Type} (d: Delay T): (unit -> T) :=
  match d with
    delayed x =>  fun _ => x
  end.

Instance DelayComonad:
  CoMonad (Delay) :=
  {
    extract A ma := (undelay ma) tt ;
    extend A B f ma := delayed (f ma)
  }.

Is that what you had in mind?

from coq-ext-lib.

I'm also trying to revive this module. In what situations are all the proper assumptions necessary, or can we simplify them away?

For example for the functor laws:

https://github.com/coq-ext-lib/coq-ext-lib/blob/e800d3e89785df7e78d1d92fbf6cf52e85058c48/theories/Structures/FunctorLaws.v#L14-L32

The above generalized identity law should follow from the plain identity law (below) and properness of fmap. I'm less sure about the composition law, when does it not hold unconditionally?

fmap id = id  (* identity *)
fmap (f . g) = fmap f . fmap g  (* composition *)
(f = g) -> fmap f = fmap g  (* properness of fmap *)
(* where [=] is [equals] (not [eq]) *)

from coq-ext-lib.

The way things work here is that there is the raw type T and then the "good part of T". The first place that this usually comes up is if we don't want to assume functional extensionality and want to pass functions around, but it also comes up if you start having functions inside of your Ms as well.

If you don't assume functions like f are proper, then you don't know proper (f x) given proper x.

from coq-ext-lib.

There are other ways to address this, one using subset types, and others using things like higher-inductive types. I'm happy to have an hour phone call about this to see how we might be able to straighten this out.

from coq-ext-lib.

I mean that specifically in the case of functor/monad laws, I have a hard time imagining a functor/monad that doesn't satisfy these laws unconditionally. I think I understand the point of properness, but I'm not convinced this is the place where it should be applied.

from coq-ext-lib.

What about instances where you have F (M x) where both F and M are Functors? It seems like if you work in the PER setting, then you PERs on everything. Can I write ret (fmap id x) if I don't have a properness fact on fmap?

from coq-ext-lib.

It's fine to have a properness fact on fmap (fmap_proper). But why do the two main functor laws (fmap_id, fmap_compose) need to quantify over proper morphisms? For which functors is it necessary?

from coq-ext-lib.

I can't think of any right now except maybe a contrived example where you have monad transformers. I'm fine with dropping them, but I wonder if it might be better to go a different route where we don't fix the PER structure, but rather parameterize over arbitrary categories.

from coq-ext-lib.

Rethinking that last comment about abstracting. I'm not sure how the category theory would bottom out.

from coq-ext-lib.