From 2ffc7cfaf05217394708d2c00ab85ab07663d03c Mon Sep 17 00:00:00 2001
From: Felix Mulder <felix.mulder@gmail.com>
Date: Fri, 7 Oct 2016 14:35:35 +0200
Subject: Migrate dotty.epfl.ch to static site in repository

---
 docs/docs/internals/type-system.md | 134 +++++++++++++++++++++++++++++++++++++
 1 file changed, 134 insertions(+)
 create mode 100644 docs/docs/internals/type-system.md

(limited to 'docs/docs/internals/type-system.md')

diff --git a/docs/docs/internals/type-system.md b/docs/docs/internals/type-system.md
new file mode 100644
index 000000000..191c107cf
--- /dev/null
+++ b/docs/docs/internals/type-system.md
@@ -0,0 +1,134 @@
+---
+layout: default
+---
+
+Type System
+===========
+The types are defined in [dotty/tools/dotc/core/Types.scala][1]
+
+## Class diagram ##
+- [PDF][2], generated with [a fork of scaladiagrams][3]
+
+## Proxy types and ground types ##
+A type which inherits `TypeProxy` is a proxy for another type accessible using
+the `underlying` method, other types are called _ground_ types and inherit
+`CachedGroundType` or `UncachedGroundType`.
+
+```
+Type -+- ProxyType --+- NamedType ----+--- TypeRef
+      |              |                 \
+      |              +- SingletonType-+-+- TermRef
+      |              |                |
+      |              |                +--- ThisType
+      |              |                +--- SuperType
+      |              |                +--- ConstantType
+      |              |                +--- MethodParam
+      |              |                +--- RefinedThis
+      |              +- PolyParam
+      |              +- RefinedType
+      |              +- TypeBounds
+      |              +- ExprType
+      |              +- AnnotatedType
+      |              +- TypeVar
+      |
+      +- GroundType -+- AndType
+                     +- OrType
+                     +- MethodType -----+- ImplicitMethodType
+                     |                  +- JavaMethodType
+                     +- PolyType
+                     +- ClassInfo
+                     |
+                     +- NoType
+                     +- NoPrefix
+                     +- ErrorType
+                     +- WildcardType
+
+```
+
+## Representations of types ##
+ Type                      | Representation
+ ------------------------- | -----------------------------
+ `p.x.type`                | `TermRef(p, x)`
+ `p#T`                     | `TypeRef(p, T)`
+ `p.x.T` == `p.x.type#T`   | `TypeRef(TermRef(p, x), T)`
+ `this.type`               | `ThisType`
+ `A & B`                   | `AndType(A, B)`
+ `A | B`                   | `OrType(A, B)`
+ `=> T`                    | `ExprType(T)`
+ `p { refinedName }`       | `RefinedType(p, refinedName)`
+ type of the value `super` | `SuperType`
+ `type T >: A <: B`        | `TypeRef` with underlying type `RealTypeBounds(A, B)`
+ `type T = A`              | `TypeRef` with underlying type `TypeAlias(A)`
+ `class p.C ...`           | `ClassInfo(p, C, ...)`
+
+### Representation of methods ###
+```scala
+def f[A, B <: Ord[A]](x: A, y: B): Unit
+```
+is represented as:
+
+```scala
+val p = PolyType(List("A", "B"))(
+  List(TypeBounds(Nothing, Any),
+       TypeBounds(Nothing,
+         RefinedType(Ordering,
+           scala$math$Ordering$$T, TypeAlias(PolyParam(p, 0))))),
+  m)
+
+val m = MethodType(List("x", "y"),
+  List(PolyParam(p, 0), PolyParam(p, 1)))(Unit)
+```
+(This is a slightly simplified version, e.g. we write `Unit` instead of
+`TypeRef(TermRef(ThisType(TypeRef(NoPrefix,<root>)),scala),Unit)`).
+
+Note that a PolyParam refers to a type parameter using its index (here A is 0
+and B is 1).
+
+## Subtyping checks ##
+`topLevelSubType(tp1, tp2)` in [dotty/tools/dotc/core/TypeComparer.scala][4]
+checks if `tp1` is a subtype of `tp2`.
+
+### Type rebasing ###
+**FIXME**: This section is no longer accurate because
+https://github.com/lampepfl/dotty/pull/331 changed the handling of refined
+types.
+
+Consider [tests/pos/refinedSubtyping.scala][5]
+```scala
+class Test {
+
+  class C { type T; type Coll }
+
+  type T1 = C { type T = Int }
+
+  type T11 = T1 { type Coll = Set[Int] }
+
+  type T2 = C { type Coll = Set[T] }
+
+  type T22 = T2 { type T = Int }
+
+  var x: T11 = _
+  var y: T22 = _
+
+  x = y
+  y = x
+
+}
+```
+We want to do the subtyping checks recursively, since it would be nice if we
+could check if `T22 <: T11` by first checking if `T2 <: T1`. To achieve this
+recursive subtyping check, we remember that `T2#T` is really `T22#T`. This
+procedure is called rebasing and is done by storing refined names in
+`pendingRefinedBases` and looking them up using `rebase`.
+
+## Type caching ##
+TODO
+
+## Type inference via constraint solving ##
+TODO
+
+[1]: https://github.com/lampepfl/dotty/blob/master/src/dotty/tools/dotc/core/Types.scala
+[2]: https://github.com/samuelgruetter/dotty/blob/classdiagrampdf/dotty-types.pdf
+[3]: https://github.com/samuelgruetter/scaladiagrams/tree/print-descendants
+[4]: https://github.com/lampepfl/dotty/blob/master/src/dotty/tools/dotc/core/TypeComparer.scala
+[5]: https://github.com/lampepfl/dotty/blob/master/tests/pos/refinedSubtyping.scala
-- 
cgit v1.2.3