Ignore type parameters

[Adam-Vandervorst]

What do you do when a class/object is invariant under changes to a certain type parameter of its parent?
If you parameterise the child, then you can't use that same instance in multiple places (even though they're identical).
If you don't parameterise the child and use a wildcard, you run into variance issues.

Behold

enum BehavedValue[+A]:
  case Conflict
  case Value(a: A)
  case Nothing
import BehavedValue.*

trait AGC[A, B]:
  self =>
  val L: A => B
  val R: B => A

  def andThen[C](other: AGC[B, C]): AGC[A, C] = new AGC[A, C]:
    val L: A => C = self.L andThen other.L
    val R: C => A = other.R andThen self.R

  def opposite: AGC[B, A] = new AGC[B, A]:
    val L = self.R
    val R = self.L

object BooleanBehavedValue extends AGC[Boolean, BehavedValue[?]]:
  val L = {
    case true => Conflict
    case false => Nothing
  }
  val R = {
    case Conflict => true
    case _: Value[_] => true
    case Nothing => false
  }

class BehavedValueOptions[X](bot: Set[X]) extends AGC[BehavedValue[X], Set[X]]:
  val L = {
    case Conflict => Set() // top
    case Value(v) => Set(v) // coatom
    case Nothing => bot // bottom
  }
  val R = s => s.size match {
    case 0 => Nothing // bottom
    case 1 => Value(s.head) // coatom
    case _ => Conflict // top
  }

@main def example =
  val notNothing = BooleanBehavedValue.opposite
  val pickSingle = BehavedValueOptions(Set(1, 2, 3)).opposite
  val nonEmpty = pickSingle andThen notNothing
  //  val nonFull = whatMissing andThen notNothing
  // ... and many more

fails on the last line with

Found:    AGC[BehavedValue[?  ], Boolean]
Required: AGC[BehavedValue[Int], Boolean]

An asInstanceOf on the notNothing obviously resolves this, but that doesn't feel as correct approach here.

[s5bug]

To phrase in another way, Adam is looking for some type argument τ such that the following subtyping rules hold:

1. ∀α, Invariant[τ] <: Invariant[BehavedValue[α]] (desired behavior)
2. BehavedValue[Nothing] <: τ (lines case true => Conflict and case false => Nothing)

τ = ? <: BehavedValue[?] is close, but backwards on rule 1 and has issues with not being concrete for rule 2.

[s5bug]

If I have everything correct,

Here's a subtyping diagram:

As far as I can tell, it directly mirrors ?:

Here's what methods look like:

	ju.List[? >: T <: U]	ju.List[¿ >: T <: U]
get	Int => U	Int => T
add	T => Unit	U => Unit

The subtyping rules look like:

def wc[L, U, A >: L <: U]: (ju.List[A] <:< ju.List[? >: L <: U]) = summon

def cw[L, U, A >: L <: U]: (ju.List[¿ >: L <: U] <:< ju.List[A]) = summon

[s5bug]

The initial problem I see is that ? is equivalent to having an abstract type member, while ¿ doesn't seem to have any such equivalence.

Feedback from someone smarter than me about types would be much appreciated.

[s5bug]

It looks to be that ¿ >: L <: U is literally ? >: U <: L, based on the subtyping rules and the variance-substitution rules. If one collapses the horizontal strip in the 2nd subtyping diagram above, a pattern is discovered: along the TRBL diagonal, the lower bound changes, and along the TLBR diagonal, the upper bound changes. Extending this below when the wildcard can actually be inhabited yields the following result:

This matches up with Adam's insight that the type parameter is ignored: there are no types within ? >: U <: L when L <: U.

Scala does not like this:

Of course, if one were to have

object Foo extends I[? >: Any <: Nothing]

one could do

Foo match {
  case _: I[t] =>

and get a type t which is both a supertype of Any and a subtype of Nothing.

This would mean you have an Any <:< t and a t <:< Nothing, which can be composed to get an Any <:< Nothing, which is obviously not correct.

Case closed as unsound? Or is it still possible to have a ¿, by solving the type variable problem?

[s5bug]

If we travel back to Scala 2 land for a moment, and rewrite ? as a forSome clause, essentially the behavior wanted by Adam is one of a forAll clause.

object BooleanBehavedValue extends (AGC[Boolean, BehavedValue[α]] forAll { type α })

If we suppose that polymorphic values exist (denoted here by parameterless polymorphic functions), we get the following subtyping:

What I still haven't figured out is, if we were to have polymorphic values, given something like

object Bar extends ([A <: Foo] => I[A])

what properties would t have in

Bar match {
  case _: Foo[t] =>

?

[s5bug]

A discussion was sparked in the Scala Discord yesterday about how to make GADT cases "valid" for multiple types. That is

trait X[T]
object Foo extends X[Fruit], X[Animal]

I suggested

trait X2[-R, +L <: R]
object Foo extends X2[Fruit | Animal, Fruit & Animal]

type X[a] = X2[a, a]

which did work

def acceptXFruit(xf: X[Fruit]): Unit = ()
def acceptXAnimal(xa: X[Animal]): Unit = ()

acceptXFruit(Foo) // => ()
acceptXAnimal(Foo) // => ()

And then I had a brain-blast: essentially, we can emulate the nature of ¿ or a forall by using the opposites of the reduction rules of wildcards:

object BooleanBehavedValue extends AGC[Boolean, Boolean, BehavedValue[Nothing], BehavedValue[Any]]

@Adam-Vandervorst ended up finishing the concept, making it compile with the rest of his code: https://scastie.scala-lang.org/5TXfm2B9Sw2N0ZqDkEEmsA

So, while it's impossible to add forall support to arbitrary objects, one can hack it in to self-made objects.

[som-snytt]

Reminiscent of https://en.wikipedia.org/wiki/The_Tholian_Web