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: scala/bug#5712, scala/bug#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

2. 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.

3. 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
  }
}

4. 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: scala/bug#5712 and scala/bug#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 }]
  }