Projection type paths can't traverse singleton types

[swaldman]

Compiler version

3.3.1

Minimized code (scala-cli scipts)

I'd like to have a type that expresses any Outer's Foo.Data. Two logical approaches fail.

//> using scala 3.3.1

class Outer:
  object Foo:
    case class Data(s : String)
  case class Foo( count : Int )

// type AnyData = Outer#Foo.Data
//
// if uncommented...
//   [error] ./cant-traverse-type.scala:8:25
//   [error] end of toplevel definition expected but '.' found
//   [error] type AnyData = Outer#Foo.Data

// type AnyData = Outer#Foo.type#Data
//
// if uncommented
//   [error] ./cant-traverse-type.scala:15:25
//   [error] end of toplevel definition expected but '.' found
//   [error] type AnyData = Outer#Foo.type#Data

I thought that the issue might only be a parser issue with . in the type projection paths, so tried a "bridge" workaround. The type alias declaration succeeds! Unfortunately, the compiler is unable to prove that the expected projections conform.

//> using scala 3.3.1
//> using option -explain

class Outer:
  object Foo:
    case class Data(s: String)
  case class Foo(count: Int)
  type FooData = Foo.Data

type AnyData = Outer#FooData // yay! compiles!

val o   = new Outer
val ofd = new o.Foo.Data("Hello!")

// val ad : AnyData = ofd
//
// if uncommented
//  [error] ./cant-traverse-bridge.scala:15:20
//  [error] Found:    (ofd : o.Foo.Data)
//  [error] Required: AnyData
//  [error] 
//  [error] Explanation
//  [error] ===========
//  [error] 
//  [error] Tree: ofd
//  [error] I tried to show that
//  [error]   (ofd : o.Foo.Data)
//  [error] conforms to
//  [error]   AnyData
//  [error] but the comparison trace ended with `false`:
//  [error] 
//  [error]   ==> (ofd : o.Foo.Data)  <:  AnyData
//  [error]     ==> (ofd : o.Foo.Data)  <:  Outer#FooData
//  [error]       ==> o.Foo.Data  <:  Outer#FooData (left is approximated)
//  [error]       <== o.Foo.Data  <:  Outer#FooData (left is approximated) = false
//  [error]     <== (ofd : o.Foo.Data)  <:  Outer#FooData = false
//  [error]   <== (ofd : o.Foo.Data)  <:  AnyData = false
//  [error] 
//  [error] The tests were made under the empty constraint
//  [error] val ad : AnyData = ofd
//  [error]                    ^^^

val ad : AnyData = ofd.asInstanceOf[AnyData] // compiles, but only with explicit cast

@main
def spew = println( ad.s ) // prints without error

Expectation

I expect that I'd be able to write a projection type that would abstract over the dependent singleton type Foo. (In real life, I just want to write some functions accepting nested dependent classes and generate reports that would not depend on the identity of the enclosing instance.)

As shown, with the type-alias bridge, I can successfully cast to a projection type and work without. But the compiler can't recognize the conformity of the type without the cast.

Thanks!

Thanks to Alexandru Nedelcu, Aly, and SlowBrain on the Scala discord for helping me work through this.

[bishabosha]

@sjrd asking for opinion on subtyping theory here

[sjrd]

I believe the behavior of the compiler is correct.

Remember that type projections in Scala 3 are not nearly as powerful as in Scala 2. In A#T, A must be a concrete (realizable) type, so that A#T uniquely identifies one type. Then, relationships between A#T are basically tested in terms of the alias that A#T can reduce to. As an exception, when T is a class type designator, some more rules apply.

On the other hand, we have path-dependent types p.x. For those, p must be a valid prefix, which also means being stable. Since A#T is never stable, (A#T).x would make no sense, and is therefore rejected by the parser. With your alias, you're creating something more like A#(T.x). But that doesn't make sense either, and won't lead to any subtyping rule applying. Arguably, that one should be eagerly rejected, but maybe doing so would cause cyclic reference errors.

Note that type FooData = Foo.Data resolves to type FooData = Outer.this.Foo.Data, which is a perfectly valid type. But then when doing Outer#FooData, in order for the type system to make sense of it, it needs to compute asSeenFrom(Outer, Outer.this.Foo.Data, Outer). That is not possible because Outer is not a valid (stable) prefix, and hence no subtyping rule can apply to make progress.

[swaldman]

Hi! Thank you for your reply!

You know the intricacies of Scala's type system lots better than I do, but as a user, this makes very little sense. A Scala object is stable. Once defined, Foo.Data will refer as certainly and clearly to a class and a type as if I had defined case class FooData(...). I would understand the compiler being much more restrictive with respect to a dependent type traversing a var, for example.

Projection types were made more cautious in Scala 3, requiring resolvability to concrete type, which is great, because it was possible to show circumventions of soundness when resolution to abstract types was allowed. But do there exist any circumstances where Outer#FooData with case class FooData(...) would be sound but Outer#(Foo.Data) would not, if Foo is an object declared in Outer? If there are, I'll agree that it should not be supported...

...and revise how I structure programs! Very often, I tacitly assume in Scala a close equivalence between, say

object A:
  object B:
    case class Foo(x : Int)
    case class Bar(y : String)

and

object A:
  case class B_Foo(x:Int)
  case class B_Bar(y:String)

That is, I use object nesting to reify namespaces and keep code ordered and organized. This projection-type issue is the first time I've encountered a discrimination that renders informal prefixing safer and more powerful than the nesting, which I usually consider preferable. Here A would be a class rather than an object type, but the choice of prefixing vs nesting at the B level is the same. If the compiler's current behavior is correct, than the right choice will be prefix, not nest, because despite the organizational advantages of nesting, the resultant types are crippled.

Again, I have to apologize (and express gratitude for all of your work!) that I don't understand the intricacies of the type system that you refer to. But I don't understand: If asSeenFrom(Outer, Outer.this.Foo.Data, Outer) is invalid because Outer is somehow unstable, why would asSeenFrom(Outer, Outer.this.FooData, Outer), referring to the very same Outer, be valid?

Thank you again for your detailed response!

[sjrd]

You know the intricacies of Scala's type system lots better than I do, but as a user, this makes very little sense. A Scala object is stable. Once defined, Foo.Data will refer as certainly and clearly to a class and a type as if I had defined case class FooData(...). I would understand the compiler being much more restrictive with respect to a dependent type traversing a var, for example.

An object per se is not stable. Only types are stable, and they are stable only when all their components are stable. So Outer.this.Foo is stable, because Outer.this and Foo are stable, but Outer#Foo is not, because Outer itself is a class with many instances.

Projection types were made more cautious in Scala 3, requiring resolvability to concrete type, which is great, because it was possible to show circumventions of soundness when resolution to abstract types was allowed. But do there exist any circumstances where Outer#FooData with case class FooData(...) would be sound but Outer#(Foo.Data) would not, if Foo is an object declared in Outer? If there are, I'll agree that it should not be supported...

The issue with that line of reasoning is: that we have not found a problem yet does not mean that there cannot be any problem. We have to prove, or at least convince ourselves, that no possible usages of the pattern can lead to a problem.

In this case, we don't really know what Outer#FooData even means, except in terms of existential types; and we don't have existential types anymore. So it is difficult to convince ourselves that it would be valid in all situations.

...and revise how I structure programs! Very often, I tacitly assume in Scala a close equivalence between, say

object A:
  object B:
    case class Foo(x : Int)
    case class Bar(y : String)

With nested objects, this always find, because any chain of objects is always stable. It's potentially an issue when there are outer classes or traits.

Again, I have to apologize (and express gratitude for all of your work!) that I don't understand the intricacies of the type system that you refer to. But I don't understand: If asSeenFrom(Outer, Outer.this.Foo.Data, Outer) is invalid because Outer is somehow unstable, why would asSeenFrom(Outer, Outer.this.FooData, Outer), referring to the very same Outer, be valid?

The latter is not valid either. It's just that we tolerate keeping Outer#FooData as is, without doing any asSeenFrom, but what we can show in terms of subtyping with that type is limited.

[swaldman]

With nested objects, this always find, because any chain of objects is always stable. It's potentially an issue when there are outer classes or traits.

Yes! But all I want is for concrete type B.Foo where B is an object to be treated as equivalently stable to B_Foo, wherever it appears. That's the only equivalency I want, but it would imply that outer.B.Foo be treated equivalently to outer.B_Foo where outer is an instance of class Outer and B is an object declared there. That's it! That's an equivalence I thought Scala already supported, but I was mistaken.

that we have not found a problem yet does not mean that there cannot be any problem. We have to prove, or at least convince ourselves, that no possible usages of the pattern can lead to a problem.

I have tremendous admiration for what you do, and I wish I were capable of helping on this score. My intuition is that treating concrete type B.Foo where B is a object the same as a substantively identical concrete type B_Foo can't break anything.

Of course I understand that you cannot rely upon my intuition. Intuitions of people much more sophisticated about type soundness than I am have proven mistaken before.

I guess I'd ask, though, that until you have pretty good reason to believe the intuition is wrong that you not affirmatively declare the compiler's current behavior to be correct. Addressing this may be hard within the compiler, and given the relative obscurity of projection types generally, I understand modifying the compiler to distinguish between more and less stable projection type paths might not be a high priority.

But the intuition that concrete types B.Foo and B_Foo where B is an object can and ideally should be treated equivalently I don't think has been shown to be mistaken. If that intuition is right — which, I concede, also has not been proven! — I think Scala should at least aspire to support these paths.

(This did actually come up in a real project, where I now use a workaround suggested by @aly from the scala-users discord.)

Thank you again for your help and your work!

[sjrd]

Overall, I agree with you that objects should be usable as namespace in all situations. That does not necessarily mean we can make it so.

The main culprit here is not objects; it's type projections. Type projections would not even exist in Scala 3 if there were not necessary to refer to Java nested non-static classes. Their additional capabilities should be considered a privilege.

I recommend you think not about using flat names instead of objects to solve your issues, but rather to use fewer type projections (if any). Use actual path-dependent types instead wherever possible.

[swaldman]

This is getting a bit off-topic, but I find that when I do use true instance-dependent types (as opposed to types just "dependent" on a nested hierarchy of singleton objects), I usually do find myself needing to resort to projection types for some abstractions. I try to stick with traditional independent types unless there's a good reason, because in my experience somehow more complexity than I expect results from instance-dependent types. But sometimes there is good reason.

In this case, I have an API made of lots of little elements (Task, Task.Run, Step and Step.Run, then two subtypes of Step) that interact only in formations that are logically parameterized by the same "payload" type. An earlier version had Task[Payload] etc, but carrying around an identical type parameters for many instances of six element types got cumbersome. Instead just defining a TaskRunner[Payload] and using tr.Step etc to define interoperable elements seemed elegant. But I want users to be able to write general reporters describing task executions, which are pretty much independent of the payload types (eg report by mail, report to text logs, report to db, etc.)

To avoid projection types, I initially defined abstract versions of each of the elements without their typed payloads, and wrote reporters in terms of that. But as the API evolved, it was annoying to evolve the inheritance hierarchy with it, and I'd sometimes be surprised by variance issues.

I suspect I could have powered through all that. But it seemed (and still seems) a bit dumb, when projection types are abstractions that represent precisely what I want without any extra code to maintain. The projection type captures everything that is common across different deployments of elements that doesn't depend on their shared type parameter.

All this is to say that I know projection types are kind of an afterthought and downplayed. But to the degree that instance-dependent types are an abstraction worth their complexity, I think that projection types are as well. This ability to specify everything-that-is-common about large families of related objects without requiring explicit specification of that commonality with inheritance is a very cool trick!

It is a bit unfair of me to say this, because it is not my work to take on but yours, but I think that continuing to explore and perfect projection types is worth the trouble, even though we've seen that they are not always trivial to reason about.

Again, easy for me to say. Please don't think I don't appreciate your work. Scala is just an extraordinary achievement, and building and perfecting an ever safer, ever more expressive type system is really a kind of heroism. Thank you again!