Hi Trevor, On Wed, Sep 10, 2014 at 11:13:43AM -0400, trevor cook wrote:
Hi Haskell Cafe,
In Vector-space-0.8.7, there is the cited inconsistency of the definition of AdditiveGroup (Maybe a). I've posted the source, including comment, below for reference. Following the logic of the counterexample and Conal's (and or Andy Gill's) comment, the problem hinges on the equality, Nothing = Just (zeroV :: a).
I'm curious about the catigorical description of this situation. Does this mean that the category of Additive Groups and Maybe Additive Groups are equivalent as categories? I'm not proposing that this is somehow a resolution to vector-space, but rather trying to gain some insight into equivalence, naturalitity, adjunction, etc.
It depends on what you want the morphisms to be in the category of "Maybe Additive Groups." Let G be the category of additive groups and MG be the category of "Maybe Additive Groups" with objects Maybe g, for g in G. If Hom_MG(Maybe a, Maybe b) := { fmap f | f <- Hom_G(a, b) }, then G is equivalent to MG. But you probably expect to have some more morphisms in MG, like e.g. (+ Just x) :: Maybe a -> Maybe a, which doesn't have the form (fmap f) for any f :: a -> a. In particular, Maybe a has at least two morphisms for any a in G (this and the identity). This is bad, because an equivalence of categories F: G -> MG must be a full functor; i.e., Hom_G(a, b) -> Hom_MG(Maybe a, Maybe b) must be surjective. If () in G is the trivial group, then Hom_G((), ()) has cardinality 1, but Hom_MG(Maybe (), Maybe ()) has at cardinality at least 2, so this is impossible. I don't know if there are any other structures you can put on MG that would make it equivalent to G...there certainly aren't if you want F = Maybe to be the equivalence. However, if s is a semigroup, then Maybe s is a monoid (with unit Nothing). So let S be the category of semigroups and M the category of monoids. Then Maybe is a functor S -> M. I think it is left adjoint to the forgetful functor U: M -> S. It might be a good exercise to check. But this still isn't an equivalence of categories, even if you restrict to the image { Maybe s : s <- S }, for the same reason as before. IMO this is probably the best "categorical" description of the situation.
My thinking as to why equivalence is that if we have the instance below defined using: zeroV = Just zeroV
and making appropriate changes following that new decision. Nothing ^+^ Nothing = zeroV a ^+^ Nothing = a Nothing ^+^ b = b negateV Nothing = zeroV negateV a = fmap negateV then we pretty much defer the group structure of (Maybe a) to be based totally on the structure of a. And since `a` and `Maybe a` are not isomorphic then "hey, I just learned about this new thing so maybe its that."
Unfortunately this isn't even a monoid since it doesn't have a unit
(Nothing + u /= Nothing for any u). So this just gives a functor G -> S;
I'm not sure you can say much more about it.
I hope that helps a little, sorry natural transformations didn't come
into play.
--
Jason McCarty