[Haskell-cafe] [Ann] group-theory

[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 <emilypi at cohomolo.gy> wrote:

> Actually, I was planning on implementing it with `FunctorWithIndex` lmao [image:
> 😂]
>
> 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 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
>>
>
> _______________________________________________
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20201213/1581487b/attachment.html>