[RFC] Lattice foundation

[sideeffffect]

This is the foundation to have Lattice (and the whole family, like Distributive lattice, ...) 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/lattice/docs/overview/diagrams.md (named JoinMeet)
More is still to come, other laws, comments/documentation and instances for more types, currently there is just Set[A] to try things out.
I would be interested in your feedback 😃

/cc @adamgfraser @jdegoes

There are some similarities to Ring-like structures, which are discussed in this PR #351 so maybe we can gain something when we will be able how the design decisions play out in both Type class hierarchies.

[sideeffffect]

Hello @adamgfraser, @jdegoes, @lemastero and anybody else involved.
I would like to revive this PR that attempts to add lattice structure to ZIO Prelude. Surely, lattice-like structures are not as omnipresent as Associative, but I still suspect that they will often come up in domain/business modelling and similar situations, so they would be good fit for zio-prelude-experimental for the beginning.

The issues here is how we represent Latices in ZIO Prelude. In contrast to for example Associative, we have here 5 independent laws with no clear candidate that should be at the top of the hierarchy. Namely

• Absorption
  • a1 vvv (a1 ^^^ a2) === a1
  • a1 ^^^ (a1 vvv a2) === a1
• DistributiveJoinMeet
  • a1 vvv (a2 ^^^ a3) === (a1 vvv a2) ^^^ (a1 vvv a3)
  • a1 ^^^ (a2 vvv a3) === (a1 ^^^ a2) vvv (a1 ^^^ a3)
• Involution
  • !(!a) === a
• ExcludedMiddle
  • !a vvv a === 1
• Noncontradiction
  • !a ^^^ a === 0

After a whole year I wasn't able to come up with any breakthrough, the options are still:

1. Have an interface at the top of the hierarchy, but only as a mere vessel for signature of the methods, a "shape": JoinMeetShape. The type class instances will be defined in its companion objects. There are also other shapes: TopShape, BottomShape and ComplementShape (the current state of the PR)
2. Have no top interface whatsoever or any shapes at all. The structures (Absorption, DistributiveJoinMeet, ...) will be just independent traits. But where would the type class instances go to? Should we have them across all 5 companion objects?
3. Pick a structure that will be at the top. But which one? This feels like an arbitrary decision with no good candidate.

So how do we get out of this pickle? I would appreciate any help or advice. Btw I think it would be better to come to a conclusion on this PR first and only then finish #351, because here the challenges are more general.

[adamgfraser]

@sideeffffect I would be inclined to go with your second option and use our functionality for coherent types to make the appropriate instances available when working with any of the types. We could then define type aliases for common intersections of these different types.

[sideeffffect]

I explored the option (2) and here are my findings

1. Shapes are gone, this is a simplification, at least in a certain sense. 👍
2. The code exploded a bit. Because there are no Shapes, there is significant duplication of code. It's not just method signatures, but also Syntax/Ops, etc. Maybe even the type class instances would have to be duplicated to each companion object. 👎
3. We don't have any means to describe a General Lattice. It used to be JoinMeetShape.Aux[A, Semilattice, Semilattice], but JoinMeetShape is no more. 👎
4. Here's the code, if you'd like to have a look yourself: sideeffffect/zio-prelude@lattice...sideeffffect:lattice-without-shapes

[adamgfraser]

I think this is definitely on the right track.

I would define something like:

type Lattice[A] = Associative[Max[A]] with Associative[Min[A]]

I realize you defined it in terms of Or and And. If you do that I would generalize Or and And so we don't need the OrF and AndF stuff. Then you can just implement a LatticeSyntax trait that implements the syntax that does not depend on specific laws about how these operators relate to each other.

[sideeffffect]

type Lattice[A] = Associative[Max[A]] with Associative[Min[A]]

How could this help us? 🤔 What would be the signature of combine? combine(l: => Max[A] with Min[A], r: => Max[A] with Min[A]): Max[A] with Min[A]? But for a lattice, we need distinct methods join and meet.

I would generalize Or and And so we don't need the OrF and AndF stuff

I'm not entirely sure what you mean. Are you suggesting to rename OrF and AndF to Or and And and replace previous uses of Or and And to Or[Boolean] and And[Boolean] -- in zio-prelude-core?

[adamgfraser]

package zio.prelude

import zio.prelude.newtypes._

object Example {

  implicit final class LatticeSyntax[A](private val self: A) extends AnyVal {
    def join(that: A)(implicit ev1: Associative[Max[A]], ev2: Associative[Min[A]]): A =
      ev1.combine(Max(self), Max(that))
    def meet(that: A)(implicit ev1: Associative[Max[A]], ev2: Associative[Min[A]]): A =
      ev2.combine(Min(self), Min(that))
  }
}

[sideeffffect]

🎉 🎉 🎉
I've made a breakthrough!

It's been in from of my eyes the whole time. To my defense, I'm not a mathematician... And not an attentive reader.

As per https://en.wikipedia.org/wiki/Lattice_(order)#General_lattice

The absorption laws, the only axioms above in which both meet and join appear, distinguish a lattice from an arbitrary pair of semilattice structures and assure that the two semilattices interact appropriately.

That means we can describe a lattice with our Absorption and that makes it the natural top of our hierarchy. I've already made other traits inherit from Absorption and removed all the Shapes. I have a good feeling about this, the pieces are finally coming together.

Please have a new look at the code now, Adam 🙏

[adamgfraser]

Big improvement!

The main source of complexity we should try to eliminate at this point is the use of path dependent types.

Here is one potential approach:

package zio.prelude.experimental

trait Absorption[A] {
  def join(l: => A, r: => A): A
  def meet(l: => A, r: => A): A
}

object Absorption {

  /**
   * Summons an implicit `Absorption[A]`.
   */
  def apply[A](implicit absorption: Absorption[A]): Absorption[A] =
    absorption

  implicit lazy val BoolInstance: Absorption[Boolean] =
    new Absorption[Boolean] {
      override def join(l: => Boolean, r: => Boolean): Boolean = l || r
      override def meet(l: => Boolean, r: => Boolean): Boolean = l && r
    }

  implicit def SetInstance[A]: Absorption[Set[A]] =
    new Absorption[Set[A]] {
      override def join(l: => Set[A], r: => Set[A]): Set[A] = l | r
      override def meet(l: => Set[A], r: => Set[A]): Set[A] = l & r
    }
}

trait AbsorptionSyntax {

  /**
   * Provides infix syntax for joining or meeting two values.
   */
  implicit class AbsorptionOps[A](private val l: A) {

    /**
     * A symbolic alias for `join`.
     */
    def vvv(r: => A)(implicit absorption: Absorption[A]): A =
      absorption.join(l, r)

    /**
     * Join two values.
     */
    def join(r: => A)(implicit absorption: Absorption[A]): A =
      absorption.join(l, r)

    /**
     * A symbolic alias for `meet`.
     */
    def ^^^(r: => A)(implicit absorption: Absorption[A]): A =
      absorption.meet(l, r)

    /**
     * Meet two values.
     */
    def meet(r: => A)(implicit absorption: Absorption[A]): A =
      absorption.meet(l, r)
  }
}

[sideeffffect]

I'm not convinced that we want to drop type members. I originally added them at the suggestion of @jdegoes, btw:
#351 (comment)
#351 (comment)

They are a big part of the modularity and expressivity story of the current design. Let's take this example:

type BoundedLattice[A] = Absorption.Aux[A, BoundedSemilattice, BoundedSemilattice]

type OrthoComplementedLattice[A] = ExcludedMiddle[A] with Involution[A] with Noncontradiction[A] {
  type Join[x] = BoundedSemilattice[x]
  type Meet[x] = BoundedSemilattice[x]
}

type Ring[A]     = Semiring[A] with Subtract[A] {
  type Addition[x] <: AbelianGroup[x]
  type Multiplication[x] <: Monoid[x]
}

Here we say that a BoundedLattice is an Absorption where both Join and Meet form a BoundedSemilattice. But there could be exemplars of BoundedLattice where they satisfy more strict laws (subtype of Absorption) or where their Join or Meet satisfy stricter laws (subtypes of BoundedSemilattice). And all of these exeplars would be valid BoundedLattice.

Or OrthoComplementedLattice satisfies ExcludedMiddle, Involution and Noncontradiction (and thus Absorption), but that's not enough, its Join and Meet both have to form BoundedSemilattice. But there could be a useful exemplar of a structure that satisfies ExcludedMiddle, Involution and Noncontradiction, but either Join or Meet (or both) are mere Semilattice. And that would be a different thing from OrthoComplementedLattice, right?

Or if we take an example from the Ring PR: Ring is a Semiring where its Addition forms AbelianGroup and its Multiplication forms Monoid. (Or anythign that is more strict/specific than that.) But we have the freedom to define a structure which is a Semiring with Multiplication that is PartialInverse.

With type members, we have this LEGO where we can assemble the pieces as we want, they allow for a very modular design. Scala's type system here allows us to express these structures very closely how they are in mathematics, which is great IMHO. Type members are also nice that, in contrast to type parameters, don't get in the way and have to interact with them only if you want to. I hope that this modularity will allow us to avoid making special case for everything, like you and @jdegoes talked about here

Wouldn't you be worried that without the design with type members, we would loose the benefits outlined above?

[adamgfraser]

Right. I think the question is whether you want to specify those properties as part of one type alias or not.

You could think of these abstractions as really describing three separate things: (1) the properties of some "maximum" operation, (2) the properties of some "minimum" operation, (3) the laws that describe how those two operations should relate to each other.

So then the question is should this abstraction describe (1) or (1), (2), and (3).

You could imagine a method like:

def foo[A](implicit max: Identity[Max[A]], min:  Associative[Min[A]], excludedMiddle: ExcludedMiddle[A]) = ???

Here you have arguably quite a precise and modular way of specifying what properties you need for the "join" operator, what properties you need for the "meet" operator, and how those two should relate together. This has the benefit of being simpler in some ways since there are no path dependent types and you are just requiring one or more capabilities as we do elsewhere.

The disadvantage is that there is no "one type" for some of these abstractions. Being one of them just is having these two operations and having them relate to each other in a particular way. In a way that is perhaps more fundamental (there is nothing "more" to these structures than having these two operations and having them relate to each other in a particular way) but it is also nice to have a reification of that.

I do worry that this adds a level of complexity beyond what we have used elsewhere in this library and I would be concerned about introducing it to teams that I would use other features of ZIO Prelude for. At the same time, these abstractions are inherently more esoteric and this is the experimental package so perhaps that is appropriate.

I'm good with whatever approach you want to take but would just suggest you consider the complexity costs here and consider if there are ways to express these ideas that would be more accessible while reflecting their underlying structure.

[sideeffffect]

Adam, please have another look.
I've implemented the simplified approach you suggested above.
Let's see how it will work. If it will turn out we need it, we can bring the reified model back.

[adamgfraser]

Sounds good. Let's get this in and then I agree we will have to see how it works.

[sideeffffect]

🎉 🎉 🎉
❤️