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

[Jason McCarty]

On Thu, Sep 11, 2014 at 08:20:38AM +0800, John Lato wrote:
> On Thu, Sep 11, 2014 at 8:01 AM, Jason McCarty <jmccarty at sent.com> 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 <jmccarty at sent.com>