Differences between Dotty and DOT - smarter/dotty GitHub Wiki

Dotty's type system is based on the DOT calculus but is much more rich, this page attempts to list the differences between the two but is not exhaustive. Note that both DOT and Dotty are in-progress work, so this page may change.

Features of Dotty's type system not present in DOT

  • Type parameters, higher-kinded types and existential types. They are encoded using refinement types, see docs/HigherKinded-v2.md
  • Variance annotations (similiar to SLS 4.5, Dotty additionally has variance annotations on type members).
  • Singleton types like x.type (see SLS 3.2.1)
    • The compiler has to be careful to detect cyclic type definitions involving singleton types like tests/neg/cycles.scala
  • Type projections like T#X (see SLS 3.2.2)

    • They are used to represent Java inner classes and to implement type lambdas in docs/HigherKinded-v2.md, the section Status of # describes their proposed meaning in Dotty.

    • See https://github.com/lampepfl/dotty/pull/271#issuecomment-67288571 for a recent discussion on them.

    • They break subtyping transitivity:

      class A { type T }
class B extends A { override type T = Int }
class C extends A { override type T = String }

      (B & C)#T is an abstract type lower-bounded by (Int | String) and upper-bounded by (Int & String) (cf. the declaration lattice of DOT). This means that Int <: (B & C)#T and (B & C)#T <: String

    • Internally, path-dependent types like p.T are implemented as p.type#T, (cf. Representation of types)

  • Class types.

    • They can only extend other class types, this excludes types like X & Y or X { type T = Int }, but includes parameterized types like List[Int] even though they're implemented using refined types (cf. docs/HigherKinded-v2.md)

    • Modeling them is not necessary because they're essentially refinement types with names, for example, we can replace

      class X
class A extends X {
  type T = String
  def f: Int = 1
}
object O {
  val a: A = new A
}

      by

      class X
object O {
  type StructuralA = X { type T = String; def f: Int }
  val a: StructuralA = new X { type T = String; def f: Int = 1 }
}

      Note that A <: StructuralA

  • Type aliases like type T = A.
    • They are very similar to bounded abstract types like type T >: A <: A, but class X extends T only works with type aliases.

Differences between DOT and Dotty for the types they have in common