[Haskell-cafe] [Ann] group-theory

[jack at jackkelly.name]

December 13, 2020 1:49 PM, "Emily Pillmore" <emilypi at cohomolo.gy> wrote:

>> My problem with maps is that if I want to stay with Group and the obvious elementwise inversion, I
>> don't have a good answer for distinguishing `mempty` values at a particular key, vs the key not
>> being present at all.
> 
> This brings up a good point about sparsity. It's probably a good idea from a resource perspective
> to consider inserting mempty as he identity on the structure, and it raises an interesting point
> about how often you should simplify by delete mempty elements if you don't conflate it. Either way,
> I think you'll be forced to pick up an additional `Eq` constraint on the values, which may not be
> ideal.

You can use `MonoidNull`. from monoid-subclasses to avoid an `Eq` constraint.

However, auto-pruning `mempty` values from a map seems wonky. You'd have to newtype everything a la monoidal-containers, and consider equivalence classes under `mempty`-pruning:

```
-- Don't export constructor, force callers to use 'fromPruning' so there's no observable differences
newtype Pruning t a = Pruning (t a) deriving (Semigroup, TheUsualSuspects)

pruneMempty :: (Filterable t, MonoidNull a) => t a -> t a
pruneMempty = catMaybes $ \a -> if null a then Nothing else Just a

fromPruning :: (Filterable t, MonoidNull a) => Pruning t a -> t a
fromPruning (Pruning ta) = pruneMempty ta

instance (Filterable t, MonoidNull a) => Eq (Pruning t a) where
  x == y = pruneMempty x == pruneMempty y
```

I suspect (but haven't confirmed) that you'd then have `instance (Group g, MonoidNull g, Ord k) => Group (Pruning (MonoidalMap k) g)`.

>> The reason I believe this is that you can't make up "additional" inverses by adding mappings from
>> some `k => mempty`. The type system stops you from choosing any particular `k`, and even if you
>> could, you fail the requirement that `x <> inverse x <> x = x`
> 
> Do you mind expanding on this? i don't quite get what you're saying here.

Sure. AIUI, for a regular semigroup, you requite each `x` to have at least one pseudoinverse `inv x` s.t.:

1. `x <> inv x <> x = x`
2. `inv x <> x <> inv x = inv x`

For an inverse semigroup, you require each pseudoinverse to be unique.
I'm then thinking about whether you can have instance `(Ord k, InverseSemigroup g) => InverseSemigroup (Map k g)` or whether `(Ord k, InverseSemigroup g) => RegularSemigroup (Map k g)` is as far as you can go.

I'm mostly thinking about whether it's possible to cook up additional pseudoinverses when trying to lift to maps. Suppose you have a map `fromList [(k, v)]`. The obvious inverse is `fromList [(k, inv v)]`. My concern was whether you could cook up arbitrary additional inverses by saying `fromList [(k, inv v), (k', mempty)]` for some `k'` not present in the map. You cannot: while it passes condition (2), it fails condition (1). Also, if your `k` type variable is unconstrained, you can't even choose other key values because you know nothing about the key type.

Next question: We can get to inverse semigroups for maps, is it worth having a class for regular semigroups at all? I haven't seen any compelling regular semigroups, but maybe there are some? Also, the typeclass method you have to provide is pretty bad, because even if an element has many pseudoinverses, they're possibly not even enumerable. So you're probably still asking for a method `inv :: g -> g` 

Other question - which I still haven't had time to think about properly - is whether there should be an InverseSemigroup class between Semigroup and Group, or whether I can do the sort of stuff I want to tidy the `patch` library and its use in `reflex` using the cancellative operations in monoid-subclasses. If I can't, I think there's maybe a case for `InverseSemigroup` in `group-theory` (might be worth adding, regardless). My instinct is to proliferate data types rather than classes, and maybe that means having a `Pruning` type in monoidal-subclasses is better than adding a new class?

Hope that's clearer.

-- Jack


> On Fri, Dec 11, 2020 at 8:25 AM, <jack at jackkelly.name> wrote:
> 
>> December 10, 2020 5:05 AM, "Emily Pillmore" <emilypi at cohomolo.gy> wrote:
>> 
>>> Correct me if I'm wrong here, because I've never seen anyone describe maps like this, but it seems
>>> to me that for an algebraic constraint `c`, `c g ⇒ Map k g` would be a `k`-graded c-structure, and
>>> we can think of algebraic operations applied to those `g` meaningfully in that sense. For example,
>>> an indexed-list where `Group a ⇒ [(Int, a)]` can be seen as a ℤ-graded group.
>>> 
>>> In your example, Jack, inversion is defined on a map by `fmap inverse ≣ inverse_k0 + inverse_k1 + …
>>> + inverse k_n`, componentwise for each key. So perhaps your problem here for maps, is equivalent to
>>> finding a nice indexed-group for structure for the types:
>>> 
>>> ```
>>> — | A functor indexed by a discrete category. Not to be confused with
>>> -- indexed as in higher functor on functor ala Atkey's Outrageous Fortune.
>>> — This is not the most general encoding.
>>> —
>>> 
>>> class GradedFunctor f where
>>> imap :: (i → a → b) → f i a → f i b
>>> — Being a graded group requires that the "overall" structure be both an indexed functor,
>>> — as well as a group, so that `t i g = g_i0 + … + giN` forms a group as well.
>> I don't have the algebra knowledge to follow what you just wrote, but this class smells like
>> FunctorWithIndex from `lens`, but I don't know how principled that class is.
>> 
>> My problem with maps is that if I want to stay with Group and the obvious elementwise inversion, I
>> don't have a good answer for distinguishing `mempty` values at a particular key, vs the key not
>> being present at all.
>> 
>> However, I'm quite confident that elementwise inversion gives you an Inverse Semigroup because
>> inverses are unique. (I had previously mentioned that I thought you only had a Regular Semigroup,
>> but I think that was an error.) The reason I believe this is that you can't make up "additional"
>> inverses by adding mappings from some `k => mempty`. The type system stops you from choosing any
>> particular `k`, and even if you could, you fail the requirement that `x <> inverse x <> x = x`
>> 
>> -- Jack