I’d like to know if the status of the following is not yet done, working as intended, or bug (I couldn’t find a proper description on the dotty site):
EDIT just tried latest master (mybad was on the linker branch) and the following no longer makes sense
This works as expected:
val a: 42 = 42
val b: 42 = 24 //doesn't compile
val c: String | Int = 1
val d: String | Int = "str"
val e: String | Int = false //doesn't compile
But this doesn’t work as expected:
val a: 42 | 45 = 43 //compiles
val b: "This" | "That" = "what?" //compiles
Also, will intersection/union types allow us to do something like
def right[L, R](a: L | R): Option[R] = ...
def left[L, R](a: L | R): Option[L] = ...
?
I understand that then the question would arise that what is L and R for something like A|B|C so I don’t know if this would make sense. Anyway, I’d like to inquire.
Sorry if my update wasn’t clear enough, as per the latest master (of the day I posted that) it does not compile saying that singleton types can’t participate of union/intersection types (a pity too).
There are many valid solutions, and I expect type inference there would (have to) be rather incomplete. For another example, String = String | Nothing, so right("foo") can be inferred as right[String, Nothing]("foo").
For another example, since A | B = B | A, then (x: A | B) => right(x): Option[A] could be typed as (x: A | B) => right[B, A](x): Option[A].
Whether such solutions can be found at all (and whether all such solutions are found by Dotty) is an entirely different question, though.
This is issue #1551 in the dotty repo. The main problem with singleton types in union types is this:
If we allow them, then the least upper bound of x.type and y.type is x.type | y.type. Hence, in an
if-then-else
if (cond) x else y
this would be the type that’s computed for it. For nested if-then-elses or multiple branch match expressions the size of the type would grow linearly. This is simply not practical. It’s unclear what to do about it, since (a) the concept of least upper bounds is central to many aspects of Scala type inference, and (b) the concept is well-defined; it is what the name says it is, so one cannot mess with it and give it another meaning.
On the other hand, if we disallow unions over singletons then the least upper bound of x.type and y.type is simply the common underlying type of x and y, which is what one would expect it to be. Simple and effective. That’s why we opted for it. If there is another solution that is more general, but at the same time stays simple and clearly demonstrates that there are no issues with other type inference aspects we can still adopt it. But so far, no such solution is known.
Thanks for the answer everyone, I have now read the discussion in #1551 as well as the linked issues. If you don’t mind, this sprouts in me another question, when doing something like Some(1) the result is Some[Int] instead of Some[1], the compiler here is already choosing to widen the type (right?), so even if singleton types were allowed in union/intersection types, why would it not do the same in the case of the if-else (or match statement) and just widen it? or backwards, why would it not choose Some[1]?
@rcano Good question. When inferring instances of type variables, we demand that the inferred type is not a singleton type, so we widen implicitly.
There’s a possible solution here. Maybe we can leave the lub of x.type and y.type to be x.type | y.type, but redefine widen to operate not only on singleton types but on unions of singleton types as well. It would be good to think about this, and experiment whether it’s feasible (i.e. does not get too complicated, does not significantly slow down compilation time).
I definitely see how singleton types could get pretty out of hand if a whole bunch of them get combined. But it does seem like they lose some significant usefulness if they get squashed by type inference in a bunch of different situations. It would make the language larger, but maybe the programmer should be able to control whether widening happens or not? It kind of seems to call for some sort of meta-type that simply controls widening behavior. Then I suppose you could use union and intersection to apply or remove that meta-type.
