morphismtech / free-categories

free categories
BSD 3-Clause "New" or "Revised" License
9 stars 2 forks source link

Added a Free Category Parameterized by a Functor #5

Closed SamuelSchlesinger closed 3 years ago

SamuelSchlesinger commented 4 years ago

Hey Eitan. You probably don't want to get rid of this Show instance, but sadly it blows up my version of ghc so its gotta be changed for my branch to compile. I'm on 8.8.1.

I think this idea of a free category parameterized by a functor is neat. It is interesting that the Applicative turns out to be the right idea to make it a QMonad, as I originally only chose that to get a QPointed for free. I haven't proved that this is actually monad in the category of categories, but I suspect it is. I have proved that it satisfies the category laws, and I will post that here, using Node instead of :>>* as that is how I had it in my original implementation and this is copied and pasted. I could verify the monad laws too if you'd like, I am not sure of them being satisfied.

Node cf csf . (Node cg csg . Node ch csh) = Node ch (fmap (Node cf csf .) (fmap (Node cg csg .) csh)) = Node ch (fmap ((Node cf csf .) . (Node cg csg .)) csh) = Node ch (fmap (\c -> Node cf csf . Node cg csg . c) csh) = Node ch (fmap ((Node cf csf . Node cg csg) .) csh) = (Node cf csf . Node cg csg) . Node ch csh