zio-prelude icon indicating copy to clipboard operation
zio-prelude copied to clipboard

[RFC] Preliminary work to bring Ring-like structures to ZIO Prelude

Open sideeffffect opened this issue 3 years ago • 15 comments

This is the foundation to have Ring (and the whole family, like Semiring, Field, ...) algebraic structures and instances for Scala library/ZIO types. You can see the skeleton of the hierarchy here: https://github.com/sideeffffect/zio-prelude/blob/ring/docs/overview/diagrams.md (named AddMultiply) More is still to come, mainly comments/documentation and the instances for more types, currently there is just Int and Double to try things out. I would be interested in your feedback :smiley:

/cc @adamgfraser @jdegoes

sideeffffect avatar Oct 23 '20 13:10 sideeffffect

I think the cornerstone of this hierarchy should be Distributive (a semiring), in keeping with other naming conventions.

In addition, a distributive is really a pair of other binary operators that satisfy certain laws. So that would argue the type class itself should contain a proof of those, possibly in the form of instances for the other two binary operators.

In fact, maybe there's some encoding where a type class is parameterized by the properties of the two binary operators, e.g.:

trait Distributive[Add[x] <: Associative[x], Multiply[x] <: Associative[x], A] {
  def add: Add[A]
  def multiply: Multiply[A]
}

jdegoes avatar Oct 23 '20 17:10 jdegoes

Thanks John for looking at this! If we look at DistributiveMultiply, we can see that it this will indeed be the most useful type class for most users' needs. But I wanted to be able to express a general Semiring. For this, a mere

DistributiveMultiply[A, Addition = CommutativeMonoid, Multiplication = Identity]

isn't enough. There is also another law specifying that 0 (neutral element for addition) annihilates when used in multiplication. This is where AnnihilatingZero comes into play, for Semiring, it is

AnnihilatingZero[A, Addition = CommutativeMonoid, Multiplication = Identity]

Both DistributiveMultiply and AnnihilatingZero share a common structure, they need to allow two operations: addition and multiplication, where each may satisfy some laws. This shared structure is captured in AddMultiply, which doesn't constrain these two operations besides being Associative (which is the top of its hierarchy).

(I opted for more verbose DistributiveMultiply, because there is another distributive comming, a DistributiveJoinMeet, when we will be adding Lattices & co.)

Does that make sense?


Btw one thing I was considering is whether the Addition and Multiplication proofs should be straight on A

  def Addition: Addition[A]
  def Multiplication: Multiplication[A]

but I settled on Sum/Prod

  def Addition: Addition[Sum[A]]
  def Multiplication: Multiplication[Prod[A]]

The reason is that since "adding" and "multiplying" the vales are both valid ways of combining them, us (ZIO Prelude developers) and our users, will defined Type class instances not directly on As, but in terms of Sum/Prod and will be able to directly reuse them here. There are helper methods add/multiply, which can be overridden to enable more efficient implementation (bypassing the apply and unwrap methods on Sum/Prod).

sideeffffect avatar Oct 26 '20 01:10 sideeffffect

I've reworked the proposal a bit, can you @jdegoes have another look, please?

One can start by having a look at the diagram (linked in the PR description). Now, there are only DistributiveMultiply and AnnihilatingZero as prominent type classes with laws.

The other traits were demoted to mere "Shape" traits. These are just helper traits containing some useful type parameters and/or methods. But otherwise, they're not considered Type classes, because they don't come with any interesting properties (i.e. laws), maybe besides that the operation(s) implemented by their method(s) are total. I've borrowed the term from this ticket https://github.com/lampepfl/dotty/issues/9028 (which borrows it from the Getting F-Bounded Polymorphism into Shape paper).

I think this move was a great improvement, because it keeps with the ZIO Prelude principle that each Type class must come with a set of laws. One way of looking at it is that the (nominal) type of the Type class trait is the law(s). We double down on deconstructing things and composing them (these individual laws) horizontally via Scala's intersection types, instead of creating vertical hierarchies (like in Haskell/ScalaZ/Cats).

sideeffffect avatar Oct 28 '20 23:10 sideeffffect

Following up on a conversation @sideeffffect and I had today, I think one encoding of this we could explore is:

package zio.prelude

trait Semiring[A] {
  def add(a1: A, a2: A): A
  def multiply(a1: A, a2: A): A
}

object Semiring {

  val laws = ???
  // Distributive law

  implicit def derive(implicit sum: Associative[Sum[A]], product: Product[A]): Semiring[A] =
    new Semiring[A] {
      def add(a1: A, a2: A): A
      def multiply(a1: A, a2: A): A
    }
}

trait SemiringWithIdentity[A] extends Semiring {
  def identity: A
}

object SemiringWithIdentity {

  val laws = ???
  // annihilation

  implicit def derive(implicit sum: Inverse[Sum[A]], product: Product[A]): SemiringWithIdentity[A] =
    ???
}

The idea is that we should be able to derive a Semiring where multiplication distributes over addition given an Associative[Sum[A]] and an Associative[Prod[A]]. Similarly we should be able to derive a version where there is also a zero element whenever we have an Associative[Inverse[A]] and an Associative[Prod[A]].

I don't think this adds functionality beyond what you already have but it would be significantly simpler (no type members, no Aux pattern, etc...). I also like it conceptually in that it makes the individual binary operations fundamental and then this type class just describes that there are two binary operations that are related in a certain way. It also avoids the need for any new implementations of the type classes because we can just delegate to the existing instances.

One consideration is that the validity of the instances here depend on the validity of the instances that the user defines for Sum and Prod. For example it would be possible to implement versions of Sum and Prod that don't satisfy the laws, say by implementing Sum in terms of multiplication and Prod in terms of addition. But I think it is fine to say that an erroneous definition. If you are going to define instances of Sum and Prod for the same type then those should relate to each other in the way we would expect in terms of multiplication distributing. If that is true then this derivation is valid.

adamgfraser avatar Nov 21 '20 19:11 adamgfraser

@adamgfraser I like this SOOO much more and hope it works out.

jdegoes avatar Dec 15 '20 03:12 jdegoes

@sideeffffect Did you get a chance to explore this more? Do you want me to try to flesh it out?

adamgfraser avatar Dec 15 '20 03:12 adamgfraser

Other comments:

  • We still need to think about names
  • Technically the mere existence of product and sum should not necessarily imply that products distribute over sums, perhaps, but we could solve that if we wanted to with a no-op type class such as:
    trait Distributive[A]
    object Distributive extends Lawful[...] { ... }
    
    Then merely "declaring" a distributive for some type, together with the sum and product, would derive the distributive. Maybe even the distributive would contain the add / multiply inside them. But all sum / product operations would go through the sum / product new types.
  • We should have special case combine operators, one for product, and one for sum. These would "go through" the appropriate newtypes

jdegoes avatar Dec 15 '20 04:12 jdegoes

I've implemented the PartialInverse. I will need more time to think through and implement the other ideas you guys have suggested. Hopefully I will have more time to spend on this in the near future.

sideeffffect avatar Dec 16 '20 01:12 sideeffffect

I have greatly simplified this and implemented DistributiveMultiply as the top of the hierarchy.

sideeffffect avatar Oct 25 '21 01:10 sideeffffect

@jdegoes can you please give this another look? Me and @adamgfraser have come up with a simplified approach to this. The algebraic structures, like Ring, are not reified, we only have type classes for the interaction between sum and prod, but the advantage is that it is much simpler, because there are no type members.

We can bring in additional structure via a trick like this:

def foo[A](implicit distributiveProd: DistributiveProd[A], sum: AbelianGroup[Sum[A]], prod:  Identity[Prod[A]]) = ???

What do you think?

sideeffffect avatar Oct 29 '21 10:10 sideeffffect

I can imagine you guys are super busy with ZIO 2 right now, but is there something I can do to help this move forward? @jdegoes @adamgfraser

sideeffffect avatar Nov 24 '21 00:11 sideeffffect

@sideeffffect I'm good with merging this into the experimental package. Can we move everything in there? Looks like there is still some stuff in core.

adamgfraser avatar Nov 24 '21 01:11 adamgfraser

Unfortunately, for this Ring-like thing to work, PartialInverse is necessary and that needs to live in core. Do you have concerns about any particular change in core that I could fix?

sideeffffect avatar Nov 24 '21 09:11 sideeffffect

Okay. Let me look in more detail. My concern is more about overall increase in complexity of the hierarchy for core functional abstractions by adding new ones that I think largely only have applicability in the math context (you basically want to describe division).

adamgfraser avatar Nov 24 '21 13:11 adamgfraser

@adamgfraser Agree with Adam! Would be good to get this in, and just under an experimental package so we have the flexibility to evaluate it for a while. Thank you for your persistence on this!

jdegoes avatar Nov 25 '21 22:11 jdegoes

I know this has literally been years, but I'd appreciate if any interested parties could have another look at this :pray:

sideeffffect avatar May 08 '24 00:05 sideeffffect

/cc @kyri-petrou

sideeffffect avatar May 11 '24 00:05 sideeffffect

@sideeffffect I'm not sure I'm the best person to review this because my understanding of algebras is basic at best.

Are there any specific parts of the code you'd like me to focus on?

kyri-petrou avatar May 11 '24 06:05 kyri-petrou

The most important thing to check is that it doesn't break any thing in the non-experimental parts. So if some match in the experimental part is "broken", doesn't really matter that much. We can always fix it later. The experimental parts are wild-west with not backward guarantees, but wouldn't want to release ZIO Prelude 1.0 with broken non-experimental parts. I'll double check tomorrow. But if somebody feels brave, you can also check it yourself.

After this is merged, it would be wise to release another RC and give some time for people to test it out. Only after that, we should release 1.0.0. Does that sound good @ghostdogpr ?

sideeffffect avatar May 11 '24 20:05 sideeffffect

Sounds good 👍

ghostdogpr avatar May 11 '24 22:05 ghostdogpr

I'll need one more approval and then let's merge :muscle:

sideeffffect avatar May 12 '24 17:05 sideeffffect