Singleton bound and type projections don't play nice with each other

[Blaisorblade]

If a value tasty has abstract type T and T is marked as being a singleton type (that is, currently, T <: Singleton), I’d expect tasty.type = T, because both types are singleton that contain tasty. This currently fails in Scalac and Dotty (the Scala report is scala/bug#10905 — this is a copy, with Scalac output swapped with Dotty output).

A minimized example:

scala> trait A { type T; val prod: T; val cons: T => Int = _ => 0 }; trait Foo { type U <: Singleton with A; val tasty: U }
// defined trait A
// defined trait Foo

scala> val v: A = new A { type T = Int; val prod: T = 1}; val u: Foo = new Foo { type U = v.type; val tasty: U = v }
val v: A = anon$1@5416f8db
val u: Foo = anon$2@64e1377c

scala> u.tasty.cons(u.tasty.prod: u.U#T)
1 |u.tasty.cons(u.tasty.prod: u.U#T)
  |             ^^^^^^^^^^^^^^^^^^^
  |             found:    u.U#T
  |             required: u.tasty.T
  |

/cc @milessabin

Background

I ran into this while prototyping a heavily path-dependent API in Dotty (an early version of Tasty reflection), in relation to https://github.com/lampepfl/dotty/pull/4577/files/b315dbfa9f2d206cc26da75779388fca98faaabd#r191016341; the workaround involved turning defs into vals, which I suspect is acceptable here but potentially annoying when trying to save memory.

Alternatives

For the example above, enabling the definition of idempotent methods might be more general, if we ever get there.

Soundness

Not formally investigated, since nobody yet added to DOT either singleton types, type projections or singleton type variables.

[milessabin]

Is there a clear statement of the intended semantics of type projections, in Dotty or in DOT?

My intuitions in Scala were always that T#U ought to mean something like t.U forAll { val t: T } if there were such a thing as a forAll construct. But the implementation in Scala never aligned with that.

[Blaisorblade]

Is there a clear statement of the intended semantics of type projections, in Dotty or in DOT?

Nothing fully satisfactory, but something exists — the 2003 nuObj paper is a good starting point and describes the intended semantics, but some of its rules break down in the presence of lower bounds. What's below are pretty educated guesses.

DOT has no type projections, which is why I didn't state my guess, but the Scala 2 implementation is supposed to be based on nuObj, the calculus in A Nominal Theory of Objects with Dependent Types, which does have type projections (called type selection). nuObj has no lower bounds, which avoids all the bad bounds issues in DOT, so type projections were no problem at all.

Then the SLS 3.5.1 and 3.5.2 have cases for type projections. 3.5.1 is vague but can be read correctly.
OTOH 3.5.2 makes me wonder. "A type projection T#t conforms [<:] to U#t if T conforms to U." seems both insufficient (no upper bounds??) and very unlikely to be sound — I don't see it in the paper and it's false under the "existential" semantics we're discussing (see below).

My intuitions in Scala were always that T#U ought to mean something like t.U forAll { val t: T } if there were such a thing as a forAll construct. But the implementation in Scala never aligned with that.

My intuition/conjectures agree, but it's neither forAll nor forSome IMHO: to me T#A is an abstract type between its bounds. More precisely, if T contains definition type A >: S <: U (and treating type A = Z as type A >: Z <: Z), and some non-null value of T exists (proving that S <: A <: U aren't bad bounds), then S <: T#A <: U. But that doesn't support SLS 3.5.2: if T <: U1, T#A and U1#A are both abstract. T#A has an "interval kind" no larger than U1#A, but since T#A is abstract, U is its least supertype (indeed, the nuObj paper talks about tight upper bounds).

EDITED: Instead, t.A forAll { val t: T } contains the values that inhabit t.A for all t (according to the semantics @TomasMikula proposed, and to semantics of forall in PER models), that is, it's the intersection of t.A over all t, and it is equal to S, and t.A forSome { val t: T } contains the values that inhabit t.A for some t, that is it's the union of t.A for all t, and it is equal to U.

Formally, the crucial rules in the nuObj paper are (Alias-=) in Sec. 4.2, (Tsel-\prec (strange <)) in 4.3, (Tsel-<:) in 4.4. They all refer to membership in (Other-\in) in Sec. 4.1, which does introduce an existential x: T. Since there are no lower bounds, those rules can only show T#A <: U (in case A's decl is type A >: S <: U) or T#A = Z (in case A's decl is type A = Z), but not T#A >: S.

[milessabin]

By t.A forAll { val t: T } I intended the intersection of the As for all t: T, not the union. I'm not 100% sure, but I think that aligns with your suggestion of "an abstract type between its bounds".

[Blaisorblade]

@milessabin That's what I meant but miswrote, I tried to edit the paragraph to clarify.
But separately from type projections, if tasty.type = T (as in the OP), it should follow that tasty.type#U = T#U — and that would be validated by the semantics we discuss, unlike the rule in SLS 3.5.2.

Proposed new clauses:
SLS 3.5.1:

A type projection T#t is equivalent to U#t if T is equivalent to U.

SLS 3.5.2:

A type projection T#t conforms to U#t if T is equivalent to U. [not if T conforms to U].

BTW, the above seems to also work for Scala 2 nested classes, tho I haven't thought about that as much and they definitely don't fit the DOT semantics of type members.

[milessabin]

I think the switch from conforms to equivalent helps here, otherwise I could imagine doing bad things with (empty) intersections of singletons. And, yes, I agree that if tasty.type = T it should follow that tasty.type#U = T#U ... if we can't have referential transparency at the type level, where can we have it? ;-)

[Blaisorblade]

And, yes, I agree that if tasty.type = T it should follow that tasty.type#U = T#U ... if we can't have referential transparency at the type level, where can we have it? ;-)

Yeah that seems uncontroversial. Actually, spelling out that rule is unnecessary, because the SLS declares equivalence to be a "congruence" — while the spec explanation is cryptic, congruence does mean that A = B implies C[A] = C[B] for all contexts C (that is, types with holes).

The tricky question that stands is whether tasty.type = T in the first place, but I'm gonna say "yes".
However, if we did that we'd risk making an existing bug more painful. As @alexknvl pointed out, rules for union types show that A <: Singleton and B <: Singleton then A | B <: Singleton, which should be false, so singleton type variables can't be marked with bounds (A >: Singleton would have the same problem with intersections). We try to reject a.type | b.type, but I expect one can write A | B and only later instantiate A and B with singletons.

[sir-wabbit]

@Blaisorblade Yes, that works:

type || [A, B] = A | B
type Boo = 0 || 1

[Blaisorblade]

scalaz/scalaz-plugin#17 requests a similar feature and points out problems with null, since it inhabits singleton types — which it ideally shouldn't? If tasty: X and X <: Singleton but tasty = null, tasty.type isn't X. That's annoying.

Since we plan to forbid x.A for x = null if we get null tracking, we could think about (1) making singletons non-nullable (yay!), which would fix the issue; (2) forbidding x.type for x null (not needed for this issue, but seems highly questionable and a way to get back in x.A for x null).