Make type projections safe instead of dropping them

[LPTK]

Background

It seems that type projections, which are of the form T # X, could be made sound if we simply disregarded the lower bound of X in T unless T is a singleton type.

For example:

class T { type X >: A <: B }
infer[T # X <:< B] // should work
infer[A <:< T # X] // should NOT work

See also the discussions on the contributors forum.

(Note: we could just as well disregard the upper bound instead, but I suppose that would be much less useful.)

Pratical Motivation

Type projections are used quite a lot in Scala 2. It would be best if we could just port most of that code as is, since migrating to not using type projections requires extensive refactoring, cannot be automated, and may introduce runtime performance concerns (see the same forum discussion).

The thing is, it seems it would be possible to port most of that existing Scala 2 code to a system with the restriction I proposed above.

I have seen lots of code where (non-trivial) upper bounds of type projections were used. I don't remember seeing lots of code where lower bounds were used. And I'm pretty sure I've never seen code where both bounds of a type projections were used, except in constructions meant to show the unsoundness of type projections.

Philosophical Motivation

Match types are a great addition to the language, in that they give us a concise and lightweight way of expressing closed type families. With scala/scala3#5996 they should even become robust in the face of abstract types.

Dually, type projections have been great because they basically give us concise and lightweight syntax for expressing open type families. If we add closed type families to Scala, it makes sense to me that we should strive to continue supporting open ones!

Semantics

What does a type projection T # X mean? I would say it means some type with a known upper bound, on which we know nothing more... that is, until T is substituted with a type in which X is concrete (at which point we can just pick that type out), or substituted with a singleton type (at which point we have a classical path-dependent type). It's easy to see that in both situations, such substitution will satisfy the upper bound that we have assumed for T # X.

Is that kind of weird? Well, IMHO it's no weirder than the nature of a non-reduced match type: a type on which we just know an upper bound (the union of the cases), but that is only made to precisely mean something when the scrutinee becomes concrete enough that the match stops being ambiguous.

---

Have I missed something? Would that actually be unsound?

[odersky]

We'd need a worked out way to map this down to DOT. Otherwise there's no way to answer the question:

Have I missed something? Would that actually be unsound?

I believe it would be great if someone undertook this effort. Foundations have to come first, and they are not optional.

[LPTK]

I agree on the principle. But AFAIK several current features of Dotty do not yet have DOT mappings either, such as higher-kinded types and match types.

Both higher-kinded types and (restricted) type projections are important for backward compatibility with Scala 2. I think that should justify their inclusion even though they have not been formally proven correct yet. At least we have a good intuition that they are "morally" sound (but of course, that intuition may turn out to be wrong).

[Blaisorblade]

@LPTK Somebody must make a judgment call for unproven addition, based on what we know anyway. Unlike for higher kinds, we know type projections have caused big trouble before.

I'm thinking again of how to add type projections to my proofs: one needs to define when values are in T#X, and check the type rules that follow. But using the semantics I and Miles suggested in scala/scala3#4583 doesn't seem to give the behavior you're asking for; one would require some twists.

==

Separately, re-reading scala/scala3#4583, it seems what you propose might be close to the original semantics for type projection in the 2003 paper:

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 >: L <: U) or T#A = Z (in case A's decl is type A = Z), but never T#A >: L.
However, I'm not sure if that paper gives good answers on intersections of conflicting bounds (and I doubt it).

[LPTK]

@Blaisorblade by "using the semantics I and Miles suggested", are you referring to this?

By t.A forAll { val t: T } I intended the intersection of the As for all t: T, not the union

How could that be the intended semantics? It would mean that given any a:A, you can upcast A#T to a.T, and that you could not upcast a.T to A#T.
This clearly goes against the intended semantics of type projections in the particular case of nested classes, which for the record I think should be the following:

class A { self => class B { /* defs */ } }

is to be understood as:

class A$B(self: A) { /* defs */ }
class A { type B <: A$B }

where A#B denotes that common ancestor class A$B of all instances of the inner classB irrelevant of which A they were instantiated from. In that sense, a type projection A#T would be the union of the types a.T living in all possible instances a of the prefix A.

[Blaisorblade]

@Blaisorblade by "using the semantics I and Miles suggested", are you referring to this?

By t.A forAll { val t: T } I intended the intersection of the As for all t: T, not the union

How could that be the intended semantics? It would mean that given any a:A, you can upcast A#T to a.T, and that you could not upcast a.T to A#T.

As I mentioned to @LPTK elsewhere. For the record, while Miles and I might not yet agree and he might be right, I favor using the union.

Assigning this to myself, as I'll keep this among my TODOs in my theoretical work.

[Blaisorblade]

(Towards?) Soundness for type projections in Coq

Good news! I've just formalized type projections in Coq (first version: Blaisorblade/dot-iris#250). And this seems to support most interesting typing rules, including lower bounds for projections out of realizable types.

I've used a "set-theoretic" semantics suggested by @LPTK, on top of my work on guarded DOT (conditionally accepted to ICFP'20). Caveats apply (see below).

The idea is to model T#A as t.A forSome {val t: T} (but without desugaring the existential as in the Scala 2 spec).

Formally, V[[T#A]] = { v | ∃ w ∈ V[[T]]. v ∈ V[[w.A]] } — that is, a value v is in T#A if there exists a value w in T such that v is in w.A.
I think that's clearly the intended semantics for forSome; in particular, this makes T#A the union of w.A for all w.A.

This semantics should validate at least the following typing rules — variants of those rules appear in the above PR:

p.type#A = p.A

Γ ⊨ T <: { A :: L .. U }
------------------------ (Proj-<:-U)
Γ ⊨ T#A <: U

Γ ⊨ T <: U
------------------------ (Proj-<:-Proj)
Γ ⊨ T#A <: U#A

From those, we can derive the following rules for lower bounds:

Γ ⊨ p : T
------------------------ (Sel-<:-Proj)
Γ ⊨ p.A <: T#A

This follows because p.A = p.type#A, and p.type <: T.

Γ ⊨ T <: { A :: L .. U }
Γ ⊨ p : T
------------------------ (Proj-<:-L)
Γ ⊨ L <: T#A

This follows from L <: p.A <: T#A.

In practice, if you have an expression e of type L and want to use it at type T#A, you certainly need a path p: T to be around, and you'd likely have to explicitly write e: p.A for some p: T.

Dotty realizability checking might help showing such a p exists and relaxing this requirement; in that case, make sure to compute the correct lower bounds for p.A.

This way, the restriction on (Proj-<:-L) deals elegantly with realizability issues: if type T is empty, you don't have such (closed) paths p: T, so you can't create expressions of type T#A.
(In an contradictory context things are trickier, but the DOT invariant is that code in such a context cannot be run).

In particular, this ends up disregarding the lower bound of T#A as @LPTK proposed.

Why are projections covariant? Why does (Proj-<:-Proj) hold?

Till now, I didn't believe this rule. Here's an informal proof using this intuitive set-theoretic semantics.

If a value v is in T#A, then v is in w.A for some w : T, but since T <: U then w : U.
In other words, v is in w.A for some w : U; that is, v is in U#A.

In sum, any v in T#A is in U#A — so T#A <: U#A.

My Coq proof formalizes the same intuition, but using a pretty different notion of "set" :-).

Possible TODOs

1. @milessabin shows various issues with projections in Conformance of type projections in SLS 3.5.2 violates expectations, conflicts with intersection types and isn't supported scala/bug#10916, and I haven't reviewed them. Those are the known bugs of with fixed by & — Scala 2 with lets you override type members (the horror!)
2. Do type projections need additional typing rules? (Hence the "Towards?" in the title).
3. EDIT: how does this scale to full Scala?

Theoretical questions

• How does this compare with past semantics?

Caveats

• Guarded DOT treats type members a bit differently from DOT; in practice I can translate any pDOT program to a gDOT program (as shown in the paper), but I haven't either automated that or proved that it can always be done.
  These differences should not matter unless you want to add unrestricted negation types.

/cc @LPTK @sstucki @namin @TiarkRompf @odersky @smarter @robbertkrebbers.

BTW, see https://dot-iris.github.io/coqdoc/D.Dot.semtyp_lemmas.tproj_lr.html for the hyperlinked source, for easier navigation.

EDIT: Gitter reactions at https://gitter.im/lampepfl/dotty?at=5ecd2bcfb101510b201a600c.

[Blaisorblade]

Unassigned myself for the next steps — @smarter or @odersky want to assign somebody to figure out what should happen?

[smarter]

I don't think we have the resources to look at this until after 3.0

[Blaisorblade]

Fair — it might be worth mentioning this somehow to people who'd need lots of effort to migrate from them, maybe in http://dotty.epfl.ch/docs/reference/dropped-features/type-projection.html.

But I'll ask on scala/contributors gitter.

[djx314]

It seems that my framework's last version is whole dependent on type projection. Now remove type projection and the functional is becoming so limited.

[Blaisorblade]

@djx314 Then maybe wait to migrate to Dotty...

[djx314]

One of my main code is

trait TypeParam {
  type H
  type T <: TypeParam
}

trait TypeContext {
  type K[T <: TypeParam]
}

class EncoderTypeContext extends TypeContext {
  override type K[T <: TypeParam] = Encoder[(T#H, T#T#H)]
}

I use type projection to implement a HList type parameter context. Now I can just codegen TypeContext to TypeContext1 - TypeContext8, this makes my code increase to 10,000 lines and the support is limit.

Use type project can also implement some code like a HList or a Nat plus Nat with no implict and no object(just type Nat3 = Nat1#Plus[Nat2]), it's worth to implenemting it in dotty.

[LPTK]

@smarter could you elaborate on what kind of resources you'd need to look at this?

From my point of view, most of the work is done. We just have to remove the current type projection limitation and instead prevent the use of their lower bounds. I could try to look into implementing it, if you think it makes sense.

Waiting until after 3.0 sounds weird. It's like creating an artificial bump on the road (remove a feature, then add it again, even though the vast majority of uses of this feature are known to be sound).

[Blaisorblade]

@djx314 I can't comment on the details, Dotty will support HList and shapeless pretty well, thanks to work by Miles.

[smarter]

@Blaisorblade listed a bunch of TODOs in #14 (comment), these look like major undertakings to me.

[LPTK]

@smarter these TODOs (note: they have been edited) look like smaller details to me and can certainly be worked out later or as we go. I don't think you can reasonably hold the position that they're real blockers for a feature, while on the other hand full support is added to the compiler for such wild things as AnyKind (about which very little is known on the theoretical side).

[smarter]

I mean, I think that at a minimum it'd be good to figure out if what TypeComparer does actually matches the rules in Blaisorblade/dot-iris#250, but that's just my opinion. (I'm also not a big fan of AnyKind, but apparently it's needed for some stuff, oh well)

[djx314]

It's a generic lib like shapeless in first step with unlimited type parameter and limited item count intermediate data structure(Tuple) https://github.com/djx314/ugeneric-compare Shows that it has 3 times faster than circe semiauto in scala 2.13, the speed will more and more faster than semiauto when the property count becoming so large. I don's konw what will happen in dotty because macros module now not yet compat to dotty. But shapeless3 is really fast in dotty. But without type projection, the lines of code is 10 times larger than last version. That's why I pay attention to this issue.

…

------------------&nbsp;原始邮件&nbsp;------------------ 发件人:&nbsp;"Paolo G. Giarrusso"<[email protected]&gt;; 发送时间:&nbsp;2020年5月28日(星期四) 晚上10:24 收件人:&nbsp;"lampepfl/dotty-feature-requests"<[email protected]&gt;; 抄送:&nbsp;"水山清风"<[email protected]&gt;;"Mention"<[email protected]&gt;; 主题:&nbsp;Re: [lampepfl/dotty-feature-requests] Make type projections safe instead of dropping them (#14) @djx314 I can't comment on the details, Dotty will support HList and shapeless pretty well, thanks to work by Miles. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

[Blaisorblade]

@smarter The "other issues" by @milessabin were not about projections. I agree with @LPTK the other concerns don't seem showstoppers.

While I'm in favor of being careful, I'd recommend:

• changing guidance for migration to "their status is uncertain, heavy users should maybe wait"
• maybe support them (best-effort) under -language:Scala2.
• give everybody time to evaluate things more closely and spend the needed effort into supporting them.

[djx314]

@Blaisorblade Should it support by a single compile parameter? It seem's that scala2 cannot use given and so on. It's not friendly coding with scala3.

[smarter]

maybe support them (best-effort) under -language:Scala2.

We'd still need to figure out what exactly we can support , @LPTK's original proposal is "disregard the lower bound of X in T unless T is a singleton type.", so there's some work to be done in TypeComparer any way to see what needs to be tweaked.

[Blaisorblade]

TypeComparer doesn’t care, there’s an error message in PostTyper, that could be made a warning in compatibility mode; that’s clearly a hack, but I think this already happens (see -strict vs not).

Slightly harder: only use lower bounds when Typer itself can be certain they are safe. That might reject some currently allowed and safe programs.

And you’re right, doing this properly is hard: actually annoying to implement: IIRC, right now Typer ignores the problem (because it basically does type inference) and PostTyper later rejects type projections out of non-realizable types - because realizability can only be checked after Typer (it needs global information; maybe that can be done in Typer, but I’d worry of CyclicReferenceErrors).

BTW, I was never confident that worked (what about type projections that the user didn’t write? How do we know they don’t arise?), but have never seen an actual bug with it. But now, you’d have to record if you used the lower bound rule and if that actually mattered — as opposed to, instead, you backtracked. And what if you used lower bounds, they were unsafe, but the overall subtyping held for another reason (because there were unions involved and you could have backtracked to a “safe” subtyping)? Argh.

[smarter]

you’d have to record if you used the lower bound rule and if that actually mattered

Can't we add as a precondition to that rule in TypeComparer that the lower and upper bound are equal?

[Blaisorblade]

FWIW, I do conjecture { A >: T <: T } # A equals T, even tho I hadn't done it (formalizing that in Coq, even with the necessary extra later connectives, seems in fact tricky; nowhere else do I need to construct new type definitions during typechecking; this would work in other realizations of my proof technique). This unproven rule underlies the existing Dotty support for projections.

However, that doesn't carry over to all subtypes of { A >: T <: T } — if U <: { A >: T <: T } then you only have U#A <: { A >: T <: T }#T = T — in this semantics, if U is uninhabited, U#A is uninhabited as well (so it satisfies the upper bound but not the lower one).

[sstucki]

FWIW, I do conjecture { A >: T <: T } # A equals T

Isn't this derivable? Isn't p = new(_){ A = T } always a valid inhabitant of { A >: T <: T }, from which we'd have that T is both an upper and lower bound of { A >: T <: T } # A, or am I missing something?

[LPTK]

I guess in this particular case it holds, but it gets complicated when A is not the only member and T refers to some non-trivial self type, which makes inhabitation unclear.

[LPTK]

@Blaisorblade re: tests/neg-strict/i1050.scala, it seems the error count is different because most errors are post-typer, but my change makes the one type projection error a typer error, thus halting compilation too early to catch the other errors.

[sstucki]

I see. If U has a member A, that is U <: { A >: T <: T }, then @Blaisorblade's caveat applies and you only get U#A <: { A >: T <: T }#T = T whereas you'd like an equality.

[Blaisorblade]

@LPTK that still worries me — lots of things in tests/neg-strict/i1050.scala are unsound and (I fear) checked by the code you commented out — starting from:

  lazy val x: A & B = ???
  val y: x.L = 1    // error: underlying conflicting bounds

But I'm not sure we should discuss that quick change here.

[Blaisorblade]

I guess in this particular case it holds, but it gets complicated when A is not the only member and T refers to some non-trivial self type, which makes inhabitation unclear.

Yes — I mean, formally any member with bad bounds is a problem, and the case where T#A uses other members of T is the more clearly dangerous one.

[LPTK]

@Blaisorblade if you comment the 2 lines which use type projection in i1050, all the errors get reported properly again, and the test passes. So it looks like my understanding was correct.

Also, interestingly, the reason neg/i1050c fails is only that it has more errors than expected in places that were already assumed to be errors, thanks to the new isSingleton check (the error locations use type projection).

You may be right that here is not the best place to discuss these things, though.

[Blaisorblade]

FWIW, I do conjecture { A >: T <: T } # A equals T, even tho I hadn't done it (formalizing that in Coq, even with the necessary extra later connectives, seems in fact tricky; nowhere else do I need to construct new type definitions during typechecking; this would work in other realizations of my proof technique). This unproven rule underlies the existing Dotty support for projections.

FWIW, I mechanized (a version of) that rule in Blaisorblade/dot-iris#304, after some changes to the model (in Blaisorblade/dot-iris#303).

"Extra later connectives" are necessary — so what you get is essentially { A >: T <: T } # A = Later T, but that's similar to other restrictions for type members in gDOT.

[Sciss]

I would just like to add my use case. My basic construction is this

trait Ref[-Tx, A] {
  def apply()(implicit tx: Tx): A
  def update(v: A)(implicit tx: Tx): Unit
}
trait Txn[S <: Sys[S]] {
  def newRef[A](init: A): Ref[S#Tx, A]
...
}
trait Sys[S <: Sys[S]] {
  type Tx <: Txn[S]
...
}

such that

trait Foo[S <: Sys[S]] {
  def bar()(implicit tx: S#Tx): Int

  def baz()(implicit tx: S#Tx): Unit = {
    val test = tx.newRef(bar())
  }
}

There are more type members involved, this is just a simplification (the API is easier to make compile than to create an actual implementation!).
I have started a preliminary project to see if I can make it work "at all" in Dotty. So far without luck. Each system S <: Sys[S]] has different behaviour, for example in-memory STM, database-backed, real-time enabled, etc. So in order to make it work, we have to have a set of types - transactions, variables, identifiers, ... - that fit together for each sub-system. If anyone can help me looking at 'DottyLucre' to understand if there is a way to make it work in Scala 3, that would be great. Otherwise, the loss of type projection is a major frustration for me, as I built a large system in the past ten years utilising these well-defined type projections.

[godenji]

Where do things stand now, are type projections permanently dropped, or will they perhaps be reintroduced post-3.0?

Really unfortunate for those of us that are trying to port Scala 2 projects to Scala 3 where workarounds for "missing" type projections are deeply disatisfying.

Such a useful feature, out with the bath water goes the baby...

[bblfish]

Perhaps it would be an idea to get a list of projects that are going to go through a lot of work without type projections. It would be interesting there to see which of them are better off reworking their code, and which are going to be uglier (assuming a fix like the one proposed here). This would allow us to gather some experience of how to make the move, or indeed to show the value of the feature proposed here.

I just got banana-rdf as close as possible to Scala3. But I now have 510 errors left due to type projections. It would be good to know if those type projections are ok with this proposal, or if they are in fact the dangerous ones the removal was attempting to protect us from.

[LPTK]

@bblfish are any of the types you project out explicitly lower-bounded? And if so, is the lower bound ever used? (Meaning something is taken as a subtype of the type projection, e.g. a value is upcasted into it.) If not, then you should be good, assuming the powers that be decide to reintroduce type projection in a later release of Scala 3.

[bblfish]

I think we should be ok. The trait type projection is used with is RDF and its various subtypes Jena, RDF4J and Plantain all are immediately used by a single object (each named at the bottom of those files respectively) so I think that counts as lower bounded. The advantage is that it allows one to write code that is completely independent of the RDF implementations as shown by all of our tests such as this one. It allows one to write libraries in Java and JS (we have not tried native yet), by abstracting the implementations.

I don't know how @betehess knew this was the right thing to do when he implemented it 10 years ago.

[LPTK]

@bblfish your usage should be completely fine. On the other hand, it seems it would be rather easy to port to using a value rdf of type RDF everywhere you currently use a type Rdf <: RDF, which would allow you to avoid type projections.

[bblfish]

You mean using dependent types? I started looking at that in August.

trait PointedGraph[T <: RDFObj](using val rdf: T) {
  def pointer: rdf.Node
  def graph: rdf.Graph
}

But with 500 errors to fix I wanted to make sure I was going in the right direction. So I thought I needed a lot more experience with Scala3, and I still think I could do with more.

It somehow seemed to lead to creating a bunch of empty brackets and made me wonder if a notation like class PG[val t: RDF](node: t.Node, gr: t.Graph) could be helpful. Otherwise it seems like bracketing issues may be re-appearing. If I remember the ordering of dependent types is tricky as arguments often depend on the dependent object...
I'll try working on this regularly in small intervals to see if I get any further...

[johnynek]

The challenge is, if you are using type projections without lower bounds, despite it being safe, you either have to remove them before adopting scala 3 or wait an extra cycle.

I guess most people will remove them and do the port already, so adding them back later will wind up only costing more effort or encouraging people not to port the given library.

https://github.com/twitter/summingbird/blob/develop/summingbird-core/src/main/scala/com/twitter/summingbird/Platform.scala

Summingbird uses abstract types, (P#Store[K, V]) in a way that I think isn't supported. So instead, we would have to change all the call sites to pass a concrete Platform and use the path dependent type. But, I think this is an example of something that isn't unsound, so if we port, we have to port twice, once for 3.0 then back again for 3.1.

[LPTK]

@johnynek note that no one forces you to port it back to using type projection in 3.1. That would be a weird thing to do.

My guess is that most people will just abandon type projections altogether or just wait before porting their libraries to Scala 3. This is really a suboptimal situation, as the former option creates needless work and breaking changes (and can also lead to less user-friendly library interfaces), and the latter option means the community is stuck on an old version of Scala for an unknown amount of time.

And all this pain is inflicted on users for pretty much no reason. There are many existing actual soundness holes in Scala, and it's not the end of the world. I have never heard of anyone being affected by the particular one that comes from Scala 2-style type projection. So even keeping unsound type projections would be a better way forward, before the restriction that makes them sound can be put in.

[godenji]

And all this pain is inflicted on users for pretty much no reason.

Clearly in Scala 3 there's been a lot of work put into proving that the language is theoretically sound; removing type projections puts theory into practice, but at the expense of rendering existing real world applications that depend on this feature, useless.

I personally have relied heavily on type projections over the years, and as a result will simply abandon all affected Scala 2 code -- a fresh start of sorts, far from ideal, but the alternative of reworking type projections into path dependent type + givens simply doesn't pay its weight.

[johnynek]

@LPTK I guess I don't understand why the suggestion of: #14 (comment) was not done. It seems like a one line diff and probably restores 90% of the use cases without adding soundness holes. Do I misunderstand?