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

On Thu, Sep 11, 2014 at 08:20:38AM +0800, John Lato wrote:

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

...

[...] 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.

Yes, it seemed that way to me -- trying to make Nothing coincide with Just zeroV collapses Maybe a to a.

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.

Obviously this also fails for e.g. computable reals. So is the hope here to treat Maybe v like a vector space over F if v is a vector space over F? I don't think it can be done consistently. But you should be able to make Maybe v a /semi/-vector space over F (inventing terminology here); i.e. Maybe v satisfies all the vector space axioms except (negate a) *^ v == a *^ (negateV v), which doesn't make sense. But I don't know that you can do much linear algebra without negation! -- Jason McCarty