Dotty: Dependent Class Types for Scala

[liufengyun]

Dependent Class Types for Scala

Motivation

Scala already supports many variants of _dependent types_ (aka. types that depend on terms), e.g.

• path-dependent types
• dependent method types
• dependent function types
• singleton types
• literal types

The combination of _higher-kinded types_ and _singleton types_ is another
commonly used approach to encode dependent types in Scala:

trait Context {
  type Tree
}

class Helper[T <: Context](val ctx: T) {
  def f(x: Int): ctx.Tree = ???
}

val ctx  : Context   =  ???
val tree : ctx.Tree  =  new Helper[ctx.type](ctx).f(5)

However, the encoding above is tedious in syntax. Instead, most programmers would
expect the following code to work:

trait Context {
  type Tree
}

class Helper(val ctx: Context) {
  def f(x: Int): ctx.Tree = ???
}

val ctx  : Context   =  ???
val tree : ctx.Tree  =  new Helper(ctx).f(5)

Compile the code above in Scala 2.12.4 will result in the following error message:

 found   : _1.ctx.Tree where val _1: Helper
 required: Test.ctx.Tree
  val tree : ctx.Tree  =  new Helper(ctx).f(5)

The fact that classes in Scala are ignorant of _referential equality_ also
limits the expressive power of _dependent function types_. For example, given
the code below, currently it's impossible to implement the function f:

class Animal(name: String)

trait Foo[T]
class Bar(val a: Animal) extends Foo[a.type]

val f : (a: Animal) => Foo[a.type] = ???

If we try to implement f with (a: Animal) => new Bar(a), the Dotty compiler will
generate following error message:

7 |  val f : (a: Animal) => Foo[a.type] = (a: Animal) =>  new Bar(a)
  |                                                           ^^^^^
  |                                                  found:    Bar
  |                                                  required: Foo[Animal(a)]

But the definition of Bar says that any instance of Bar(a) is a subtype of Foo[a.type]!

Related issues: https://github.com/scala/bug/issues/5712, https://github.com/scala/bug/issues/5700, #1262.

Proposal

To address the problems above as well as make dependent types more useful, we
propose _dependent class types_. We introduce an annotation @dependent that can be
used to mark a public field of in a class constructor depenent:

class Animal(name: String)

trait Foo[T]
class Bar(@dependent val a: Animal) extends Foo[a.type]

The compiler should produce a _dependent refinement type_ for dependent class instantiation as follows:

val dog  : Dog =  new Animal("dog")
val bar  : Bar { val a: dog.type @dependent }  =  new Bar(dog)

The subtype checking should allow the following:

// Bar { val a: dog.type @dependent }  <:  Foo[dog.type]
val foo  : Foo[dog.type] = bar

Rules

1. @dependent can only be used in class primary constructor to decorate
   _non-private_, _non-mutable_, _non-lazy_, _non-overloaded_ fields.

2. A depenent refinement type M { val x: T @dependent } is valid if x is a
   _non-private_, _non-mutable_, _non-lazy_, _non-overloaded_ field of M, and
   T is a subtype of M.member(x).

3. If a primary constructor parameter x of a class Bar is annotated with
   @dependent, the return type of the constructor is refined as Bar { val x: x.type @dependent }. The x in x.type refers the constructor parameter, thus the constructor
   has a dependent method type.

4. When getting the base type of a _valid_ dependent refinement type M { val x: T @dependent } for a parent class P, first get the base type B from
   baseType(M, P), then substitute all references to M.member(x) with the
   type T.

Implementation

We don't need syntax change to the language, nor introduce new types in the compiler.

1. We need to introduce an annotation @dependent.

package scala.annotation

final class dependent extends StaticAnnotation

1. We need add checks for valid usage of @dependent in class definitions and dependent refinement types. The checks are better to be done in RefChecks, as they are semantic.

2. We need to update the type checking for constructors, to refine the result type with the dependent refinement { val x: x.type @dependent } if any constructor parameter x is annotated with @dependent. The change in consideration looks like the following:

val oldRetType  = ...
val refinedRetType = termParamss.foldLeft(oldRetType) { (acc, termParams) =>
  termParams.foldLeft(acc) { (acc, termParam) =>
    if (acc.hasDependentAnnotation)
      RefinedType(acc, termParam.name, termParam.termRef)
    else acc
  }
}

1. We need to change base type computation to handle dependent refinements. The change in consideration looks like the following:

case tp @ RefinedType(parent, name, refine) =>
  val res = baseTypeOf(tp.superType)
  if (tp.isDependentRefinement)
    res.subst(tp.nonPrivateMember(name).symbol :: Nil, refine :: Nil)
  else res

Application

Dependent class types can implement ML-like functor modules:

import scala.annotation.dependent

trait Ordering {
  type T
  def compare(t1:T, t2: T): Int
}

class SetFunctor(@dependent val ord: Ordering) {
  type Set = List[ord.T]
  def empty: Set = Nil

  implicit class helper(s: Set) {
    def add(x: ord.T): Set = x :: remove(x)
    def remove(x: ord.T): Set = s.filter(e => ord.compare(x, e) != 0)
    def member(x: ord.T): Boolean = s.exists(e => ord.compare(x, e) == 0)
  }
}

object Test {
  val orderInt = new Ordering {
    type T = Int
    def compare(t1: T, t2: T): Int = t1 - t2
  }

  val IntSet = new SetFunctor(orderInt)
  import IntSet._

  def main(args: Array[String]) = {
    val set = IntSet.empty.add(6).add(8).add(23)
    assert(!set.member(7))
    assert(set.member(8))
  }
}

Change Logs

1. Changed @dep to @dependent, thanks @propensive .
2. Added related issues, thanks @julienrf .
3. Add application about functor modules

[smarter]

class Helper[T <: Context](val ctx: T) {
  def f(x: Int): ctx.Tree = ???
}

val ctx  : Context   =  ???
val tree : ctx.Tree  =  new Helper[ctx.type](ctx).f(5)

You can avoid having to write the type parameter by hand at the use-site by having a Singleton upper bound:

class Helper[T <: Context with Singleton](val ctx: T) {
  def f(x: Int): ctx.Tree = ???
}

val ctx  : Context   =  ???
val tree : ctx.Tree  =  new Helper(ctx).f(5)

[julienrf]

I wholeheartedly support this idea that would save me a lot of lines of code. The workaround based on upper bounded type parameters is inconvenient (see also #1262 where I give more details about that). I don’t understand why we need an annotation for that, though. Why couldn’t that be the default behavior?

Maybe related issues in scala: https://github.com/scala/bug/issues/5712 and https://github.com/scala/bug/issues/5700

[propensive]

I think the use case is very important, though I've never been an advocate of more annotations for Scala, so I'd prefer a solution which avoids them...

...however, if it is the best way, could you use @dependent instead? Using @dep saves only a few characters on a (likely) rarely-used annotation, but comes at the cost of some clarity for people who encounter it for the first time.

[liufengyun]

@julienrf Having it as the default behaviour will generate a lot of refinement types in the compiler, which slows down (sub-)type checking. It's too expensive for a feature that's not widely used. Also, as @smarter pointed out in #1262, it causes user inconvenience in other usages:

val foo1 = new Foo { ... }
val foo2 = new Foo { ... }
var x = new Quux(foo1) // x is inferred to have type `Quux { val foo: foo1.type }`
x = new Quux(foo2) // error: foo2.type does match foo1.type
// To solve this, write "var x: Quux = ..."

[propensive]

Not sure how exactly this would work out, but could you utilize the final keyword to indicate that the types should be dependent? There's already some kind of precedent for using final like this, in that final val x = 1 will be typed as 1, whereas val x = 1 will be typed as Int.

[liufengyun]

Reuse keyword for a language feature would make the keyword mysterious, IMHO. In types, we could remove val to denote a dependent refinement, i.e. to write Bar { a: dog.type } instead of Bar { val a: dog.type @dependent }.

[propensive]

Well, I think in the case of final, that "mysteriousness" is already there in Scala/Dotty, and half of the meaning of final (for me, at least) is that its inferred type will not be widened. That seems to be related to the semantics of @dep...

Though if final were to be chosen, I don't know whether "finality" is what you want, or whether you would want to be able to override these values subclasses. But subtyping introduces a large amount of additional complexity, and if it's not useful (maybe @julienrf has some ideas about this...?), then making dependent-typing go hand-in-hand with the finality of parameters would be a convenient way to avoid having to explore this complexity.

It would be like, "you can use this feature, but if you do, you lose the ability to change the value and its type in a subclass". It doesn't seem so bad to avoid the intersection of two subtle features by making them into just one.

[liufengyun]

I see your point @propensive , we can consider it if there is known incompatibility of this proposal and subclass/overidding. In absence of known major incompatibilities, it seems difficult to justify the design decision from the theoretical perspective. The justification from ergonomics and worry about potential uncertain issues is not strong enough.

[propensive]

Yes, I'm not 100% sure it's right solution, but I would have said exactly the same about the use of final to preserve singleton types in assignments... But the best thing to do would be to explore it further!

[Blaisorblade]

Cool that you’re looking into this! Here and elsewhere, it looks to me like it’s often hard to use certain features of the Scala core—Scala supports many forms of abstractions from ML modules (and it is designed to do so), they’re just hard to use.

Well, I think in the case of final, that "mysteriousness" is already there in Scala/Dotty, and half of the meaning of final (for me, at least) is that its inferred type will not be widened. That seems to be related to the semantics of @dep...
[... discussion about the other meanings of final...]

I’m not happy about overloading final as “no widening”: final is described as matching Java’s final and meaning “immutable” and “not overridable”. However, it’s true that since val is already immutable, final val was a redundant combination, so I guess that’s why it took the new meaning. If nowadays final in this context (actually, which one?) has a meaning, overloading it seems... worse?

[smarter]

What if we had a dependent class desugaring that worked a bit like the case class desugaring, e.g. given:

trait Context {
  type Tree
}

the user write:

dependent class Helper(val ctx: Context) {
  def f(x: Int): ctx.Tree = ???
}

and we generate:

class Helper(val ctx: Context) {
  def f(x: Int): ctx.Tree = ???
}
object Helper {
  def apply(ctx0: Context): Helper { val ctx: ctx0.type } = {
    class Helper0(ctx: ctx0.type) extends Helper(ctx)
    new Helper0(ctx0)
  }
}

Then the following code would compile:

object Test {
  val ctx  : Context   =  ???
  val tree : ctx.Tree  =  Helper(ctx).f(5)
}

[smarter]

We could also avoid having to create a subclass by using a cast in the implementation:

  def apply(ctx0: Context): Helper { val ctx: ctx0.type } = {
    new Helper(ctx0).asInstanceOf[Helper { val ctx: ctx0.type }]
  }

[julienrf]

But subtyping introduces a large amount of additional complexity, and if it's not useful (maybe @julienrf has some ideas about this...?), then making dependent-typing go hand-in-hand with the finality of parameters would be a convenient way to avoid having to explore this complexity.

When I use dependent types with val members in traits (as opposed to constructor parameters of classes), yes, I find it sometimes useful to narrow the type of the val. Here is an example from https://github.com/julienrf/endpoints.

[propensive]

@Blaisorblade final val isn't a redundant combination, though. If we have,

class Bar() extends Foo(0) { override val x = 1 }

that will work if Foo is defined as class Foo(val x: Int) but not for class Foo(final val x: Int).

Also, I'm not sure I got your question and/or point at the end about overloading the meaning of final. ;) I would agree the English word final implies nothing about not-widening, so my suggestion was only in the context given final already has this additional meaning in both Scala and Dotty. "Additional", and seemingly orthogonal, but actually it's rare that you would care about both the finality of a val and its singleton type, such that you would want to control them both independently.

I sort of see it as a few separate questions:

1. Should finality and non-widening of the type be inseparably "the same" feature?
2. Is the "surprising" feature of non-widening less surprising ("better") if it applies to a smaller set of cases, or if it applies more consistently in more places?
3. Should this feature be called final?
   where the answer to (3) is "probably not, but that ship has sailed".

[liufengyun]

The following code (which compiles and runs with #3936 ) shows that _dependent class types_ can implement ML-like functor modules:

import scala.annotation.dependent

trait Ordering {
  type T
  def compare(t1:T, t2: T): Int
}

class SetFunctor(@dependent val ord: Ordering) {
  type Set = List[ord.T]
  def empty: Set = Nil

  implicit class helper(s: Set) {
    def add(x: ord.T): Set = x :: remove(x)
    def remove(x: ord.T): Set = s.filter(e => ord.compare(x, e) != 0)
    def member(x: ord.T): Boolean = s.exists(e => ord.compare(x, e) == 0)
  }
}

object Test {
  val orderInt = new Ordering {
    type T = Int
    def compare(t1: T, t2: T): Int = t1 - t2
  }

  val IntSet = new SetFunctor(orderInt)
  import IntSet._

  def main(args: Array[String]) = {
    val set = IntSet.empty.add(6).add(8).add(23)
    assert(!set.member(7))
    assert(set.member(8))
  }
}

[liufengyun]

@smarter Making dependent as a keyword and use desugaring is an interesting idea. The only worry is that it's not specific enough about which field is dependent. Also, it seems it cannot make the following type check, unless we change how computeBaseType works as what's done in #3936 :

// Bar { val a: dog.type @dependent }  <:  Foo[dog.type]
val foo  : Foo[dog.type] = bar

[Blaisorblade]

@liufengyun That’s cool! I’d love to see how much can be conveniently encoded, including sharing constraints and so on. I’d like to try encoding the examples from my Scala’16 talk, and look for better ones from the literature.

[liufengyun]

From a discussion with @julienrf , I'm convinced that his proposal in #1262 makes sense and it is a better proposal. His proposal overlaps with this one, but it's more coherent with the language/compiler, and it's practical enough to solve real world problems.

_Dependent class types_ can become tricky with subtyping and correct compiler implementation, and its theoretical foundation is unknown. I'd like to keep it as a separate research instead of proposing it as a language feature.

Thus I'm closing the issue for now. We can continue research discussions offline or by email.

[Blaisorblade]

@liufengyun @julienrf Right now both #1262 and this proposal are closed. Is the plan to proceed on #1262 or to do more research on this? EDIT: or to... keep thinking about the problem without any open issue to track it?

[mdedetrich]

I actually really like the proposal said here https://github.com/lampepfl/dotty/issues/3920#issuecomment-361248494 with the caveat that @dependant should not be an annotation and it instead should be an actual keyword (i.e. dependant)

I agree with @Blaisorblade here though, both tickets are now closed which implies that none of the approaches are being considered?

[liufengyun]

The problem with this proposal is that it doesn't work with _trait parameters_, thus this proposal is proposing an _incoherent_ language feature.

Currently abstract member of trait or class will get a refinement type:

trait Animal
class Dog extends Animal
class Cat extends Animal

abstract class Bar { val x: Animal }
val bar: Bar { val x: Cat } = new Bar { val x = new Cat }

trait Foo { val x: Animal }
val foo: Foo { val x: Cat } = new Foo { val x = new Cat }

As convincingly argued by @julienrf , there should be a _symmetry_ if the members are in the constructor positions:

abstract class Bar(val x: Animal)
val bar: Bar { val x: Cat } = new Bar(new Cat) {}  // error

trait Foo(val x: Animal)
val foo: Foo { val x: Cat } = new Foo(new Cat) {} // error

If such symmetry exists, it will be sufficient for most important usage in practice, thus makes this proposal not so useful.

[mdedetrich]

@liufengyun Maybe we should reopen the other ticket then?

[julienrf]

Actually my initial proposal is not applicable because it would cause too much type refinements. We have to improve it. I think the direction proposed in this proposal is very nice, it is not clear to me why it can not be applied to trait parameters?

[liufengyun]

@julienrf I was wrong, it could work with traits, but still it introduces an unfriendly syntax for an important language feature, it doesn't seem to be an elegant design.

Instead, during a discussion about this in the morning meeting, people tend to agree with your argument that the symmetry of type checking behaviour is well-founded, and we should try to do that for traits and abstract classes without introducing an annotation like @dependent. If we only do that for traits and abstract classes, I think it addresses your worry about proliferation of type refinements.