Type negation in Scala 3

Question

Is it possible to implement fail proof Not[A] type in Scala 3? Here is a question asked some years ago: how-can-i-have-a-negation-type-in-scala. Unfortunately, a solution based on 'not given A <:< B' fails if either is an abstract type: absence of evidence is not an evidence of absence fallacy. Technically, with macros, it should be possible to verify the type of the expression and produce an error if full type information is not known. However, I'd like it also to work not just when 'not A <:< B', but only if A with B is effectively Nothing: either type is sealed/final and not possible to mix into the other. On the other hand, in that scenario, full information about both types shouldn't be required: if A is final, any upper bound on B which is neither a type variable nor A should work.

Motivation:

sealed trait Marker
sealed trait A[X]
final class Special[X <: Marker] extends A[X]
final class Generic[X :Not[Marker]#Proof] extends A[X]

In the example above, If I have an a :A[Marker], then I know for sure that a.asInstanceOf[Special[Marker]] is sound.

Dmytro Mitin · Accepted Answer · 2023-04-10T18:09:59.370

The type class Not can't be defined with Scala 3 implicits. The ambiguity trick doesn't work any more. The semantics of implicit resolution changed. The ambiguity error is not propagated.

Difference between Scala 2 implicits and Scala 3 given/using (answer)

That's the reason why in Scala 3 Not (like Scala 2 shapeless.Refute) is built-in: scala.util.NotGiven

https://docs.scala-lang.org/scala3/reference/contextual/givens.html#negated-givens

https://docs.scala-lang.org/scala3/reference/changed-features/implicit-resolution.html

Not in all languages with type classes Not is possible. For example in Haskell it's impossible (with standard tools)

How do I conditionally declare an instance? (answer)

How to implement `Constraint` reflection? [Ad-Hoc polymorphism based on available Constraints]

Take action based on a type parameter's typeclass?

Can't code my component in a tagless-final way / using type classes and instances

You can try something like

import scala.util.NotGiven
import scala.compiletime.summonFrom

final class Generic[X](using (NotGiven[X <:< Marker] || IsAbstract[X])) extends A[X]

trait ||[A, B]
object ||:
  transparent inline given [A, B]: (A || B) =
    summonFrom {
      case _: A => new (A || B) {}
      case _: B => new (A || B) {}
    }

import scala.quoted.*

trait IsAbstract[X]
object IsAbstract:
  transparent inline given [X]: IsAbstract[X] = ${mkIsAbstractImpl[X]}

  def mkIsAbstractImpl[X: Type](using Quotes): Expr[IsAbstract[X]] =
    import quotes.reflect.*
    val tpe = TypeRepr.of[X]

    if tpe.typeSymbol.isAbstractType
    then '{new IsAbstract[X] {}}
    else report.errorAndAbort(s"${tpe.show} is not abstract")

The ordinary union type NotGiven[X <:< Marker] | IsAbstract[X] doesn't prioritize instances of type classes, so leads to ambiguity.

If necessary you can add IsSealed, IsFinal etc.

Great! I think though that `||` is unnecessary - I exactly wanted *both* `NotGiven[IsAbstract[X]]` and `NotGiven[X <:< Marker]` because that's a precaution against someone creating an object parameterized with an incompatible type in a generic context. I am a noob in Scala3 reflection though: doesn't `errorAndAbort` produce a compilation error, or does it only fail the implicit search? — Turin, Mar 23 '23 at 21:05
@Turin Ok, then you need `(using NotGiven[X <:< Marker], IsAbstract[X])` with comma. `errorAndAbort` produces a compilation error but in [transparent](https://docs.scala-lang.org/overviews/macros/implicits.html#blackbox-vs-whitebox) macro this only fails the implicit search (like [whitebox](https://docs.scala-lang.org/overviews/macros/blackbox-whitebox.html) macros in Scala 2). — Dmytro Mitin, Mar 23 '23 at 21:20
https://www.youtube.com/watch?v=HQojyuZK-Uo Scala 3: Anti-Givens by Rock the JVM — Dmytro Mitin, Apr 10 '23 at 18:06

Type negation in Scala 3

1 Answers1