[Haskell-cafe] Categorical description for vector-space instance of AdditiveGroup (Maybe a)

[trevor cook]

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 monoidinstance 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' fromNothing. I could fix the Just + Just line to use Nothing
instead of JustzeroV when a' ^+^ b' == zeroV, although doing so would
require Eq a andhence lose some generality. Even so, the abstraction
leak would probablyshow up elsewhere.Hm.-}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140910/ee6cb14b/attachment.html>