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.