Path dependent types (on types and on inner classes)

Question

While experimenting with path dependent types, I experienced some unexpected results:

object Funny1 {
  class X {
    type Y = String
    val y: Y = "y"
  }

  val x1 = new X
  val x2 = new X

  def foo(x: X)(y: x.Y): Unit = ()
  def foo_diff(y1: x1.Y)(y2: x2.Y): Unit = () // 1.3
  def foo_gen(y1: X#Y)(y2: X#Y) : Unit = ()

  foo(x1)(x1.y)
  foo(x1)(x2.y) // <-- 1.1 would expect this to fail

  foo_diff(x1.y)(x2.y)
  foo_diff(x2.y)(x2.y) // <-- 1.2 would expect this to fail

  foo_gen(x1.y)(x2.y)
  foo_gen(x2.y)(x2.y)
}


object Funny2 {
  class X {
    class Y {
    }
  }

  val x1 = new X
  val x2 = new X

  val x1y = new x1.Y
  val x2y = new x2.Y

  def foo(x: X)(y: x.Y): Unit = ()
  def foo_diff(y1: x1.Y)(y2: x2.Y): Unit = ()
  def foo_gen(y1: X#Y)(y2: X#Y) : Unit = ()

  foo(x1)(x1y)
  // foo(x1)(x2y) // does not compile

  foo_diff(x1y)(x2y)
  // foo_diff(x2y)(x2y) // does not compile

  foo_gen(x1y)(x2y)
  foo_gen(x2y)(x2y)
}

object Funny3 {
  trait X {
    type Y
    def y: Y
  }

  val x1 = new X {
    override type Y = String

    override def y: String = "y"
  }
  val x2 = new X {
    override type Y = Int

    override def y: Int = 3
  }

  def foo(x: X)(y: x.Y): Unit = ()
  def foo_diff(y1: x1.Y)(y2: x2.Y): Unit = ()
  def foo_gen(y1: X#Y)(y2: X#Y) : Unit = ()

  foo(x1)(x1.y)
  // foo(x1)(x2.y)    // 3.1 fails as expected

  foo_diff(x1.y)(x2.y)
  // foo_diff(x2.y)(x2.y)  // 3.2 fails as expected

  foo_gen(x1.y)(x2.y)
  foo_gen(x2.y)(x2.y)
}



object Funny3b {
  trait X {
    type Y
    def y: Y
  }

  val x1 = new X {
    override type Y = String

    override def y: String = "y"
  }
  val x2 = new X {
    override type Y = String

    override def y: String = "y2"
  }

  def foo(x: X)(y: x.Y): Unit = ()
  def foo_diff(y1: x1.Y)(y2: x2.Y): Unit = ()
  def foo_gen(y1: X#Y)(y2: X#Y) : Unit = ()

  foo(x1)(x1.y)
  foo(x1)(x2.y)    // 3b.1 does not fail

  foo_diff(x1.y)(x2.y)
  foo_diff(x2.y)(x2.y)  // 3b.2 does not fail

  foo_gen(x1.y)(x2.y)
  foo_gen(x2.y)(x2.y)
}

Especially, I am interested in the answers to the questions:

Why do the line marked 1.1 and 1.2) compile?
Why is no reference to x as first parameter required in 1.3 foo_diff ?
Why do the lines 3.1 and 3.2 not compile, but 3b.1 and 3b.2 compile? Especially as the path dependency seems to be "lost" in 3b, if underlying types can be resolved to be identical (here: String).

Thanks, Martin

user_182660 · Answer

I think the fundamental misunderstanding that underlies all of your question is that you assume that a construction:

trait / class ClassName {
  type T = something
}

creates a dependent type. It doesn't. If you open the subsection 3.5.1 Equivalence of the section 3.5 "Relations between types" of the spec, you may see that:

If t is defined by a type alias type t = T, then t is equivalent to T.

That's why in your first example for example, compiler sees x1.Y and x2.Y and X#Y as just String. If you substitute all that with just String there are no questions left on why that code compiles.

Similarly your 3rd example just define some aliases. If you substitute those aliases with their definitions, it again becomes quite clear why that code compiles and fails.

Your second example uses a different construct

trait / class ClassName {
  trait / class InnerName
}

This is the construct that creates a path-dependent type and thus the code you expect to not compile actually fails. According to my understanding this is the only of your examples that really involves dependent types.

Also if you open Tour of Scala articles Abstract Type Members and Inner Classes that describe the first and the second construction, you might notice that only the latter (but not the former!) mentions the "path-dependent types".

Path dependent types (on types and on inner classes)

1 Answers