<div dir="auto">Having a decidable equality seems important for reasoning about groups.  Or computing on representations thereof. </div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Dec 12, 2020 at 10:52 PM Emily Pillmore <<a href="mailto:emilypi@cohomolo.gy">emilypi@cohomolo.gy</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)"><div><div><div><div><div>Actually, I was planning on implementing it with `FunctorWithIndex` lmao <img src="https://emojis.superhuman.com/1F602.png" alt="😂" title="😂" style="height: 15px !important; width: 15px !important; vertical-align: text-bottom !important;" height="15" width="15"><br></div><div><br></div><blockquote><div><span>but I don't know how principled that class is.</span><br></div></blockquote><div><div><br></div><div>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 <a href="https://ncatlab.org/nlab/show/graded+set" target="_blank">graded objects</a>",  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)`. <br></div><div><br></div></div><blockquote><div><span>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.</span><br></div></blockquote><div><div><br></div><div>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. <br></div><div><br></div></div><blockquote><div><span>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`</span><br></div></blockquote><div><div><br></div><div>Do you mind expanding on this? i don't quite get what you're saying here. <br></div><div><br></div><div>Cheers,<br></div><div>E<br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><div><br></div></div><div><div style="display:none;border:0px;width:0px;height:0px;overflow:hidden"><img src="https://r.superhuman.com/hGuKaP2qvw06QLZjyQMgHkQg5D4e75ftLJaOUfJmr7T3XUCwgi85cM8RArvzTleT9UvCJB-4e9WzekmE-QHkyKQvaf-qDNWCgwuKRoJ5bp0_UXK6TIj9cyRSt6ucW0Uagc5c8V18VFRcy0XimSKKFEE65PSm7aILroLYx49gUlZ65kD-qie7n9YEUw4.gif" alt=" " width="1" height="0" style="display: none; border: 0px; width: 0px; height: 0px; overflow: hidden;"></div><br><div></div></div></div></div></div><div><div><div><br><div><div class="gmail_quote">On Fri, Dec 11, 2020 at 8:25 AM,  <span dir="ltr"><<a href="mailto:jack@jackkelly.name" target="_blank">jack@jackkelly.name</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)"><div class="gmail_extra"><div class="gmail_quote" id="m_6966964094642861859null"><p>
December 10, 2020 5:05 AM, "Emily Pillmore" <<a rel="noopener noreferrer" href="mailto:emilypi@cohomolo.gy" target="_blank">emilypi@cohomolo.gy</a>> wrote:
</p><blockquote><p>
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.
</p><p>
In your example, Jack, inversion is defined on a map by `fmap inverse ≣ inverse_k0 + inverse_k1 + …
<br>
+ 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:
</p><p>
```
<br>
— | A functor indexed by a discrete category. Not to be confused with
<br>
-- indexed as in higher functor on functor ala Atkey's Outrageous Fortune.
<br>
— This is not the most general encoding.
<br>
—
</p><p>
class GradedFunctor f where
<br>
imap :: (i → a → b) → f i a → f i b
<br>
— Being a graded group requires that the "overall" structure be both an indexed functor,
<br>
— as well as a group, so that `t i g = g_i0 + … + giN` forms a group as well.
</p></blockquote><p>
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.
</p><p>
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.
</p><p>
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`
</p><p>
-- Jack</p></div></div></blockquote></div></div><br></div></div></div>_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div></div>