Dotty: 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.

[alexknvl]

@Blaisorblade Yes, that works:

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

[Blaisorblade]

https://github.com/scalaz/scalaz-plugin/issues/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).

[pshirshov]

I've met similar problem on scala 2.12 and have a dirty workaround for it:

https://gist.github.com/pshirshov/1273add00d902a6cfebd72426d7ed758

So I'm wondering if it may be improved in dotty.

[Blaisorblade]

@pshirshov

To be short: val c: C, c.SOMETYPE value isn't equal to C#SOMETYPE. Moreover there is no any kind of relationship between them.

That is correct — if C#SOMETYPE is abstract (as in your example), then c.SOMETYPE could be anything, so it's unrelated to C#SOMETYPE; in particular, it isn't a subtype or supertype of C#SOMETYPE. You can have c1, c2: C such that c1.SOMETYPE = Int and c2.SOMETYPE = String, so C#SOMETYPE cannot be related to c.SOMETYPE.

In fact, C#SOMETYPE is highly problematic because it can lead the typechecker to conclude false typing relations, and Dotty will restrict its use.

In this case, it seems type projections are also pretty confusing; c.SOMETYPE is instead clearer, as it refers to the type members in c. While this isn't the motivation for the change, the restriction might help you in this way.

In your Problem.scala, it'd be nice to allow writing Super[c.IO] (not sure if it will happen), but if that doesn't work the better solution is to make IO a type member of Super, so that its definition can be specified in the body.

[smarter]

it'd be nice to allow writing Super[c.IO] (not sure if it will happen),

In fact, this is already allowed in Dotty.

[Blaisorblade]

Most of this issue discusses type projections in general — so the semantics proposed at https://github.com/lampepfl/dotty-feature-requests/issues/14#issuecomment-633778378 is relevant. In this proposal, a value v is in T#A if there exists a value w in T such that v is in w.A. To me, that resembles to t.A forSome {val t: T} (not using forAll).

In particular, unlike I thought, type projections are indeed covariant, per SLS 3.5.2:

"A type projection T#t conforms [<:] to U#t if T conforms to U."

However, I now wonder about SLS 3.2.12; that suggests that t.A forSome {val t: T} mean U#A forSome {type U <: T & Singleton}, which wouldn't help us — and worse, since Nothing <: T & Singleton, U could be Nothing