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