[Ann] group-theory

[Emily Pillmore]

Hello all,

I am pleased to announce the release of the  group-theory package: a package aimed at implementing the theory of finite groups in a reasonably ergonomic, well-documented, and featureful way. It's hardly finished, but my co-maintainer, Reed Mullanix (@totbwf) and I thought this was a good mvp with which we could announce.  

Contributions are very welcome, and I hope everyone enjoys.

Cheers,

Emily Pillmore

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

[Emily Pillmore]

Hi Marcin,

Nice work; I also implemented free groups in the free-algebra package

Wonderful - I'll take a look. Those were a bit rough, and it'd be good to see how you encoded them in `free-algebra`. Maybe we can collaborate on expanding the knowledgebase and utility of free group calculations in our respective packages :)

However 'FG' is the free group in the class of all groups.

I'm glad you noted this as well! The `DList` encoding is interesting - I'll need to study that a bit :)

Someone has also linked me to Sjoerd's `free-functors` library, which seems is also very interesting: 

https://github.com/sjoerdvisscher/free-functors/blob/master/src/Data/Functor/Free.hs#L70

There's an interesting difference between 'FreeGroup' (using notation of your package) and 'FG'.  First one is not a free group in the class of all groups, but only free in the class of groups for which multiplication is strict in the left argument

Correct. Regarding motivation, I provided both because I know some people do like to operate in the fast-and-loose strict subset of Haskell. It's no skin off my back. But I was very unsatisfied with strict (vis. "moral") Free constructions with respect to bottoms, and, inspired by Dan Doel's article (http://comonad.com/reader/2015/free-monoids-in-haskell/), attempted to find a free construction for groups that was more in line with Haskell's domain-like types. I note this article in the documentation for FG.

Maybe this deserves a broader blog post? 

I identified that `Foldable` can only be defined for algebraic structures for which `Endo b` has the same algebra type; this fails for groups: only automorphisms form a group.  Having a seprate `GroupFoldable` class makes sense.

That class ended up being good for two things: 

1. Great puns.
   
2. Very convenient word evaluation
   

If you'd like to add to it, I'd be stoked.

Cheers,

Emily

On Sat, Dec 05, 2020 at 2:53 PM, <[hidden email]> wrote:

Hi Emily,

Nice work; I also implemented free groups in the free-algebra package.

There's an interesting difference between 'FreeGroup' (using notation of your package) and 'FG'.  First one is not a free group in the class of all groups, but only free in the class of groups for which multiplication is strict in the left argument, i.e. ones that satisfy the equation `⊥ <> a == ⊥`.   That's because `++` is strict in the left argument. For the same reason `[]` is free monoid in the class of left strict monoids.

However 'FG' is the free group in the class of all groups.  Another isomorphic construction of a free group  (in the class of all groups) can be based on `DList` - the free monoid.  You might want to check out https://hackage.haskell.org/package/free-algebras-0.1.0.0/docs/Data-Algebra-Free.html which gives a uniform interface for all free algebras (not just groups).  You'll recover there `Monad` instance of `FG` (and `FreeGroup`), and a bit more.

I identified that `Foldable` can only be defined for algebraic structures for which `Endo b` has the same algebra type; this fails for groups: only automorphisms form a group.  Having a seprate `GroupFoldable` class makes sense.

Cheers,

Marcin Szamotulski

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐

On Saturday, December 5th, 2020 at 19:52, Emily Pillmore <[hidden email]> wrote:

Hello all,

I am pleased to announce the release of the  group-theory package: a package aimed at implementing the theory of finite groups in a reasonably ergonomic, well-documented, and featureful way. It's hardly finished, but my co-maintainer, Reed Mullanix (@totbwf) and I thought this was a good mvp with which we could announce.  

Contributions are very welcome, and I hope everyone enjoys.

Cheers,

Emily Pillmore

_______________________________________________
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 - Haskell-Cafe mailing list]

Hi Emily, Reed,

Congrats on the release. The mathematics involved is a little above my pay grade (there's only a bit of undergrad group theory in my brain somewhere, covered in cobwebs), but there is an implementation thing I'd like your thoughts on, while your heads are in this space:

Over in Reflex-land, they've been using an internal Group class for their `patch` library ( https://hackage.haskell.org/package/patch ), which has an instance (Ord k, Group q) => Group (MonoidalMap k q) that's unlawful:

fromList [(1,Sum 1)] <> invert (fromList [(1, Sum 1)]) == fromList [(1, Sum 0)]

(This is used in reflex's QueryT, I think so you can get incremental updates to the answer to a query.)

I think the actual abstraction they'd want is more like an inverse semigroup, where (x <> invert x <> x == x) and (invert x <> x <> invert x == x). But when I was chatting with taneb about this (we were talking about moving `patch` over to `groups` at one point), just putting `class InverseSemigroup` into a groups package means you have a tower of three classes that differ only in laws. And that feels a bit awkward.

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

-- Jack

December 6, 2020 4:52 AM, "Emily Pillmore" <[hidden email]> wrote:

> Hello all,
>
> I am pleased to announce the release of the group-theory package: a package aimed at implementing
> the theory of finite groups in a reasonably ergonomic, well-documented, and featureful way. It's
> hardly finished, but my co-maintainer, Reed Mullanix (@totbwf) and I thought this was a good mvp
> with which we could announce.
>
> Contributions are very welcome, and I hope everyone enjoys.
> Cheers,
> Emily Pillmore

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

[Mario]

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.


_______________________________________________
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 - Haskell-Cafe mailing list]

December 9, 2020 4:16 AM, "Mario" <[hidden email]> 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 ), 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
_______________________________________________
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.

[Emily Pillmore]

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, <[hidden email]> wrote:

December 9, 2020 4:16 AM, "Mario" <[hidden email]> 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 ), 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

_______________________________________________
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 - Haskell-Cafe mailing list]

December 10, 2020 5:05 AM, "Emily Pillmore" <[hidden email]> 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.

[Emily Pillmore]

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",  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, <[hidden email]> wrote:

December 10, 2020 5:05 AM, "Emily Pillmore" <[hidden email]> 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.

[Carter Schonwald]

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

On Sat, Dec 12, 2020 at 10:52 PM Emily Pillmore <[hidden email]> wrote:

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",  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, <[hidden email]> wrote:

December 10, 2020 5:05 AM, "Emily Pillmore" <[hidden email]> 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.

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

[Viktor Dukhovni]

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.

[Zemyla]

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

[Carter Schonwald]

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

_______________________________________________
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 - Haskell-Cafe mailing list]

December 13, 2020 1:49 PM, "Emily Pillmore" <[hidden email]> 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, <[hidden email]> wrote:
>
>> December 10, 2020 5:05 AM, "Emily Pillmore" <[hidden email]> 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.

[宮里 洸司]

> 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 <[hidden email]>:

>
> December 13, 2020 1:49 PM, "Emily Pillmore" <[hidden email]> 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, <[hidden email]> wrote:
> >
> >> December 10, 2020 5:05 AM, "Emily Pillmore" <[hidden email]> 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 <[hidden email]> */
_______________________________________________
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.

[Olaf Klinke]

Koji Miyazato wrote:
> > 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.

A beautiful example of topological groups: Their topology is completely
determined by the neighbourhoods of the identity element. If the
identity element is isolated, the entire group is discrete.

Olaf

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