Union types and generalisations

I think you confused & with |.

 A | ~A  =:=  Any
 A & ~A  =:=  Nothing

Apart from what @odersky already mentioned (that A & ~A =:= Nothing, not Any), I realize there may still be some issues with soundness. For example subtyping may complicate it pretty badly. And @Blaisorblade brought up an example on gitter of val x = new { type T = ~this.T }.

But even if it were only allowed in some positions – like type bounds on type parameters, for example – I think it could still be really useful. If it were only allowed in type parameter bounds, would there be any soundness holes?

You’re 100% correct! I was thinking ~ was a Group-like inverse function, but I assume that is the exact difference between an inverse and a complement.

So what are other axioms a potential ~ might follow?

Double negation? ~(~A) =:= A
De morgan? ~A & ~B =:= ~(A | B) and ~A | ~B =:= ~(A & B)

Very exciting! It would basically turn Scala’s type system into a boolean algebra.

1 Like

Wouldn’t that be an illegal cyclic reference even without the ~?
I don’t think
val x = new { type T = this.T } compiles in Scala today.

EDIT: confirmed it doesn’t compile in either Dotty 0.20.0-RC1 or Scala 2.13.1

I’m curious to see a use case, because I’m wondering what good it is to know that something is not of a given type.

1 Like

Lets make a practical example:
Lets define a trait Vehicle and create a class garage. Garage could then have a method that takes Vehicle ∩ ~Tank

2 Likes

There’s a use case at the top of this thread! I’ll rephrase it slightly:

trait Attempt[+E, +S] {
  def recover[E1 <: E, S1 <: S](fn: E1 => S1): Attempt[E & ~E1, S1] = ???
}

// this is an attempt that can fail with A or B or C and succeed with String
val x1: Attempt[A | B | C, String] = ???

// here we want to be able to infer that the x2 cannot fail with B, since it's been handled
// so it can only fail with A or C. We want Attempt[A | C, String] to be inferred.
val x2 = x1.recover[B](b => "Oh well.")

// here we want to infer that x3 cannot fail at all, since all possible failures have been handled.
// We want Attempt[Nothing, String] to be inferred.
val x3 = x2.recover[A | C](aOrC => "Dang.")

Another use case involves intersection types (phantom or otherwise):

// Some data type that carries some sort of properties at the type level
trait Data[+Props]

// Some sort of function that operates on those data types, which can
// require some properties of its input and assert properties on its output
trait MyFunction[-In, +Out] {
  // here there's a compile time assertion that the input satisfies the properties
  def apply(in: Data[In]): Data[Out]

  def andThen[In1 <: In, Out1](next: MyFunction[In1, Out1]): MyFunction[In1 & ~Out, Out & Out1]
}

// x1 requires properties A and B, and asserts properties C and D
val x1: MyFunction1[A & B, C & D] = ???

// x2 requires D and E.
val x2: MyFunction1[D & E, F] = ???

// we don't want the composition to require D, because it is already satisfied by x1.
// So we want the composition to require (A & B & D & E) & ~(C & D), which is A & B & E.
val x2 = x1 andThen x2

Edit: Just to mention, I talked about how we use something like the second example at ScalaDays, and it’s been quite useful. Currently we have to use a macro to eliminate already-satisfied schema properties from the composition, which works but isn’t ideal. A general purpose Not type operator would have tons of use cases beyond these!

1 Like

Why is that useful? Because the tank is too big? Looks like your garage still accepts a bucket-wheel excavator.

1 Like

@jeremyrsmith

In all examples you presented here assume a reduction of type parameters, here. Is this always possible?

If Vehicle is a saeled trait and an excavator is not defined, one can limit the input classes. This could be useful for entety management in games or similar usecases.

In cases where the type is sealed or a union type, one could, instead of using complement, define the desired type as a union of the other types.

A general ~T type constructor will probably not be very useful in a language that has open type hierarchies in an open world. To ever be able to answer true to the test S <: ~T, it is not sufficient that the test S <: T returns false. You must prove that there exists no U such that U <: S and U <: T. Unless S or T is final or sealed, or both are unrelated classes, you can’t do that.

However, note that in basically all mentioned use cases in this thread, ~T is actually used in a larger U & ~T. Since ~ cannot be made useful, can we build a U \ T type constructor that would provide most of the benefits of U & ~T? It couldn’t be equivalent of course (otherwise we could build ~T on top of it as ~T = Any \ T. But we can at least make it work for the use cases that have been mentioned here, mostly “removing” an alternative from a union. And that we can in fact do. At least we can do it for a fixed T:

def subtractT[R](x: R | T): R

taking advantage of type inference to infer a reasonably precise R. By construction, R >: (R | T) & ~T because the latter is also (R & ~T) | (T & ~T) = (R & ~T) | Nothing = R & ~T. Whether it is sufficiently precise for the rest of the program to typecheck is not guaranteed and depends on type inference, but we should be able to make it work for unions, and in any case I’m pretty sure it wouldn’t cause unsoundness (only impreciseness).

3 Likes

Yes! Exactly what I’m arguing is that this by itself is useful, i.e. a relative complement operator even if a full complement operator isn’t possible. It would certainly cover all the use cases I can think of. The only trick is that like you said, a relative complement in isolation would start to look a lot like a general complement operator if you can use it with a non-intersection (or non-union) type.

An interesting thing that I noticed is that IntelliJ’s separate typing algorithm already infers what I want in this case:

case class Foo[-In, +Out]() {
  def andThen[In1 <: In, Out1](next: Foo[In1 with Out, Out1]): Foo[In1, Out with Out1] = Foo()
}

val x1: Foo[A with B, C with D] = Foo()
val x2: Foo[C with D with E, F] = Foo()

// IntelliJ infers Foo[A with B with E, C with D with F]. Which is what I want
// Scala infers Foo[A with B with C with D with E, C with D with F]
val x3 = x1 andThen x2

Obviously it’s not that useful for IntelliJ to infer something that Scala doesn’t, but it’s the one case I’ve found where it infers something that I wish Scala would infer.

Edit: I guess the point being that even relative complement operator wouldn’t be necessary for this use case if somehow the minimal intersection type would be inferred.

2 Likes

And FWIW I know that this is a really edge use case, and just because someone is trying to do something crazy and it doesn’t quite work the way they want it to doesn’t mean that the language ought to support that use case. But I think there are other legitimate uses for such things, so I wouldn’t be the only one to appreciate it!

Type inference involving solving constraints with union or intersection types is tricky, because there’s more than one way possible sets of constraints we can pick and we can’t afford to backtrack in general, see https://github.com/lampepfl/dotty/blob/f1c701e4c14016e013635e232274aa685ea73edc/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1308-L1342
In the case of your subtractT, dotty actually does a pretty good job at eliminating the T from an arbitrary union but I’m confused about what this is supposed to achieve since its definition lets us typecheck the following:

def foo(x: T): Nothing =
  subtractT[Nothing](x)
1 Like

This is inferred as Foo[A & B & E, C & D & F] in Dotty already :). (but note the caveat about type inference and unions/intersections in my previous post, more complicated examples might not do what you want)

1 Like

You can only infer that if the type of x was T in the first place. I probably wasn’t clear but this would be used when x is of type A | T and then the result R would hopefully be inferred as A. If not it would at least be >= A. It couldn’t be Nothing.

That is true for a small collection of sub classes. But if we assume 10+ case classes, like one might do in a dsl, i would rather remove one class than specify n-1. This would also better describe intend.

People expected that soundness of not was straightforward, but that sort of cycle is allowed in DOT, and that’s enough to suspect that soundness of not is tricky.
Of course Dotty’s cycle detection might rule out all direct and indirect cycles ensuring soundness, but nobody has formalized that.
EDIT: whether that should stop you is not obvious; extensions without foundations exist, but need special attention.

I’m afraid that in Scala a constraint such as this would not be very useful in practice.

trait Vehicle
class Tank extends Vehicle

def enterGarage(v: Vehicle & ~Tank) = ???

val tank = new Tank
enterGarage(tank: Vehicle) // what now?

And also, if Vehicle <: (Vehicle & ~Tank) and Tank <: Vehicle shouldn’t that mean that Tank <: (Vehicle & ~Tank)? It could indeed work for sealed types if you say that Vehicle itself is not a subtype, but then complement types still don’t work in general. That sounds more like a shapeless-like typeclass than a firstclass typesystem concept.

3 Likes