morganthomas / purescript-group

Algebraic groups for PureScript.
Apache License 2.0
6 stars 6 forks source link

cyclic and finite cyclic groups #12

Closed matthewleon closed 6 years ago

matthewleon commented 6 years ago

This might seem a bit backward, but I'll start this proposal with the finite cyclic groups. They seem to be the more useful ones, because they give you principled conversion from Int.

class (Cyclic g, BoundedEnum g) <= FiniteCyclic g where
  fromInt :: Int -> g

The Cyclic superclass gives us:

class (Group g) <= CyclicGroup g where
  generator :: g

You can define a defaultFromInt that uses the generator.

The most immediate problem I see this resolving is that BoundedEnum's fromInt has a Maybe, and no sensible default implementation.

Curious for others' thoughts.

morganthomas commented 6 years ago

Re: default implementation of fromInt. If I understand the BoundedEnum laws right, then the integers corresponding to the values of a BoundedEnum g can be computed as:

fromEnum bottom, fromEnum (succ bottom), fromEnum (succ (succ bottom)) ..., fromEnum top

That will be a sequence of contiguous integers. It gives us a mapping from an interval in the integers to g, and we can extend that to a mapping from all integers to g by repeating it cyclically. At least conceptually. I haven't thought through how best to do it in code, or if there's a really good way to do it in code.

Is fromInt supposed to be a group homomorphism from Int to g? Do the laws of Cyclic and FiniteCyclic guarantee that's so? For example maybe this is a law of fromInt:

fromInt 0 = bottom

That would make sense with bottom being required to be the identity of the finite cyclic group, as expressed by the laws:

for all x :: g. bottom <> x == x for all x :: g. x <> bottom == x

On the other hand, I'm not sure that bottom should be required to be the identity.

Also, I believe that fromInt could be defined on Cyclic and not just FiniteCyclic. Every infinite cyclic group is isomorphic to the integers. fromInt could be required to be a homomorphism from Int to g for all Cyclic, and in the case of infinite cyclic groups it will be an isomorphism (automatically, I think).

I imagine there's quite a bit more to think through here. Just brainstorming.

morganthomas commented 6 years ago

What about this law?

fromInt 1 = generator

I'm thinking fromInt -1 = generator could also be true, but that mathematically, either 1 or -1 must be the generator, i.e. nothing else can serve as the generator for the additive group of integers. In the background I'm assuming that we want this to be a true law:

fromInt generator = generator

hdgarrood commented 6 years ago

Cyclic groups are necessarily abelian, so perhaps this should have a Commutative superclass? Also, it’s maybe worth considering whether a type class is the right encoding for this idea; since there is only one cyclic group of any given cardinality up to isomorphism, you could potentially argue that a concrete type makes more sense? There’s already Int for the infinite case (or various bigint options if necessary), and there’s modular-arithmetic for the finite cases.

Is the idea of FiniteCyclic to provide a more performant alternative to flip power generator?

morganthomas commented 6 years ago

I guess you might want a FiniteCyclic type class in a case where you have an enum which you want to view as being a cyclic group, because there's some binary operation on it which you care about, which makes it a cyclic group. I haven't thought of a satisfying, concrete example which is not numbers.

matthewleon commented 6 years ago

Cyclic groups are necessarily abelian, so perhaps this should have a Commutative superclass?

Whoops, missed that! Thanks.

matthewleon commented 6 years ago

Re: default implementation of fromInt. If I understand the BoundedEnum laws right, then the integers corresponding to the values of a BoundedEnum g can be computed as:

fromEnum bottom, fromEnum (succ bottom), fromEnum (succ (succ bottom)) ..., fromEnum top

That will be a sequence of contiguous integers.

I got caught by that one, too! But no, from what I can see, nothing in the laws guarantees that the integers are contiguous. It really surprised me!

See https://github.com/purescript/purescript-enums/pull/33#issuecomment-346425325

It's definitely one of my goals with this TC to try to achieve that. But I'm not sure I'm doing it right, or even actually doing it. I will think about the rest of your comments and see what I can come up with.

matthewleon commented 6 years ago

Also, I believe that fromInt could be defined on Cyclic and not just FiniteCyclic.

My problem with this is that Int is not really "the integers", but rather the set of 32-bit integers. Annoying and surprising things tend to happen when you try to make Int into a platonic integer.

Now, fromBigInt and toBigInt, on the other hand, I think could be reasonable. But then there's the question of whether you want that dependency.

matthewleon commented 6 years ago

Is the idea of FiniteCyclic to provide a more performant alternative to flip power generator?

Basically, yes. Still thinking about it, though. You've raised good points.

matthewleon commented 6 years ago

Also, it’s maybe worth considering whether a type class is the right encoding for this idea; since there is only one cyclic group of any given cardinality up to isomorphism, you could potentially argue that a concrete type makes more sense?

Perhaps what I really want here is a Newtype that creates a "free cyclic group" over any BoundedEnum, modeled on Group.Free.

matthewleon commented 6 years ago

Sorry, I should say a "free finite cyclic group", as from what I can see the free group in Group.Free is already cyclic.

hdgarrood commented 6 years ago

I think a free group is only cyclic when the set of generators has exactly one element - in which case it is isomorphic to the integers.

matthewleon commented 6 years ago

Closing this for now, as I think I've come up with a better solution to the problem that initially prompted me to open this. If someone has an objection, or something to add, I'll reopen.