[Haskell-cafe] [Ann] group-theory

[jack at jackkelly.name]

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