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.

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."

Its a horrible argument, hopefully the cafe will show some better thinking for me.

Regards,
Trevor

-- Maybe is handled like the Maybe-of-Sum monoid
instance AdditiveGroup a => AdditiveGroup (Maybe a) where
  zeroV = Nothing
  Nothing ^+^ b'      = b'
  a' ^+^ Nothing      = a'
  Just a' ^+^ Just b' = Just (a' ^+^ b')
  negateV = fmap negateV

{-

Alexey Khudyakov wrote:

  I looked through vector-space package and found lawless instance. Namely Maybe's AdditiveGroup instance

  It's group so following relation is expected to hold. Otherwise it's not a group.
  > x ^+^ negateV x == zeroV

  Here is counterexample:

  > let x = Just 2 in x ^+^ negateV x == zeroV
  False

  I think it's not possible to sensibly define group instance for
  Maybe a at all.

I see that the problem here is in distinguishing 'Just zeroV' from
Nothing. I could fix the Just + Just line to use Nothing instead of Just
zeroV when a' ^+^ b' == zeroV, although doing so would require Eq a and
hence lose some generality. Even so, the abstraction leak would probably
show up elsewhere.

Hm.

-}