Proposal to remove general type projection from the language

Scala Improvement Process
1

Hi Scala Community!

I’d like to open the discussion for the pending SIP on dropping general type projection from the language. You can find a brief write up here.

Summary

Scala 2 currently allows general type projection of the form T#A where T is an arbitrary type and A names a type member of T.

Dotty prohibits this if T is an abstract type (class types, singleton types and type aliases are still permitted). This change was made because unrestricted type projection is unsound.

Implications

The use of type projection from abstract types has been used to implement type functions in Scala 2 (see eg. this encoding of the SKI combinator calculus). This will no longer be possible.

In mitigation, this way of encoding type functions was always limited and extremely fragile due to compiler bugs and confusion around the semantics, and it has largely been displaced by implicit-driven type level computation. In Dotty we also have match types which allow type functions to be expressed directly.

Opening this up for general community discussion and insight into any other use cases that should be considered.

7 Likes
2

Off the top of my head this seems like a good change. I can’t think of anything I use type projection for that type lambdas or match types won’t do better.

1 Like
3

Dotty type lambdas replace Scala 2 type lambdas, which also use type projection, but in fact the type projections typically used in that case are still permitted under this proposal.

2 Likes
4

FWIW, my STM overlaying object system Lucre relies heavily on type projections, such as

trait Sys[S <: Sys[S]] {
  type Id
  type Tx
}

and then a proliferation of S#Tx in the entire code base. I don’t see a straight forward way to move this project (thus my entire project stack) to Dotty if S#Tx for S <: Sys[S] wasn’t supported. I experimented for a long time till I came up with this construction, everything else, including path depenendent types failed miserably.

1 Like
5

The proposal is only to prohibit type projections when the type on the LHS is an abstract type. Could you give some examples of type projections from your codebase which also meet that condition?

6

Here is a simplified case, working in Scala 2: https://scastie.scala-lang.org/Fr5USmSUTJO7IzisPt1q4Q

None of that compiles in Dotty: https://scastie.scala-lang.org/2nOXdSHcQtGxXpqQnVo61Q

7

P.S.: If you can make this work, and without having to store an actual val s: S in every use case instance, you will be a genius:

8

In that example, the following strikes me as a bit odd,

trait Txn[S <: Sys[S]] {
  def system: S
  
  def newId(): S#Id
  
  def newVar[A](id: S#Id, init: A): S#Vr[A]
}

I’m surprised that system is unstable (ie. a def rather than a val). The following seems a lot more natural to me,

trait Txn[S <: Sys[S]] {
  val system: S
  
  def newId(): s.Id
  
  def newVar[A](id: s.Id, init: A): s.Vr[A]
}

Why did you go with the former rather than the latter?

9

Look at my second reply - it’s simply not possible to use path dependent types. I have really tried to make them work for a long period back when I designed the system. The crucial thing is to make the entire construction work, including the classes parametrised with S. Putting only path dep types in Txn is easy in isolation.

(And yes, it’s val system: S in all practical applications)

10

I got this far: https://scastie.scala-lang.org/Jasper-M/xCnTcvKHQSadcbylphV8Ng

Can’t live without your erased system though… Of course I don’t know if this will even work in your unsimplified project.

11

Is it possible to give some examples of cases where T#A is acceptable and unacceptable as far as this SIP is concerned?

12 
class Outer {
  class Inner
}

var a  = mutable.ListBuffer.empty[Outer#Inner]

Will it work in your proposal?

13

Yes (emphasis mine):

14

As far as I understand, the only thing that will not work is A#B where A is either:

  • defined in a type parameter list [A <: X], or
  • defined as an abstract type alias type A <: X.
15

@Jasper-M thanks, your example already looks good.

Now the next problem is that you immediately get diverging paths, because type system doesn’t unify s across values: https://scastie.scala-lang.org/aIw4sn6zTUKsUDfeOCH0tw

I’m rather pessimistic that this can work smoothly.

16

Ok - with a trick: https://scastie.scala-lang.org/hAENQ0sLQciq9fEwCPFjvQ

A bit of a try to “cross compile” with Scala 2: https://scastie.scala-lang.org/tBT48WpAQkiqV3DD2cgNDw

Which begs the question - will erased values be ported back to Scala 2?

17

If you could rewrite to def gimme()(implicit tx: s.Tx): UseCase[s.type] it works again.
However what most of these examples of heavy type projection use cases eventually show IMO, is that once you start rewriting to hardcore path dependent types all-over you will eventually come into conflict with the type inference strategy of widening singleton types by default.

19

This is going to be problem: https://scastie.scala-lang.org/0HkKTrGaQleHmnbJSPL4cw

trait Sys

trait Obj {
  erased val s: Sys
  
  type S = s.type  // error!
}

Is there a reason this doesn’t work in Dotty? If this worked, I could see an elegant way to porting my type projection based system to use path dependent types instead. For example: https://scastie.scala-lang.org/S3yD86zjSU6CX7y1i5A76g - it thus requires that the above is allowed, and that a non-erased val can override/implemented an erased val.

20

Is there a reason this doesn’t work in Dotty?

Unfortunately, yes. In fact, it’s the same reason why type projection is outlawed now. Both are unsound. To explain the issue very roughly: To maintain soundness we need to make sure that every prefix of a type selection has been constructed somewhere. That’s not true for type projections (since the prefix is a type) and it is also not true for erased types (since the prefix will never be constructed explicitly).

However, there might be a way to still allow this if we demand realizability instead. Question: Would your construction also work if s was not erased? I.e. is erased just an optimitzation to save space?

21

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

trait Sys { type X }

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