On 2020-12-05 7:04 p.m., Jack Kelly via Haskell-Cafe wrote:

Dunno what the answer is, but I wanted to flag it while your package is young and breaking changes are easy. I've been meaning to have a crack at moving the reflex patch-verse over to monoid-subclasses ( https://hackage.haskell.org/package/monoid-subclasses ), which I provides some the necessary tools with different names (patch reinvents MonoidNull, and I'm hoping that a subtraction-that-removes keys could be lawful for one of the Reductive/Cancellative classes).

I'm the author and maintainer of monoid-subclasses, and I'd accept a PR that adds InverseSemigroup without overly disturbing the existing classes. The whole purpose of the package, after all, is to support mathematical abstractions that are richer than semigroups but are not proper groups.

Okay, I'm fully caffeinated and out of bed. 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. — class (GradedFunctor t, Group (t i g), Group g)  ⇒ GradedGroup t i g where ixinvert :: i→ t i g → t i g ``` Something along those lines. Thoughts? I'm spitballing here. Cheers, Emily On Wed, Dec 09, 2020 at 5:43 AM, < jack@jackkelly.name > wrote:

December 9, 2020 4:16 AM, "Mario" < blamario@ rogers. com ( blamario@rogers.com ) > wrote:

...

On 2020-12-05 7:04 p.m., Jack Kelly via Haskell-Cafe wrote:

...

Dunno what the answer is, but I wanted to flag it while your package is young and breaking changes are easy. I've been meaning to have a crack at moving the reflex patch-verse over to monoid-subclasses ( https:/ / hackage. haskell. org/ package/ monoid-subclasses ( https://hackage.haskell.org/package/monoid-subclasses ) ), which I provides some the necessary tools with different names (patch reinvents MonoidNull, and I'm hoping that a subtraction-that-removes keys could be lawful for one of the Reductive/Cancellative classes).

I'm the author and maintainer of monoid-subclasses, and I'd accept a PR that adds InverseSemigroup without overly disturbing the existing classes. The whole purpose of the package, after all, is to support mathematical abstractions that are richer than semigroups but are not proper groups.

Thanks for the offer. There are two things I want to sort out first:

1. I may have erred when suggesting InverseSemigroup; "inverting" a `Group g => Map k g` via `fmap invert` might admit nonunique inverses, which gives you an even weaker structure called a Regular Semigroup.

2. I want to see if I can make the behaviour I want fit the existing classes provided by `monoid-subclasses` (specifically `Cancellative` and maybe `Reductive` instances for types provided by `monoidal-containers`). It might be something like `instance (MonoidNull g, Group g, Commutative g, Ord k) => Reductive (MonoidalMap k g)`, where the reduction operation subtracts values at matching keys, pruning nulls. I need to at least write out the property tests to see if it might be sound.

Best,

-- Jack

Actually, I was planning on implementing it with `FunctorWithIndex` lmao 😂

but I don't know how principled that class is.

I haven't thought about this in depth enough to triple check this, but I do think the class is principled. My mental model for it is "structures that can be decomposed in terms of graded objects ( https://ncatlab.org/nlab/show/graded+set ) ",  that is, `FunctorWithIndex` is a functor `C^J → D` from the category of J-graded objects of C to some other category `D`. Such a functor should take a mapping of graded objects `i → (a → b)` to a mapping `f a → f b` in D. This gets you the signature described in the class:   `imap :: (i → a → b) → (f a → f b)`.

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.

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. Cheers, E On Fri, Dec 11, 2020 at 8:25 AM, < jack@jackkelly.name > wrote:

December 10, 2020 5:05 AM, "Emily Pillmore" < emilypi@ cohomolo. gy ( emilypi@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

On Sun, Dec 13, 2020 at 12:19:18AM -0500, Carter Schonwald wrote:

Having a decidable equality seems important for reasoning about groups. Or computing on representations thereof.

This is of course not always possible. If a group is presented as a quotient of a free group on a set of generators via some set of relators, then deciding whether two words are equal is IIRC known to be generally intractable. One can still perform the group operation, but there is no known terminating algorithm for constructing a canonical form for an element, performing equality tests, ... Of course one might take the view that groups where equality is not computable are not "useful", but that might rule out some applications. -- Viktor.

Absolutely. I do think that the moment you start caring about representations or presentations, as I believe emily has mentioned, some stronger assumptions for certain families of interfaces is worth considering to allow for cool stuff when those assumptions are admissible. On Sun, Dec 13, 2020 at 1:51 AM Zemyla wrote:

A simpler example of groups with no computable equality: the Sum group on computable reals. x + negate x === 0 for all x, but we can never fully prove it, only demonstrate it for each number of digits. And yet this is a perfectly well behaved abelian group.

On Sat, Dec 12, 2020, 23:41 Viktor Dukhovni wrote:

...

On Sun, Dec 13, 2020 at 12:19:18AM -0500, Carter Schonwald wrote:

...

Having a decidable equality seems important for reasoning about groups. Or computing on representations thereof.

This is of course not always possible. If a group is presented as a quotient of a free group on a set of generators via some set of relators, then deciding whether two words are equal is IIRC known to be generally intractable. One can still perform the group operation, but there is no known terminating algorithm for constructing a canonical form for an element, performing equality tests, ...

Of course one might take the view that groups where equality is not computable are not "useful", but that might rule out some applications.

-- Viktor. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

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

For groups, there is no difference between `MonoidNull` and `Eq`, as you can define `x == y` be `null (x <> inv y)`. There are monoids which `==` is not even decidable but `null` is (e.g. context-free grammars with equality defined by the language it defines), but such monoid necessarily has no `Group` instance. 2020年12月25日(金) 22:08 Jack Kelly via Haskell-Cafe :

December 13, 2020 1:49 PM, "Emily Pillmore" 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, wrote:

...

December 10, 2020 5:05 AM, "Emily Pillmore" 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

---

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- /* Koji Miyazato */