1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
Differences between DOT and Dotty
=================================
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 [Higher Kinded v2]
* 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 [Higher Kinded v2], the section [Status of#] describes their proposed
meaning in Dotty.
- See [#271] for a recent discussion on them.
- They break subtyping transitivity:
```scala
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. [Higher Kinded v2])
- Modeling them is not necessary because they're essentially refinement types
with names, for example, we can replace
```scala
class X
class A extends X {
type T = String
def f: Int = 1
}
object O {
val a: A = new A
}
```
by
```scala
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
The exact rules for what constitute a valid refinement type in Dotty are not
fixed yet, see [checkRefinementNonCyclic]
[DOT calculus]: http://lampwww.epfl.ch/~amin/dot/fool.pdf
[Higher Kinded v2]: https://github.com/lampepfl/dotty/blob/master/docs/internals/higher-kinded-v2.md
[SLS 4.5]: http://www.scala-lang.org/files/archive/spec/2.11/04-basic-declarations-and-definitions.html#variance-annotations
[SLS 3.2.1]: http://www.scala-lang.org/files/archive/spec/2.11/03-types.html#singleton-types
[tests/neg/cycles.scala]: https://github.com/lampepfl/dotty/blob/master/tests/neg/cycles.scala
[SLS 3.2.2]: http://www.scala-lang.org/files/archive/spec/2.11/03-types.html#type-projection
[Status of#]: https://github.com/lampepfl/dotty/blob/master/docs/HigherKinded-v2.md#status-of-
[#271]: https://github.com/lampepfl/dotty/pull/271#issuecomment-67288571
[Representation of types]: https://github.com/smarter/dotty/wiki/Type-System-Internals#representations-of-types
[checkRefinementNonCyclic]: https://github.com/lampepfl/dotty/blob/master/src/dotty/tools/dotc/typer/Checking.scala#L190
|