On Thu, Sep 11, 2014 at 8:01 AM, Jason McCarty wrote:

Hi Trevor,

...

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

On Wed, Sep 10, 2014 at 11:13:43AM -0400, trevor cook wrote: 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.

Well, this is the crux of the problem. If you want to define

zeroV = Just zeroV

, you'll run into abstraction leaks unless you also have

Nothing == Just zeroV = True

(and this should commute too), because it explicitly makes the two units (Nothing and zeroV) equivalent. But even if that were possible to write, you probably don't really want it. Even if you have

newtype MaybeAG a = MaybeAG (Maybe a)

and suitably hide everything, so that a `MaybeAG a` is observably identical to just `a`, you may as well use `a` directly. Unfortunately the other proposed solution, of making 'Just a ^+^ Just b' use Nothing if 'a^+^b == zeroV', in addition to being less general, looks like trouble if `a` is a Float or Double. John L.

This is a fool rushing in where angels fear to tread, but having Nothing or Maybe v where v is in an additive group reminds me a bit of Grassman Algebra and makes me wonder if Maybe is really what's wanted here.