Pre SIP: Improvements to Modularity #18958

odersky · 2023-11-17T13:20:07Z

For a tracked class parameter we add a refinement in the constructor type that
the class member is the same as the parameter. E.g.

class C { type T }
class D(tracked val x: C) { type T = x.T }

This will generate the constructor type:

(x1: C): D { val x: x1.type }

Without tracked the refinement would not be added. This can solve several problems with dependent class
types where previously we lost track of type dependencies.

In particular it addresses the parser combinator test cases that were prompted by this discussion in Scala Users: https://users.scala-lang.org/t/create-an-instance-of-a-type-class-with-methods-depending-on-type-members/9613/4.

This PR is essentially a feasibility study. It shows that we can get better tracking of types through constructors without breaking anything.

But I am not sure yet a new modifier tracked is the best way to achieve this. Ideally, we would detect when a class uses a class parameter as a path in a type, and refine those parameters only. The problem is that we don't know this in general when we compute the type of a constructor application, since types of class members are computed lazily on first access.

Example:

    trait A:
       type T
       def m: T

    class D(x: A):
       def f = x.m

We need to typecheck the RHS of f in D to figure out that f's result type x.T refers to the parameter x, so that x needs a refinement. So computing precise info of what needs to be refined is infeasible.

Some of the other options are:

The current scheme: use a modifier such as tracked to indicate refinement. To make this more robust we could make it an error if a type in a public signature refers to an untracked class parameter. So in the example above, we could enforce that class D is declared as class D(tracked x: A).
Overapproximate wildly: Make all class parameters tracked (probably this would cause lots of problems).
Overapproximate more conservatively: Maybe make all non-private class parameters tracked. This is appealing at first glance since private class parameters cannot appear in refinements anyway. On the other hand, it would still make all case class parameters tracked, which is probably overkill again. Variations: Make all parameters declared with explicit vals tracked, and/or make all parameters in given ... with clauses tracked.
Try to guess: Assume tracked for parameters that appear "obviously" in a path. E.g. there is a path with the name of the parameter in an explicitly given signature in the class. Provide a fallback such as a tracked modifier or an annotation for parameters that are not obviously in a path. The goal of this compared to (1) is to be less annoying. Why insist on explicit tracked if it is clear from the source that a parameter needs to be refined? But I don't like the fragility of this scheme.

odersky · 2023-11-17T13:27:17Z

These are variations of a Scala Users discussion

The critical part is shown in parsercombinators-expanded.scala. definition of combine:

def combine[A, B](
      _f: Combinator[A],
      _s: Combinator[B] { type Context = _f.Context}
    ): combine[A, B] {
      type Context = _f.Context
      type Element = (_f.Element, _s.Element)
    } = new combine[A, B](_f, _s).asInstanceOf
    // cast is needed since the type of new combine[A, B](_f, _s)
    // drops the required refinement.

We'd need to appy the scheme for instantiating dependent methods also to class instance creations.
If a new expression of a class that defines type members mentioning parameters, we need to add a refinement
that substitutes actual arguments for formal parameter names.

odersky · 2023-11-17T13:28:37Z

See also #3964, #3920

odersky · 2023-11-19T15:58:05Z

I now see that #3936 is very similar to this PR (and might also solve some problems wrt inheritance in this PR). Definitely worth following up. Maybe we should re-open #3936? /cc @liufengyun @julienrf

liufengyun · 2023-11-19T19:42:51Z

I now see that #3936 is very similar to this PR (and might also solve some problems wrt inheritance in this PR). Definitely worth following up. Maybe we should re-open #3936? /cc @liufengyun @julienrf

Indeed it's similar. Glad to see there's real requirement from real-world programming. This PR is much more polished than #3936, it makes sense to keep the current PR. Some of the tests in #3936 can be ported here.

BTW, I remember @mbovel is working on something related.

odersky · 2023-11-19T21:25:14Z

I was particularly interested in the way #3936 handles base types. This PR has nothing in that department. Maybe that's needed to fix the remaining failures in neg/i3964.scala?

liufengyun · 2023-11-19T22:10:52Z

I was particularly interested in the way #3936 handles base types. This PR has nothing in that department. Maybe that's needed to fix the remaining failures in neg/i3964.scala?

I forgot exactly why the changes in handling base types, but it seems to be motivated by the last test case there. However, I'm not sure if the changes make sense, as I was not very familiar with the base type computation at the time.

odersky · 2023-11-21T16:57:57Z

Some more info: Making all explicit vals tracked causes a failing bootstrap and ~50 failing tests. Particular issues:

Private vals escaping in inferred refinements of non-private values
Cyclic references between a class and its parents
Type errors because a too precise type was inferred

So, not sure this idea will fly.

liufengyun · 2023-11-22T07:21:01Z

I was wondering will the errors go away if track is opt-in.

Some more info: Making all explicit vals tracked causes a failing bootstrap and ~50 failing tests. Particular issues:

Private vals escaping in inferred refinements of non-private values

It seems this will go away if track is only allowed on non-private values.

Cyclic references between a class and its parents

Type errors because a too precise type was inferred

This might go way as well with explicit track --- at least users can understand and easily fix if too precise inference due to track becomes a problem.

So, not sure this idea will fly.

odersky · 2023-11-22T08:33:39Z

@liufengyun Yes, I agree, explicit tracked solves most of these things. But #19015 is still useful since it might us help discover problems that also arise on widespread uses of explicit tracked parameters, and that could be fixed now.

odersky · 2023-11-22T08:41:04Z

Another thing that currently does not work is this test from neg/i3964.scala:

object Test3:
  trait Vec(tracked val size: Int)
  class Vec8 extends Vec(8):
    val s: 8 = size    // error, but should work

The problem is we currently keep track of refinements in constructors and therefore in constructed values. But we don't do the same thing inside classes. Inside classes we could experiment with

Synthetic abstract members, like in Vec8 we'd need a synthetic abstract member val size: 8. The general case looks more tricky, though.
Refinements on the self type. I.e. Vec8 would be expanded to class Vec8 { this: Vec8 { val self: 8 }}. We do a similar thing for opaque type aliases.

liufengyun · 2023-11-24T06:30:46Z

But we don't do the same thing inside classes. Inside classes we could experiment with

Synthetic abstract members, like in Vec8 we'd need a synthetic abstract member val size: 8. The general case looks more tricky, though.

Refinements on the self type. I.e. Vec8 would be expanded to class Vec8 { this: Vec8 { val self: 8 }}. We do a similar thing for opaque type aliases.

I was thinking whether it is possible to handle it in base type computation logic? Conceptually, it seems to be the same problem as refining types of members with regards to type parameters and prefixes.

odersky · 2023-11-24T09:05:01Z

I was thinking whether it is possible to handle it in base type computation logic? Conceptually, it seems to be the same problem as refining types of members with regards to type parameters and prefixes.

That's an interesting idea, but I am not sure about how this would work in detail?

sjrd · 2023-11-24T09:51:19Z

I don't think baseType is the right solution for this. baseType deals with type parameters and prefixes of parent class types because those things are not otherwise accessible. Also they have to deal with variance. For type and value members, we can select them from outside, and we get refined types through asSeenFrom, not baseType.

Also, baseType is currently guaranteed, by spec, to always return a type of the form p.C[T1, ..., Tn] (or p.C for n = 0). This assumption is relied upon in other parts of the spec that call baseType. It seems unwise to break that contract without thorough analysis of the implications.

liufengyun · 2023-11-24T09:55:42Z

I was thinking whether it is possible to handle it in base type computation logic? Conceptually, it seems to be the same problem as refining types of members with regards to type parameters and prefixes.

That's an interesting idea, but I am not sure about how this would work in detail?

I was thinking that in the following example the parent call Vec(8) gets a refinement type Vec { val size: 8 } from the super constructor call. Then in base type computation (or member type computation), it takes that refinement into consideration.

  trait Vec(tracked val size: Int)
  class Vec8 extends Vec(8):
    val s: 8 = size    // error, but should work

My knowledge is limited regarding the base type computation, just an intuition, so not sure if that would work.

mbovel · 2023-12-04T15:03:08Z

Here are a few notes, most of them coming from discussions we had in person.

Do we need inheritance for classes with `tracked` parameters?

Most of the complexity of this PR comes from allowing extension of classes with tracked parameters. Do we really need this? Or could we allow tracked parameters on final classes only?

Should parameters of `given .. with` automatically be `tracked`?

The point of given .. with is to get a precise type for the declared given. So maybe parameters should be tracked by default in this case?

Interaction with a potential future class constructor sugar

In the future, we might want to introduce a syntactic sugar allowing to refine classes based on their constructor argument types:

class Vec(tracked val size: Int)
val vec: Vec(8)            = Vec(8)
//  vec: Vec {val size: 8} = Vec(8)

For this reason, I was initially more in favor of a parameters-list-wise or class-wise keyword, so that all the argument of the first parameter list are refined, or none.

However, further thinking about it, the constructor sugar might not need to be tighly coupled with the tracked keyword. It's probably okay to use only if all args of the first parameters list are tracked, and to use the usual syntax otherwise:

class Foo(tracked val x: Int, val y: Int)
val foo: Foo {val x: 42} = Foo(42, 43)

class Bar(tracked val x: Int, tracked val y: Int)
val bar: Bar(42, 43) = Bar(42, 43)

Observation: term refs are also kept in refinements

With this PR, we can do:

class VecN(tracked val n: Int) extends Vec(n)
  
val v9 = VecN(9)
val _: Vec { val size: 9 } = v9a

val m: Int = ???
val vm = VecN(m)
val _: Vec { val size: m.type } = vm

So both constant and term-ref types are not widened in refinements. That's probably what we want.

Observation: similarities with `transparent inline given`

What can be achieved with given ... with is somehow similar to what can be achieved with transparent inline given and an anonymous class.

Minimal example:

abstract class Foo:
  val x: Any

// Need `given ... with` here, as `transparent inline given x = ...` is invalid.
given Foo with
  val x: Int = 1

abstract class Bar:
  val y: Any
  type T <: Any

// Similar to `given Bar(using foo: Foo): Bar with`
transparent inline given bar(using foo: Foo): Bar = new Bar:
  val y: foo.x.type = foo.x

@main def demo25 =
  val x0: Int = summon[Foo].x
  val bar = summon[Bar]
  val y0: Int = bar.y

  val bar2 = new Bar:
    val y: Int = 1
    type T = Int
  val _: Bar {
    val y: Int
    type T = Int
  } = bar2

Encoding of the combinators example

import collection.mutable

/// A parser combinator.
trait Combinator[T]:

  /// The context from which elements are being parsed, typically a stream of tokens.
  type Context <: Any
  /// The element being parsed.
  type Element <: Any

  extension (self: T)
    /// Parses and returns an element from `context`.
    def parse(context: Context): Option[Element]
end Combinator

final case class Apply[C, E](action: C => Option[E])
final case class Combine[A, B](first: A, second: B)

transparent inline given apply[C, E]: Combinator[Apply[C, E]] = new Combinator[Apply[C, E]] {
  type Context = C
  type Element = E
  extension(self: Apply[C, E]) {
    def parse(context: C): Option[E] = self.action(context)
  }
}

transparent inline given combine[A, B](
    using f: Combinator[A]
)( // must have two parameter lists, otherwise f.Context is too precise?
    using s: Combinator[B] { type Context = f.Context }
): Combinator[Combine[A, B]] = new Combinator[Combine[A, B]] {
  type Context = f.Context
  type Element = (f.Element, s.Element)
  extension(self: Combine[A, B]) {
    def parse(context: Context): Option[Element] = ???
  }
}

extension [A] (buf: mutable.ListBuffer[A]) def popFirst() =
  if buf.isEmpty then None
  else try Some(buf.head) finally buf.remove(0)

@main def hello: Unit = {
  val source = (0 to 10).toList
  val stream = source.to(mutable.ListBuffer)

  val n = Apply[mutable.ListBuffer[Int], Int](s => s.popFirst())
  val m = Combine(n, n)

  val c = combine(
    using apply[mutable.ListBuffer[Int], Int])(
    using apply[mutable.ListBuffer[Int], Int]
  ) // c can't be inferred
  val r = c.parse(m)(stream)
  val rc: Option[(Int, Int)] = r
  // it would be great if this worked
}

odersky · 2024-01-07T17:39:49Z

This PR now bundles three improvements to modularity, all available under the experimental.modularity language import:

tracked type parameters
refinements in class parents
non-final type export forwarders

The doc page for these changes is

https://github.com/dotty-staging/dotty/blob/add-class-deps/docs/_docs/reference/experimental/modularity.md

The first two commits come from #19392

mushtaq · 2024-01-10T04:10:52Z

How about using dep instead of tracked val?

class D(dep x: C) { type T = x.T }

liufengyun

LGTM, nice generalization to parent refinements 🎉

liufengyun · 2024-01-10T20:31:21Z

compiler/src/dotty/tools/dotc/ast/Desugar.scala

@@ -443,13 +443,13 @@ object desugar {
  private def toDefParam(tparam: TypeDef, keepAnnotations: Boolean): TypeDef = {
    var mods = tparam.rawMods
    if (!keepAnnotations) mods = mods.withAnnotations(Nil)
-    tparam.withMods(mods & (EmptyFlags | Sealed) | Param)
+    tparam.withMods(mods & EmptyFlags | Param)


This is equivalent to just Param?

liufengyun · 2024-01-10T20:44:23Z

compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala

@@ -1049,7 +1050,7 @@ class TreeUnpickler(reader: TastyReader,
      }
      val parentReader = fork
      val parents = readParents(withArgs = false)(using parentCtx)
-      val parentTypes = parents.map(_.tpe.dealias)
+      val parentTypes = parents.map(_.tpe.dealiasKeepAnnots.separateRefinements(cls, null))


Compare this with pickling, it seems we loose symmetry?

liufengyun · 2024-01-10T20:47:01Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

@@ -62,7 +62,7 @@ object Parsers {
    case ExtensionFollow // extension clause, following extension parameter

    def isClass = // owner is a class
-      this == Class || this == CaseClass
+      this == Class || this == CaseClass || this == Given


Consider change the method name or add a comment to avoid misuse --- it's not obvious for Given.

liufengyun · 2024-01-10T21:10:12Z

compiler/src/dotty/tools/dotc/typer/RefChecks.scala

+        || mbr.is(Tracked)
+          // Tracked members correspond to existing val parameters, so they don't
+          // count as deferred. The val parameter could not implement the tracked
+          // refinement since it usually has a wider type.


Reminds me of the erased flag. Might be possible to generalize in the future.

liufengyun · 2024-01-10T21:23:54Z

docs/_docs/reference/experimental/modularity.md

+  def m(): 22
+
+class D extends R:
+  def next(): D


Should class C and D be abstract?

liufengyun · 2024-01-10T21:41:49Z

How about using dep instead of tracked val?
class D(dep x: C) { type T = x.T }

dep is too cryptic as a name --- a full word is better. dependent has been discussed before --- tracked is shorter and nicer.

LPTK · 2024-01-11T06:17:37Z

Why not refined?

tracked evokes the tracking of free variables in capture-tracking. That's the first thing that came to my mind when I saw the keyword.

odersky · 2024-01-11T07:36:17Z

refined works on the class, but not on the parameter (and we need it to work on the parameter, in the end). dependent is too much type theory jargon, it sounds scary.

tracked in its informal meaning in capture tracking and in its meaning here is actually the same thing. If a field of a class was a capability, I would expect it to be tracked, in the sense that we keep track of what the actual capability argument was.

odersky · 2024-01-15T17:13:10Z

Needs minor release since it introduces a new Tasty tag.

smarter · 2024-01-16T20:55:58Z

Another possible keyword here would be precise since at least in spirit this reminds me of scala/improvement-proposals#48 (/cc @soronpo)

soronpo · 2024-01-16T21:42:27Z

Another possible keyword here would be precise since at least in spirit this reminds me of scala/improvement-proposals#48 (/cc @soronpo)

This feature doesn't solve most of the problems the Precise Type SIP targeted so I don't see what is so precise about it. I think dependent fits better and I know nothing about the theory and I'm not scared :) .
Other suggestions: preserved, retained, observed

mushtaq · 2024-01-17T16:07:48Z

dep is too cryptic as a name --- a full word is better. dependent has been discussed before --- tracked is shorter and nicer.

dep is adopted by scala-cli to mean a dependency. In that sense, it is well understood.

My other comment was about the need to write both tracked and val given that tracked is proposed to work only with val parameters.

The rules for export forwarders are changed as follows. Previously, all export forwarders were declared `final`. Now, only term members are declared `final`. Type aliases left aside. This makes it possible to export the same type member into several traits and then mix these traits in the same class. `typeclass-aggregates.scala` shows why this is essential to be able to combine multiple givens with type members. The change does not lose safety since different type aliases would in any case lead to uninstantiatable classes.

Refinements of a class parent are added as synthetic members to the inheriting class. # Conflicts: # compiler/src/dotty/tools/dotc/config/ScalaSettings.scala # compiler/src/dotty/tools/dotc/typer/Implicits.scala # compiler/src/dotty/tools/dotc/typer/Namer.scala # tests/pos/typeclass-aggregates.scala

For a tracked class parameter we add a refinement in the constructor type that the class member is the same as the parameter. E.g. ```scala class C { type T } class D(tracked val x: C) { type T = x.T } ``` This will generate the constructor type: ```scala (x1: C): D { val x: x1.type } ``` Without `tracked` the refinement would not be added. This can solve several problems with dependent class types where previously we lost track of type dependencies.

odersky · 2024-04-07T18:01:39Z

This is part of #20061

odersky force-pushed the add-class-deps branch 2 times, most recently from 02eb2f7 to 0f4aba8 Compare November 19, 2023 09:33

odersky changed the title ~~Test cases for generic parser combinators~~ Experiment: Add tracked modifier to express class parameter dependencies Nov 19, 2023

odersky marked this pull request as draft November 19, 2023 15:17

odersky mentioned this pull request Nov 21, 2023

Stress test for add-class-deps (#18958) #19015

Closed

odersky mentioned this pull request Jan 6, 2024

Chain of two given...with fail to fetch dependent type #13580

Open

odersky force-pushed the add-class-deps branch from 30c78c1 to afefb9e Compare January 7, 2024 17:32

odersky force-pushed the add-class-deps branch from afefb9e to 7ba2303 Compare January 7, 2024 17:51

odersky marked this pull request as ready for review January 7, 2024 17:55

odersky changed the title ~~Experiment: Add tracked modifier to express class parameter dependencies~~ Improvements to Modularity Jan 7, 2024

This was referenced Jan 7, 2024

Allow class parents to be refined types. #19256

Closed

Pre-SIP: Improvements to Type Classes #19395

Closed

odersky requested review from liufengyun and mbovel January 9, 2024 11:11

odersky assigned mbovel Jan 9, 2024

odersky added the needs-minor-release This PR cannot be merged until the next minor release label Jan 9, 2024

liufengyun approved these changes Jan 10, 2024

View reviewed changes

odersky added 6 commits February 2, 2024 14:19

New modularity language import

c403fbf

Allow vals in using clauses of givens

fafeb51

Some tweaks to modularity.md

adff7dc

odersky force-pushed the add-class-deps branch from d5dcbe0 to adff7dc Compare February 2, 2024 13:20

Update MimaFilters

f173142

odersky changed the title ~~Improvements to Modularity~~ Pre SIP: Improvements to Modularity Feb 17, 2024

odersky closed this Apr 7, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pre SIP: Improvements to Modularity #18958

Pre SIP: Improvements to Modularity #18958

odersky commented Nov 17, 2023 •

edited

Loading

odersky commented Nov 17, 2023

odersky commented Nov 17, 2023 •

edited

Loading

odersky commented Nov 19, 2023 •

edited

Loading

liufengyun commented Nov 19, 2023 •

edited

Loading

odersky commented Nov 19, 2023

liufengyun commented Nov 19, 2023

odersky commented Nov 21, 2023

liufengyun commented Nov 22, 2023

odersky commented Nov 22, 2023

odersky commented Nov 22, 2023

liufengyun commented Nov 24, 2023

odersky commented Nov 24, 2023

sjrd commented Nov 24, 2023

liufengyun commented Nov 24, 2023 •

edited

Loading

mbovel commented Dec 4, 2023

odersky commented Jan 7, 2024 •

edited

Loading

mushtaq commented Jan 10, 2024

liufengyun left a comment

liufengyun Jan 10, 2024

liufengyun Jan 10, 2024

liufengyun Jan 10, 2024

liufengyun Jan 10, 2024

liufengyun Jan 10, 2024

liufengyun commented Jan 10, 2024

LPTK commented Jan 11, 2024

odersky commented Jan 11, 2024 •

edited

Loading

odersky commented Jan 15, 2024

smarter commented Jan 16, 2024

soronpo commented Jan 16, 2024 •

edited

Loading

mushtaq commented Jan 17, 2024

odersky commented Apr 7, 2024

Pre SIP: Improvements to Modularity #18958

Pre SIP: Improvements to Modularity #18958

Conversation

odersky commented Nov 17, 2023 • edited Loading

odersky commented Nov 17, 2023

odersky commented Nov 17, 2023 • edited Loading

odersky commented Nov 19, 2023 • edited Loading

liufengyun commented Nov 19, 2023 • edited Loading

odersky commented Nov 19, 2023

liufengyun commented Nov 19, 2023

odersky commented Nov 21, 2023

liufengyun commented Nov 22, 2023

odersky commented Nov 22, 2023

odersky commented Nov 22, 2023

liufengyun commented Nov 24, 2023

odersky commented Nov 24, 2023

sjrd commented Nov 24, 2023

liufengyun commented Nov 24, 2023 • edited Loading

mbovel commented Dec 4, 2023

Do we need inheritance for classes with tracked parameters?

Should parameters of given .. with automatically be tracked?

Interaction with a potential future class constructor sugar

Observation: term refs are also kept in refinements

Observation: similarities with transparent inline given

odersky commented Jan 7, 2024 • edited Loading

mushtaq commented Jan 10, 2024

liufengyun left a comment

Choose a reason for hiding this comment

liufengyun Jan 10, 2024

Choose a reason for hiding this comment

liufengyun Jan 10, 2024

Choose a reason for hiding this comment

liufengyun Jan 10, 2024

Choose a reason for hiding this comment

liufengyun Jan 10, 2024

Choose a reason for hiding this comment

liufengyun Jan 10, 2024

Choose a reason for hiding this comment

liufengyun commented Jan 10, 2024

LPTK commented Jan 11, 2024

odersky commented Jan 11, 2024 • edited Loading

odersky commented Jan 15, 2024

smarter commented Jan 16, 2024

soronpo commented Jan 16, 2024 • edited Loading

mushtaq commented Jan 17, 2024

odersky commented Apr 7, 2024

odersky commented Nov 17, 2023 •

edited

Loading

odersky commented Nov 17, 2023 •

edited

Loading

odersky commented Nov 19, 2023 •

edited

Loading

liufengyun commented Nov 19, 2023 •

edited

Loading

liufengyun commented Nov 24, 2023 •

edited

Loading

Do we need inheritance for classes with `tracked` parameters?

Should parameters of `given .. with` automatically be `tracked`?

Observation: similarities with `transparent inline given`

odersky commented Jan 7, 2024 •

edited

Loading

odersky commented Jan 11, 2024 •

edited

Loading

soronpo commented Jan 16, 2024 •

edited

Loading