[Haskell-cafe] [Ann] group-theory

[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 ( 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@ cohomolo. gy (
> 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
> 
> 
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20201213/61a32f1c/attachment.html>