Proposal to remove general type projection from the language


#42

Understood. It sounds like you’re angling at the cake/virtual classes encoding way of doing things … did you try things along the followng lines?

trait BaseSys extends Sys {
  type Tx <: BaseTxn
  trait BaseTxn { ... }
}

trait Sys1 extends BaseSys {
  type Tx <: Txn1
  trait Txn1 extends BaseTxn { ... }
}

trait Sys2 extends BaseSys {
  type Tx <: Txn2
  trait Txn2 extends BaseTxn { ... }
}

#43

(That could kind of work, although in actuality the transactions will mixin different base traits.)


#44

Here’s an attempt at a summary of the scenarios that @Sciss and @Alexander raised …

I would describe them as attempts to encode family polymorphism/virtual classes without requiring an unerased term to represent the family.

My take is that in Scala 2 the requirement for a term isn’t really all that burdensome, although admittedly it will take a bit of restructuring to get to something which has reasonably pleasant ergonomics (see my suggestions above).

Speaking for myself, I’d go for a different type of design altogether and represent those kinds of family relationships with type classes, but I appreciate that the path from here to there could be quite hard going.


#45

And STM and FP are really very different approaches to modelling things. I can’t see me rewriting this system using type classes and massive passing around of evidences.


#46

Another final remark. After seeing that it’s basically possible to write with path dep types, they do offer something that the projections didn’t do, namely ensure that it’s not possible to accidentally use a transaction from one system in another system of the same type. Right now it’s technically possible to use a transaction bound to database A to issue modification in an object that is actually persisted in database B, if S1 =:= S2. Although it is very unlikely to run into this situation, the path dep types exclude that possibility in the first place, because there will be precisely one value of s1: S1 and one value of s2: S2 and by definition s1.type != s2.type. This may not apply to all scenarios where type projections are used, but here it does work out.

So I will just curiously watch the evaluation of the erased term discussion.


#47

Summingbird also uses this pattern:

We do that in order to write code like:

def job[P <: Platform[P]](source: Producer[P, String], store: P#Store[String, Int]) =
  sources.map { word => (word, 1L) }.sumByKey(store)

I know that general type projection is unsound, but I’m not sure how these examples are (e.g. we know that P <: Platform[P] or the STM example which did something similar).

We could rewrite this code, I guess, as something like:

def job[P <: Platform](p: P)(source: Producer[P, String], store: p.Store[String, Int]) ...

but this will require changing a lot of call-site code.


#48

Unfortunately this will change semantics, whole purpose of DomainRepository is return instance of Customer by provided type, in real case it would be some case class of Customer entity, so in that case I need to find a way how to tell that Customer object is a hint for Customer case class instance, but all ways that I now is also require type reference. I’ve updated scastie snippet with more details.


#49

I’m not seeing that …


#50

I made fork, hope this works


#51

How about this.


#52

Quick clarification: Type projection is still allowed under -language:Scala2. So that means it’s not an immediate blocker for migrating.

We need to outlaw unrestricted type projection in the spec since it is unsound. One thing we could potentially do is enable it under a special compiler flag such as -language:unsoundProjections. That would mean we could technically support it in the new compiler without having to spec it. This is basically the same as what @soronpo proposes, except for the spec part.

On the other hand, I would like to avoid language flags where possible. So I see this more as a last resort in case this remains a blocker for upgrading in the future.


#53

Then I don’t really understand why this is allowed:

trait Sys { type X }

trait Obj {
  erased val s: Sys
  
  type S = s.X
}

I can’t reproduce that. I get in both cases:

6 |  type S = s.X
  |           ^
  |           Sys(Obj.this.s) is not a legal path
  |           since it refers to nonfinal value s
one error found

#54

So the problem with the erased approach of @sciss is that the erased value is not a path since it is
non-final. Being non-final it could be implemented by a value that introduces bad bounds.

There might be a way out of this, but it requires more research: One could think of a path modifier or annotation that specifies that all overriding implementations must be legal path prefixes. That could be checked in a modular way.

Erased being overridden by non-erased: I don’t know. That would again require lots of careful research, and I can already see how it would complicate the implementation. Is that absolutely needed?.


#55

It works for me in scastie. And I think I tried it in a recent version of the dotty REPL, but not 100% sure to be honest.


#56

Hmm. Does scastie enable Scala-2 mode by chance?


#57

I wholeheartedly agree. I hate flags. But in this feature’s case the migration may be too difficult for not so few projects, which will cause them to stay behind on Scala releases if they have no escape path like a language flag. The lesser of two evils, a language flags or a community split, is a flag IMO.
I’m for removing it from the spec in either case.


#58

Regarding the name, I would recommend something more “scary”. A beginner user can copy-paste build files (especially SBT files which users avoid like the plague when they start) or imports without understanding the risk or lack of support involved.


#59

Scastie uses an old version of Dotty, upgrading Dotty is blocked on https://github.com/scalacenter/scastie/issues/281, untl then don’t use scastie to infer anything about Dotty’s current behavior.


#61

Probably not. I just thought it would be convenient here. But this is all very hypothetical and therefore too early to say whether it will be crucial or not (probably not). At some point, in one of the next Dotty releases, I should see how far I can get with a non-scala2-mode implementation of the Lucre base module using path dependent types.


#62

I think there’s a subtle but important distinction to be made here: are all such type projections unsound, or are they just not proven to be sound? There could well be cases where a certain use of type projections is in fact sound (i.e. never has the potential to introduce runtime errors) but isn’t covered by the cases that DOT has proven sound (or is equivalent to one of those cases but not trivially so).

There’s a difference between “unsound” and “not yet proven to be sound”.