Adds iterative categories to CategoryTheory, adding a general notion of loops of which both aloop (modulo a tweak or two) and mrec are instances, thus providing some basic lemmas to try and generalize our techniques to mrec.
Fixes the implicit arguments of lemmas using type classes (previously we had to sprinkle typeclasses eauto all over the place)
Iterative categories are essentially a subclass of traced categories (which we had previously defined only for the special case of ktrees), with an additional axiom to unfold loops. The definition also uses fewer axioms, making the theory less painful to instantiate. There are quite a few different presentations of this structure, the current axioms are taken from Complete Elgot Monads and Coalgebraic Resumptions, Goncharov et al. https://arxiv.org/abs/1603.02148v1 (Elgot monads are basically those whose Kleisli categories are iterative categories.)
I'm wondering how to prove a loop unrolling lemma which informally looks like loop f = loop (f ;; f). I'm not sure this theory is sufficient and we may need something more specific. More generally, the category-based equational theory is still far from complete to support everything one might want to prove. It currently requires an awkward unfolding step to connect to definitions using the more usual monadic notation, such as the Imp semantics in our main example. Such unfolding is also currently necessary for coinductive reasoning with paco, both to prove the current equational theory, and more elaborate equations that the current CategoryTheory does not cover. It would be nice to have a smoother interface between the monadic and categorical notations.
Adds iterative categories to
CategoryTheory, adding a general notion of loops of which bothaloop(modulo a tweak or two) andmrecare instances, thus providing some basic lemmas to try and generalize our techniques tomrec.Fixes the implicit arguments of lemmas using type classes (previously we had to sprinkle
typeclasses eautoall over the place)Iterative categories are essentially a subclass of traced categories (which we had previously defined only for the special case of ktrees), with an additional axiom to unfold loops. The definition also uses fewer axioms, making the theory less painful to instantiate. There are quite a few different presentations of this structure, the current axioms are taken from Complete Elgot Monads and Coalgebraic Resumptions, Goncharov et al. https://arxiv.org/abs/1603.02148v1 (Elgot monads are basically those whose Kleisli categories are iterative categories.)
I'm wondering how to prove a loop unrolling lemma which informally looks like
loop f = loop (f ;; f). I'm not sure this theory is sufficient and we may need something more specific. More generally, the category-based equational theory is still far from complete to support everything one might want to prove. It currently requires an awkward unfolding step to connect to definitions using the more usual monadic notation, such as the Imp semantics in our main example. Such unfolding is also currently necessary for coinductive reasoning with paco, both to prove the current equational theory, and more elaborate equations that the currentCategoryTheorydoes not cover. It would be nice to have a smoother interface between the monadic and categorical notations.