Browse files

types chapter fully converted. Added link to jquery and some experime…

…ntal

code for a fixed pop-out version of the table of contents, which is
currently disabled.
  • Loading branch information...
1 parent 3340862 commit bb53357a77105d4c01cc0c7566497f05a7620878 @iainmcgin iainmcgin committed Oct 26, 2012
Showing with 480 additions and 425 deletions.
  1. +3 −3 03-lexical-syntax.md
  2. +12 −12 04-identifiers-names-and-scopes.md
  3. +399 −406 05-types.md
  4. +6 −0 16-references.md
  5. +16 −1 README.md
  6. +3 −2 build.sh
  7. +20 −0 resources/ScalaReference.js
  8. +2 −0 resources/scala-ref-template.html5
  9. +19 −1 resources/style.css
View
6 03-lexical-syntax.md
@@ -23,7 +23,7 @@ classes (Unicode general category given in parentheses):
#. Whitespace characters. `\u0020 | \u0009 | \u000D | \u000A`{.grammar}
#. Letters, which include lower case letters(Ll), upper case letters(Lu),
titlecase letters(Lt), other letters(Lo), letter numerals(Nl) and the
- two characters \\u0024 ‘$’ and \\u005F ‘_’, which both count as upper case
+ two characters \\u0024 ‘\\$’ and \\u005F ‘_’, which both count as upper case
letters
#. Digits ` ‘0’ | … | ‘9’ `{.grammar}
#. Parentheses ` ‘(’ | ‘)’ | ‘[’ | ‘]’ | ‘{’ | ‘}’ `{.grammar}
@@ -70,9 +70,9 @@ decomposes into the three identifiers `big_bob`, `++=`, and
_variable identifiers_, which start with a lower case letter, and
_constant identifiers_, which do not.
-The ‘$’ character is reserved
+The ‘\$’ character is reserved
for compiler-synthesized identifiers. User programs should not define
-identifiers which contain ‘$’ characters.
+identifiers which contain ‘\$’ characters.
The following names are reserved words instead of being members of the
syntactic class `id` of lexical identifiers.
View
24 04-identifiers-names-and-scopes.md
@@ -41,18 +41,18 @@ val x = 1;
neither binding of `x` shadows the other. Consequently, the
reference to `x` in the third line above would be ambiguous.
-A reference to an unqualified (type- or term-) identifier _x_ is bound
+A reference to an unqualified (type- or term-) identifier $x$ is bound
by the unique binding, which
- defines an entity with name $x$ in the same namespace as the identifier, and
-- shadows all other bindings that define entities with name _x_ in that
+- shadows all other bindings that define entities with name $x$ in that
namespace.
-It is an error if no such binding exists. If _x_ is bound by an
-import clause, then the simple name _x_ is taken to be equivalent to
-the qualified name to which _x_ is mapped by the import clause. If _x_
-is bound by a definition or declaration, then _x_ refers to the entity
-introduced by that binding. In that case, the type of _x_ is the type
+It is an error if no such binding exists. If $x$ is bound by an
+import clause, then the simple name $x$ is taken to be equivalent to
+the qualified name to which $x$ is mapped by the import clause. If $x$
+is bound by a definition or declaration, then $x$ refers to the entity
+introduced by that binding. In that case, the type of $x$ is the type
of the referenced entity.
(@) Assume the following two definitions of a objects named
@@ -95,9 +95,9 @@ of the referenced entity.
}}}}}}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A reference to a qualified (type- or term-) identifier `e.x` refers to
-the member of the type _T_ of _e_ which has the name _x_ in the same
-namespace as the identifier. It is an error if _T_ is not a
-[value type](#value-types). The type of `e.x` is the member type of the
-referenced entity in _T_.
+A reference to a qualified (type- or term-) identifier $e.x$ refers to
+the member of the type $T$ of $e$ which has the name $x$ in the same
+namespace as the identifier. It is an error if $T$ is not a
+[value type](#value-types). The type of $e.x$ is the member type of the
+referenced entity in $T$.
View
805 05-types.md
@@ -29,12 +29,12 @@ Value types are either _concrete_ or _abstract_.
Every concrete value type can be represented as a _class type_, i.e. a
[type designator](#type-designators) that refers to a
-a [class or a trait](#class-definitions) [^1], or as a
+[class or a trait](#class-definitions) [^1], or as a
[compound type](#compound-types) representing an
intersection of types, possibly with a [refinement](#compound-types)
that further constrains the types of its members.
<!--
-A shorthand exists for denoting function types (\sref{sec:function-types}).
+A shorthand exists for denoting [function types](#function-types)
-->
Abstract value types are introduced by [type parameters](#type-parameters)
and [abstract type bindings](#type-declarations-and-type-aliases).
@@ -76,21 +76,21 @@ and in that function form a central role in Scala's type system.
A path is one of the following.
- The empty path ε (which cannot be written explicitly in user programs).
-- `C.this`, where _C_ references a class.
- The path `this` is taken as a shorthand for `C.this` where
- _C_ is the name of the class directly enclosing the reference.
-- `p.x` where _p_ is a path and _x_ is a stable member of _p_.
+- `$C$.this`, where $C$ references a class.
+ The path `this` is taken as a shorthand for `$C$.this` where
+ $C$ is the name of the class directly enclosing the reference.
+- `$p$.$x$` where $p$ is a path and $x$ is a stable member of $p$.
_Stable members_ are packages or members introduced by object definitions or
by value definitions of [non-volatile types](#volatile-types).
-- `C.super.x` or `C.super[M].x`
- where _C_ references a class and _x_ references a
- stable member of the super class or designated parent class _M_ of _C_.
- The prefix `super`{.scala} is taken as a shorthand for `C.super` where
- _C_ is the name of the class directly enclosing the reference.
-
+- `$C$.super.$x$` or `$C$.super[$M$].$x$`
+ where $C$ references a class and $x$ references a
+ stable member of the super class or designated parent class $M$ of $C$.
+ The prefix `super`{.scala} is taken as a shorthand for `$C$.super` where
+ $C$ is the name of the class directly enclosing the reference.
A _stable identifier_ is a path which ends in an identifier.
+
Value Types
-----------
@@ -103,10 +103,10 @@ forms.
SimpleType ::= Path ‘.’ type
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A singleton type is of the form `p.type`{.scala}, where _p_ is a
+A singleton type is of the form `$p$.type`{.scala}, where $p$ is a
path pointing to a value expected to [conform](#expression-typing)
to `scala.AnyRef`{.scala}. The type denotes the set of values
-consisting of `null`{.scala} and the value denoted by _p_.
+consisting of `null`{.scala} and the value denoted by $p$.
A _stable type_ is either a singleton type or a type which is
declared to be a subtype of trait `scala.Singleton`{.scala}.
@@ -117,12 +117,13 @@ declared to be a subtype of trait `scala.Singleton`{.scala}.
SimpleType ::= SimpleType ‘#’ id
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A type projection `T#x`{.scala} references the type member named
-_x_ of type _T_.
+A type projection `$T$#$x$`{.scala} references the type member named
+$x$ of type $T$.
<!--
The following is no longer necessary:
-If $x$ references an abstract type member, then $T$ must be a stable type (\sref{sec:singleton-types}).
+If $x$ references an abstract type member, then $T$ must be a
+[stable type](#singleton-types)
-->
### Type Designators
@@ -134,22 +135,22 @@ SimpleType ::= StableId
A type designator refers to a named value type. It can be simple or
qualified. All such type designators are shorthands for type projections.
-Specifically, the unqualified type name _t_ where _t_ is bound in some
-class, object, or package _C_ is taken as a shorthand for
-`C.this.type#t`{.scala}. If _t_ is
-not bound in a class, object, or package, then _t_ is taken as a
-shorthand for `ε.type#t`.
+Specifically, the unqualified type name $t$ where $t$ is bound in some
+class, object, or package $C$ is taken as a shorthand for
+`$C$.this.type#$t$`{.scala}. If $t$ is
+not bound in a class, object, or package, then $t$ is taken as a
+shorthand for `ε.type#$t$`.
A qualified type designator has the form `p.t` where `p` is
a [path](#paths) and _t_ is a type name. Such a type designator is
equivalent to the type projection `p.type#t`{.scala}.
(@) Some type designators and their expansions are listed below. We assume
- a local type parameter _t_, a value `maintable`
- with a type member `Node` and the standard class `scala.Int`,
+ a local type parameter $t$, a value `maintable`
+ with a type member `Node` and the standard class `scala.Int`{.scala},
-------------------- --------------------------
- t $\epsilon$.type#t
+ t ε.type#t
Int scala.type#Int
scala.Int scala.type#Int
data.maintable.Node data.maintable.type#Node
@@ -163,16 +164,16 @@ SimpleType ::= SimpleType TypeArgs
TypeArgs ::= ‘[’ Types ‘]’
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A parameterized type T[ U~1~ , , U~n~ ] consists of a type
-designator _T_ and type parameters _U~1~ , , U~n~_ where
-_n ≥ 1_. _T_ must refer to a type constructor which takes _n_ type
-parameters _a~1~ , , s a~n~_.
+A parameterized type $T[ U_1 , \ldots , U_n ]$ consists of a type
+designator $T$ and type parameters $U_1 , \ldots , U_n$ where
+$n \geq 1$. $T$ must refer to a type constructor which takes $n$ type
+parameters $a_1 , \ldots , a_n$.
-Say the type parameters have lower bounds _L~1~ , , L~n~_ and
-upper bounds _U~1~ … U~n~_. The parameterized type is
+Say the type parameters have lower bounds $L_1 , \ldots , L_n$ and
+upper bounds $U_1 , \ldots , U_n$. The parameterized type is
well-formed if each actual type parameter
-_conforms to its bounds_, i.e. _σ L~i~ <: T~i~ <: σ U~i~_ where σ is the
-substitution [ _a~1~_ := _T~1~_ , , _a~n~_ := _T~n~_ ].
+_conforms to its bounds_, i.e. $σ L_i <: T_i <: σ U_i$ where $σ$ is the
+substitution $[ a_1 := T_1 , \ldots , a_n := T_n ]$.
(@param-types) Given the partial type definitions:
@@ -219,8 +220,8 @@ substitution [ _a~1~_ := _T~1~_ , … , _a~n~_ := _T~n~_ ].
SimpleType ::= ‘(’ Types ‘)’
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A tuple type (T~1~ , , T~n~) is an alias for the
-class `scala.Tuple`~n~`[`T~1~`, … , `T~n~`]`, where _n ≥ 2_.
+A tuple type $(T_1 , \ldots , T_n)$ is an alias for the
+class `scala.Tuple$_n$[$T_1$, … , $T_n$]`, where $n \geq 2$.
Tuple classes are case classes whose fields can be accessed using
selectors `_1` , … , `_n`. Their functionality is
@@ -230,14 +231,14 @@ standard Scala library (they might also add other methods and
implement other traits).
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ {.scala}
-case class Tuple_n[+T1, … , +Tn](_1: T1, … , _n: Tn)
-extends Product_n[T1, … , Tn] {}
+case class Tuple$n$[+T1, … , +$T_n$](_1: T1, … , _n: $T_n$)
+extends Product_n[T1, … , $T_n$] {}
-trait Product_n[+T1, … , +Tn] {
- override def arity = n
+trait Product_n[+T1, … , +$T_n$] {
+ override def arity = $n$
def _1: T1
- def _n: Tn
+ def _n: $T_n$
}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -247,9 +248,9 @@ trait Product_n[+T1, … , +Tn] {
AnnotType ::= SimpleType {Annotation}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-An annotated type _T a~1~ , , a~n~_
+An annotated type $T$ `$a_1 , \ldots , a_n$`
attaches [annotations](#user-defined-annotations)
-_a~1~ , , a~n~_ to the type _T_.
+$a_1 , \ldots , a_n$ to the type $T$.
(@) The following type adds the `@suspendable`{.scala} annotation to the type
`String`{.scala}:
@@ -270,12 +271,12 @@ RefineStat ::= Dcl
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A compound type `T1 with … with Tn { R }`
+A compound type `$T_1$ with … with $T_n$ { $R$ }`
represents objects with members as given in the component types
-_T1 , , Tn_ and the refinement `{ R }`. A refinement
-`{ R }` contains declarations and type definitions.
+$T_1 , \ldots , T_n$ and the refinement `{ $R$ }`. A refinement
+`{ $R$ }` contains declarations and type definitions.
If a declaration or definition overrides a declaration or definition in
-one of the component types _T1 , , T_n_, the usual rules for
+one of the component types $T_1 , \ldots , T_n$, the usual rules for
[overriding](#overriding) apply; otherwise the declaration
or definition is said to be “structural” [^2].
@@ -291,11 +292,11 @@ definition within the refinement. This restriction does not apply to
the function's result type.
If no refinement is given, the empty refinement is implicitly added,
-i.e.\ `T1 with … with Tn`{.scala} is a shorthand for
-`T1 with … with Tn {}`{.scala}.
+i.e.\ `$T_1$ with … with $T_n$`{.scala} is a shorthand for
+`$T_1$ with … with $T_n$ {}`{.scala}.
A compound type may also consist of just a refinement
-`{ R }` with no preceding component types. Such a type is
+`{ $R$ }` with no preceding component types. Such a type is
equivalent to `AnyRef{ R }`{.scala}.
(@) The following example shows how to declare and use a function which
@@ -335,10 +336,11 @@ equivalent to `AnyRef{ R }`{.scala}.
InfixType ::= CompoundType {id [nl] CompoundType}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-An infix type _T~1~ op T~2~_ consists of an infix
-operator _op_ which gets applied to two type operands _T~1~_ and
-_T~2~_. The type is equivalent to the type application
-`op[T₁, T₂]`. The infix operator _op_ may be an arbitrary identifier,
+An infix type `$T_1$ \mathit{op} $T_2$` consists of an infix
+operator $\mathit{op}$ which gets applied to two type operands $T_1$ and
+$T_2$. The type is equivalent to the type application
+`$\mathit{op}$[$T_1$, $T_2$]`. The infix operator $\mathit{op}$ may be an
+arbitrary identifier,
except for `*`, which is reserved as a postfix modifier
denoting a [repeated parameter type](#repeated-parameters).
@@ -349,11 +351,13 @@ ending in a colon ‘:’ are right-associative; all other
operators are left-associative.
In a sequence of consecutive type infix operations
-$t_0 \, op \, t_1 \, op_2 \, \, op_n \, t_n$,
-all operators $\op_1 , , \op_n$ must have the same
+$t_0 \, \mathit{op} \, t_1 \, \mathit{op_2} \, \ldots \, \mathit{op_n} \, t_n$,
+all operators $\mathit{op}_1 , \ldots , \mathit{op}_n$ must have the same
associativity. If they are all left-associative, the sequence is
-interpreted as `(… (t_0 op_1 t_1) op_2 …) op_n t_n`,
-otherwise it is interpreted as $t_0 op_1 (t_1 op_2 ( … op_n t_n) …)$.
+interpreted as
+$(\ldots (t_0 \mathit{op_1} t_1) \mathit{op_2} \ldots) \mathit{op_n} t_n$,
+otherwise it is interpreted as
+$t_0 \mathit{op_1} (t_1 \mathit{op_2} ( \ldots \mathit{op_n} t_n) \ldots)$.
### Function Types
@@ -371,18 +375,19 @@ An argument type of the form $\Rightarrow T$
represents a [call-by-name parameter](#by-name-parameters) of type $T$.
Function types associate to the right, e.g.
-`S => T => U` is the same as `S => (T => U)`.
+$S \Rightarrow T \Rightarrow U$ is the same as
+$S \Rightarrow (T \Rightarrow U)$.
Function types are shorthands for class types that define `apply`
functions. Specifically, the $n$-ary function type
-`(T1 , , Tn) => U` is a shorthand for the class type
-`Function_n[T1 , … , Tn, U]`. Such class
+$(T_1 , \ldots , T_n) \Rightarrow U$ is a shorthand for the class type
+`Function$_n$[T1 , … , $T_n$, U]`. Such class
types are defined in the Scala library for $n$ between 0 and 9 as follows.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ {.scala}
package scala
-trait Function_n[-T1 , … , -Tn, +R] {
- def apply(x1: T1 , … , xn: Tn): R
+trait Function_n[-T1 , … , -T$_n$, +R] {
+ def apply(x1: T1 , … , x$_n$: T$_n$): R
override def toString = "<function>"
}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -400,63 +405,64 @@ ExistentialDcl ::= ‘type’ TypeDcl
| ‘val’ ValDcl
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-An existential type has the form `T forSome { Q }`
-where _Q_ is a sequence of
+An existential type has the form `$T$ forSome { $Q$ }`
+where $Q$ is a sequence of
[type declarations](#type-declarations-and-type-aliases).
-Let $t_1[\mathit{tps}_1] >: L_1 <: U_1 , \ldots , t_n[\mathit{tps}_n] >: L_n <: U_n$
+Let
+$t_1[\mathit{tps}_1] >: L_1 <: U_1 , \ldots , t_n[\mathit{tps}_n] >: L_n <: U_n$
be the types declared in $Q$ (any of the
-type parameter sections [ _tps~i~_ ] might be missing).
-The scope of each type _t~i~_ includes the type _T_ and the existential clause _Q_.
-The type variables _t~i~_ are said to be _bound_ in the type `T forSome { Q }`.
-Type variables which occur in a type _T_ but which are not bound in _T_ are said
-to be _free_ in _T_.
-
-%%% iainmcgin: to here
-
-A _type instance_ of ~\lstinline@$T$ forSome {$\,Q\,$}@
-is a type $\sigma T$ where $\sigma$ is a substitution over $t_1 \commadots t_n$
-such that, for each $i$, $\sigma L_i \conforms \sigma t_i \conforms \sigma U_i$.
-The set of values denoted by the existential type ~\lstinline@$T$ forSome {$\,Q\,$}@~
+type parameter sections `[ $\mathit{tps}_i$ ]` might be missing).
+The scope of each type $t_i$ includes the type $T$ and the existential clause
+$Q$.
+The type variables $t_i$ are said to be _bound_ in the type
+`$T$ forSome { $Q$ }`.
+Type variables which occur in a type $T$ but which are not bound in $T$ are said
+to be _free_ in $T$.
+
+A _type instance_ of `$T$ forSome { $Q$ }`
+is a type $\sigma T$ where $\sigma$ is a substitution over $t_1 , \ldots , t_n$
+such that, for each $i$, $\sigma L_i <: \sigma t_i <: \sigma U_i$.
+The set of values denoted by the existential type `$T$ forSome {$\,Q\,$}`
is the union of the set of values of all its type instances.
-A _skolemization_ of ~\lstinline@$T$ forSome {$\,Q\,$}@~ is
+A _skolemization_ of `$T$ forSome { $Q$ }` is
a type instance $\sigma T$, where $\sigma$ is the substitution
-$[t'_1/t_1 \commadots t'_n/t_n]$ and each $t'_i$ is a fresh abstract type
+$[t'_1/t_1 , \ldots , t'_n/t_n]$ and each $t'_i$ is a fresh abstract type
with lower bound $\sigma L_i$ and upper bound $\sigma U_i$.
#### Simplification Rules
Existential types obey the following four equivalences:
#. Multiple for-clauses in an existential type can be merged. E.g.,
-~\lstinline@$T$ forSome {$\,Q\,$} forSome {$\,Q'\,$}@~
+`$T$ forSome { $Q$ } forSome { $Q'$ }`
is equivalent to
-~\lstinline@$T$ forSome {$\,Q\,$;$\,Q'\,$}@.
+`$T$ forSome { $Q$ ; $Q'$}`.
#. Unused quantifications can be dropped. E.g.,
-~\lstinline@$T$ forSome {$\,Q\,$;$\,Q'\,$}@~
+`$T$ forSome { $Q$ ; $Q'$}`
where none of the types defined in $Q'$ are referred to by $T$ or $Q$,
is equivalent to
-~\lstinline@$T$ forSome {$\,Q\,$}@.
+`$T$ forSome {$ Q $}`.
#. An empty quantification can be dropped. E.g.,
-~\lstinline@$T$ forSome { }@~ is equivalent to ~\lstinline@$T$@.
-#. An existential type ~\lstinline@$T$ forSome {$\,Q\,$}@~ where $Q$ contains
-a clause ~\lstinline@type $t[\tps] >: L <: U$@ is equivalent
-to the type ~\lstinline@$T'$ forSome {$\,Q\,$}@~ where $T'$ results from $T$ by replacing every
-covariant occurrence (\sref{sec:variances}) of $t$ in $T$ by $U$ and by replacing every
-contravariant occurrence of $t$ in $T$ by $L$.
+`$T$ forSome { }` is equivalent to $T$.
+#. An existential type `$T$ forSome { $Q$ }` where $Q$ contains
+a clause `type $t[\mathit{tps}] >: L <: U$` is equivalent
+to the type `$T'$ forSome { $Q$ }` where $T'$ results from $T$ by replacing
+every [covariant occurrence](#variance-annotations) of $t$ in $T$ by $U$ and by
+replacing every contravariant occurrence of $t$ in $T$ by $L$.
#### Existential Quantification over Values
As a syntactic convenience, the bindings clause
in an existential type may also contain
-value declarations \lstinline@val $x$: $T$@.
-An existential type ~\lstinline@$T$ forSome { $Q$; val $x$: $S\,$;$\,Q'$ }@~
+value declarations `val $x$: $T$`.
+An existential type `$T$ forSome { $Q$; val $x$: $S\,$;$\,Q'$ }`
is treated as a shorthand for the type
-~\lstinline@$T'$ forSome { $Q$; type $t$ <: $S$ with Singleton; $Q'$ }@, where $t$ is a fresh
-type name and $T'$ results from $T$ by replacing every occurrence of
-\lstinline@$x$.type@ with $t$.
+`$T'$ forSome { $Q$; type $t$ <: $S$ with Singleton; $Q'$ }`, where $t$ is a
+fresh type name and $T'$ results from $T$ by replacing every occurrence of
+`$x$.type` with $t$.
#### Placeholder Syntax for Existential Types
@@ -465,26 +471,29 @@ WildcardType ::= ‘_’ TypeBounds
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Scala supports a placeholder syntax for existential types.
-A _wildcard type_ is of the form ~\lstinline@_$\;$>:$\,L\,$<:$\,U$@. Both bound
-clauses may be omitted. If a lower bound clause \lstinline@>:$\,L$@ is missing,
-\lstinline@>:$\,$scala.Nothing@~
-is assumed. If an upper bound clause ~\lstinline@<:$\,U$@ is missing,
-\lstinline@<:$\,$scala.Any@~ is assumed. A wildcard type is a shorthand for an
-existentially quantified type variable, where the existential quantification is implicit.
+A _wildcard type_ is of the form `_$\;$>:$\,L\,$<:$\,U$`. Both bound
+clauses may be omitted. If a lower bound clause `>:$\,L$` is missing,
+`>:$\,$scala.Nothing`
+is assumed. If an upper bound clause `<:$\,U$` is missing,
+`<:$\,$scala.Any` is assumed. A wildcard type is a shorthand for an
+existentially quantified type variable, where the existential quantification is
+implicit.
A wildcard type must appear as type argument of a parameterized type.
-Let $T = p.c[\targs,T,\targs']$ be a parameterized type where $\targs, \targs'$ may be empty and
-$T$ is a wildcard type ~\lstinline@_$\;$>:$\,L\,$<:$\,U$@. Then $T$ is equivalent to the existential
+Let $T = p.c[\mathit{targs},T,\mathit{targs}']$ be a parameterized type where
+$\mathit{targs}, \mathit{targs}'$ may be empty and
+$T$ is a wildcard type `_$\;$>:$\,L\,$<:$\,U$`. Then $T$ is equivalent to the
+existential
type
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-$p.c[\targs,t,\targs']$ forSome { type $t$ >: $L$ <: $U$ }
+$p.c[\mathit{targs},t,\mathit{targs}']$ forSome { type $t$ >: $L$ <: $U$ }
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
where $t$ is some fresh type variable.
-Wildcard types may also appear as parts of infix types
-(\sref{sec:infix-types}), function types (\sref{sec:function-types}),
-or tuple types (\sref{sec:tuple-types}).
+Wildcard types may also appear as parts of [infix types](#infix-types)
+, [function types](#function-types),
+or [tuple types](#tuple-types).
Their expansion is then the expansion in the equivalent parameterized
type.
@@ -548,24 +557,24 @@ report as the internal types of defined identifiers.
### Method Types
-A method type is denoted internally as $(\Ps)U$, where $(\Ps)$ is a
-sequence of parameter names and types $(p_1:T_1 \commadots p_n:T_n)$
+A method type is denoted internally as $(\mathit{Ps})U$, where $(\mathit{Ps})$
+is a sequence of parameter names and types $(p_1:T_1 , \ldots , p_n:T_n)$
for some $n \geq 0$ and $U$ is a (value or method) type. This type
-represents named methods that take arguments named $p_1 \commadots p_n$
-of types $T_1 \commadots T_n$
+represents named methods that take arguments named $p_1 , \ldots , p_n$
+of types $T_1 , \ldots , T_n$
and that return a result of type $U$.
-Method types associate to the right: $(\Ps_1)(\Ps_2)U$ is
-treated as $(\Ps_1)((\Ps_2)U)$.
+Method types associate to the right: $(\mathit{Ps}_1)(\mathit{Ps}_2)U$ is
+treated as $(\mathit{Ps}_1)((\mathit{Ps}_2)U)$.
A special case are types of methods without any parameters. They are
-written here \lstinline@=> T@. Parameterless methods name expressions
+written here `=> T`. Parameterless methods name expressions
that are re-evaluated each time the parameterless method name is
referenced.
Method types do not exist as types of values. If a method name is used
-as a value, its type is implicitly converted to a corresponding
-function type (\sref{sec:impl-conv}).
+as a value, its type is [implicitly converted](#implicit-conversions) to a
+corresponding function type.
(@) The declarations
@@ -585,16 +594,15 @@ function type (\sref{sec:impl-conv}).
### Polymorphic Method Types
-
-A polymorphic method type is denoted internally as ~\lstinline@[$\tps\,$]$T$@~ where
-\lstinline@[$\tps\,$]@ is a type parameter section
-~\lstinline@[$a_1$ >: $L_1$ <: $U_1 \commadots a_n$ >: $L_n$ <: $U_n$]@~
+A polymorphic method type is denoted internally as `[$\mathit{tps}\,$]$T$` where
+`[$\mathit{tps}\,$]` is a type parameter section
+`[$a_1$ >: $L_1$ <: $U_1 , \ldots , a_n$ >: $L_n$ <: $U_n$]`
for some $n \geq 0$ and $T$ is a
(value or method) type. This type represents named methods that
-take type arguments ~\lstinline@$S_1 \commadots S_n$@~ which
-conform (\sref{sec:param-types}) to the lower bounds
-~\lstinline@$L_1 \commadots L_n$@~ and the upper bounds
-~\lstinline@$U_1 \commadots U_n$@~ and that yield results of type $T$.
+take type arguments `$S_1 , \ldots , S_n$` which
+[conform](#parameterized-types) to the lower bounds
+`$L_1 , \ldots , L_n$` and the upper bounds
+`$U_1 , \ldots , U_n$` and that yield results of type $T$.
(@) The declarations
@@ -613,7 +621,11 @@ conform (\sref{sec:param-types}) to the lower bounds
### Type Constructors
A type constructor is represented internally much like a polymorphic method type.
-~\lstinline@[$\pm$ $a_1$ >: $L_1$ <: $U_1 \commadots \pm a_n$ >: $L_n$ <: $U_n$] $T$@~ represents a type that is expected by a type constructor parameter (\sref{sec:type-params}) or an abstract type constructor binding (\sref{sec:typedcl}) with the corresponding type parameter clause.
+`[$\pm$ $a_1$ >: $L_1$ <: $U_1 , \ldots , \pm a_n$ >: $L_n$ <: $U_n$] $T$`
+represents a type that is expected by a
+[type constructor parameter](#type-params) or an
+[abstract type constructor binding](#type-declarations-and-type-aliases) with
+the corresponding type parameter clause.
(@) Consider this fragment of the `Iterable[+X]`{.scala} class:
@@ -644,300 +656,283 @@ These notions are defined mutually recursively as follows.
#. The set of _base types_ of a type is a set of class types,
given as follows.
- - The base types of a class type $C$ with parents $T_1 \commadots T_n$ are
+ - The base types of a class type $C$ with parents $T_1 , \ldots , T_n$ are
$C$ itself, as well as the base types of the compound type
- ~\lstinline@$T_1$ with $\ldots$ with $T_n$ {$R\,$}@.
+ `$T_1$ with with $T_n$ { $R$ }`.
- The base types of an aliased type are the base types of its alias.
- The base types of an abstract type are the base types of its upper bound.
- The base types of a parameterized type
- ~\lstinline@$C$[$T_1 \commadots T_n$]@~ are the base types
+ `$C$[$T_1 , \ldots , T_n$]` are the base types
of type $C$, where every occurrence of a type parameter $a_i$
of $C$ has been replaced by the corresponding parameter type $T_i$.
- - The base types of a singleton type \lstinline@$p$.type@ are the base types of
+ - The base types of a singleton type `$p$.type` are the base types of
the type of $p$.
- The base types of a compound type
- ~\lstinline@$T_1$ with $\ldots$ with $T_n$ {$R\,$}@~
+ `$T_1$ with $\ldots$ with $T_n$ { $R$ }`
are the _reduced union_ of the base
classes of all $T_i$'s. This means:
- Let the multi-set $\SS$ be the multi-set-union of the
+ Let the multi-set $\mathscr{S}$ be the multi-set-union of the
base types of all $T_i$'s.
- If $\SS$ contains several type instances of the same class, say
- ~\lstinline@$S^i$#$C$[$T^i_1 \commadots T^i_n$]@~ $(i \in I)$, then
+ If $\mathscr{S}$ contains several type instances of the same class, say
+ `$S^i$#$C$[$T^i_1 , \ldots , T^i_n$]` $(i \in I)$, then
all those instances
are replaced by one of them which conforms to all
- others. It is an error if no such instance exists. It follows that the reduced union, if it exists,
- produces a set of class types, where different types are instances of different classes.
- - The base types of a type selection \lstinline@$S$#$T$@ are
+ others. It is an error if no such instance exists. It follows that the
+ reduced union, if it exists,
+ produces a set of class types, where different types are instances of
+ different classes.
+ - The base types of a type selection `$S$#$T$` are
determined as follows. If $T$ is an alias or abstract type, the
previous clauses apply. Otherwise, $T$ must be a (possibly
parameterized) class type, which is defined in some class $B$. Then
- the base types of \lstinline@$S$#$T$@ are the base types of $T$
+ the base types of `$S$#$T$` are the base types of $T$
in $B$ seen from the prefix type $S$.
- - The base types of an existential type \lstinline@$T$ forSome {$\,Q\,$}@ are
- all types \lstinline@$S$ forSome {$\,Q\,$}@ where $S$ is a base type of $T$.
-
-2. The notion of a type $T$
-{\em in class $C$ seen from some prefix type
-$S\,$} makes sense only if the prefix type $S$
-has a type instance of class $C$ as a base type, say
-~\lstinline@$S'$#$C$[$T_1 \commadots T_n$]@. Then we define as follows.
-\begin{itemize}
- \item
- If \lstinline@$S$ = $\epsilon$.type@, then $T$ in $C$ seen from $S$ is $T$ itself.
- \item
- Otherwise, if $S$ is an existential type ~\lstinline@$S'$ forSome {$\,Q\,$}@, and
- $T$ in $C$ seen from $S'$ is $T'$,
- then $T$ in $C$ seen from $S$ is ~\lstinline@$T'$ forSome {$\,Q\,$}@.
- \item
- Otherwise, if $T$ is the $i$'th type parameter of some class $D$, then
- \begin{itemize}
- \item
- If $S$ has a base type ~\lstinline@$D$[$U_1 \commadots U_n$]@, for some type parameters
- ~\lstinline@[$U_1 \commadots U_n$]@, then $T$ in $C$ seen from $S$ is $U_i$.
- \item
- Otherwise, if $C$ is defined in a class $C'$, then
- $T$ in $C$ seen from $S$ is the same as $T$ in $C'$ seen from $S'$.
- \item
- Otherwise, if $C$ is not defined in another class, then
- $T$ in $C$ seen from $S$ is $T$ itself.
- \end{itemize}
-\item
- Otherwise,
- if $T$ is the singleton type \lstinline@$D$.this.type@ for some class $D$
- then
- \begin{itemize}
- \item
- If $D$ is a subclass of $C$ and
- $S$ has a type instance of class $D$ among its base types,
- then $T$ in $C$ seen from $S$ is $S$.
- \item
- Otherwise, if $C$ is defined in a class $C'$, then
- $T$ in $C$ seen from $S$ is the same as $T$ in $C'$ seen from $S'$.
- \item
- Otherwise, if $C$ is not defined in another class, then
- $T$ in $C$ seen from $S$ is $T$ itself.
- \end{itemize}
-\item
- If $T$ is some other type, then the described mapping is performed
- to all its type components.
-\end{itemize}
-
-If $T$ is a possibly parameterized class type, where $T$'s class
-is defined in some other class $D$, and $S$ is some prefix type,
-then we use ``$T$ seen from $S$'' as a shorthand for
-``$T$ in $D$ seen from $S$''.
-
-3. The _member bindings_ of a type $T$ are (1) all bindings $d$ such that
-there exists a type instance of some class $C$ among the base types of $T$
-and there exists a definition or declaration $d'$ in $C$
-such that $d$ results from $d'$ by replacing every
-type $T'$ in $d'$ by $T'$ in $C$ seen from $T$, and (2) all bindings
-of the type's refinement (\sref{sec:refinements}), if it has one.
-
-The _definition_ of a type projection \lstinline@$S$#$t$@ is the member
-binding $d_t$ of the type $t$ in $S$. In that case, we also say
-that \lstinline@$S$#$t$@ _is defined by_ $d_t$.
-share a to
+ - The base types of an existential type `$T$ forSome { $Q$ }` are
+ all types `$S$ forSome { $Q$ }` where $S$ is a base type of $T$.
+
+#. The notion of a type $T$ _in class $C$ seen from some prefix type $S$_
+ makes sense only if the prefix type $S$
+ has a type instance of class $C$ as a base type, say
+ `$S'$#$C$[$T_1 , \ldots , T_n$]`. Then we define as follows.
+ - If `$S$ = $\epsilon$.type`, then $T$ in $C$ seen from $S$ is
+ $T$ itself.
+ - Otherwise, if $S$ is an existential type `$S'$ forSome { $Q$ }`, and
+ $T$ in $C$ seen from $S'$ is $T'$,
+ then $T$ in $C$ seen from $S$ is `$T'$ forSome {$\,Q\,$}`.
+ - Otherwise, if $T$ is the $i$'th type parameter of some class $D$, then
+ - If $S$ has a base type `$D$[$U_1 , \ldots , U_n$]`, for some type
+ parameters `[$U_1 , \ldots , U_n$]`, then $T$ in $C$ seen from $S$
+ is $U_i$.
+ - Otherwise, if $C$ is defined in a class $C'$, then
+ $T$ in $C$ seen from $S$ is the same as $T$ in $C'$ seen from $S'$.
+ - Otherwise, if $C$ is not defined in another class, then
+ $T$ in $C$ seen from $S$ is $T$ itself.
+ - Otherwise, if $T$ is the singleton type `$D$.this.type` for some class $D$
+ then
+ - If $D$ is a subclass of $C$ and $S$ has a type instance of class $D$
+ among its base types, then $T$ in $C$ seen from $S$ is $S$.
+ - Otherwise, if $C$ is defined in a class $C'$, then
+ $T$ in $C$ seen from $S$ is the same as $T$ in $C'$ seen from $S'$.
+ - Otherwise, if $C$ is not defined in another class, then
+ $T$ in $C$ seen from $S$ is $T$ itself.
+ - If $T$ is some other type, then the described mapping is performed
+ to all its type components.
+
+ If $T$ is a possibly parameterized class type, where $T$'s class
+ is defined in some other class $D$, and $S$ is some prefix type,
+ then we use ``$T$ seen from $S$'' as a shorthand for
+ ``$T$ in $D$ seen from $S$''.
+
+#. The _member bindings_ of a type $T$ are (1) all bindings $d$ such that
+ there exists a type instance of some class $C$ among the base types of $T$
+ and there exists a definition or declaration $d'$ in $C$
+ such that $d$ results from $d'$ by replacing every
+ type $T'$ in $d'$ by $T'$ in $C$ seen from $T$, and (2) all bindings
+ of the type's [refinement](#compound-types), if it has one.
+
+ The _definition_ of a type projection `$S$#$t$` is the member
+ binding $d_t$ of the type $t$ in $S$. In that case, we also say
+ that ~$S$#$t$` _is defined by_ $d_t$.
+ share a to
Relations between types
-----------------------
We define two relations between types.
-\begin{quote}\begin{tabular}{l@{\gap}l@{\gap}l}
-\em Type equivalence & $T \equiv U$ & $T$ and $U$ are interchangeable
-in all contexts.
-\\
-\em Conformance & $T \conforms U$ & Type $T$ conforms to type $U$.
-\end{tabular}\end{quote}
+
+----------------- ---------------- -------------------------------------------------
+Type equivalence $T \equiv U$ $T$ and $U$ are interchangeable in all contexts.
+Conformance $T <: U$ Type $T$ conforms to type $U$.
+----------------- ---------------- -------------------------------------------------
+
### Type Equivalence
-\label{sec:type-equiv}
-
-Equivalence $(\equiv)$ between types is the smallest congruence\footnote{ A
-congruence is an equivalence relation which is closed under formation
-of contexts} such that the following holds:
-\begin{itemize}
-\item
-If $t$ is defined by a type alias ~\lstinline@type $t$ = $T$@, then $t$ is
-equivalent to $T$.
-\item
-If a path $p$ has a singleton type ~\lstinline@$q$.type@, then
-~\lstinline@$p$.type $\equiv q$.type@.
-\item
-If $O$ is defined by an object definition, and $p$ is a path
-consisting only of package or object selectors and ending in $O$, then
-~\lstinline@$O$.this.type $\equiv p$.type@.
-\item
-Two compound types (\sref{sec:compound-types}) are equivalent if the sequences of their component
-are pairwise equivalent, and occur in the same order, and their
-refinements are equivalent. Two refinements are equivalent if they
-bind the same names and the modifiers, types and bounds of every
-declared entity are equivalent in both refinements.
-\item
-Two method types (\sref{sec:method-types}) are equivalent if they have equivalent result types,
-both have the same number of parameters, and corresponding parameters
-have equivalent types. Note that the names of parameters do not
-matter for method type equivalence.
-\item
-Two polymorphic method types (\sref{sec:poly-types}) are equivalent if they have the same number of
-type parameters, and, after renaming one set of type parameters by
-another, the result types as well as lower and upper bounds of
-corresponding type parameters are equivalent.
-\item
-Two existential types (\sref{sec:existential-types})
-are equivalent if they have the same number of
-quantifiers, and, after renaming one list of type quantifiers by
-another, the quantified types as well as lower and upper bounds of
-corresponding quantifiers are equivalent.
-\item %@M
-Two type constructors (\sref{sec:higherkinded-types}) are equivalent if they have the
-same number of type parameters, and, after renaming one list of type parameters by
-another, the result types as well as variances, lower and upper bounds of
-corresponding type parameters are equivalent.
-\end{itemize}
+
+Equivalence $(\equiv)$ between types is the smallest congruence [^3] such that
+the following holds:
+
+- If $t$ is defined by a type alias `type $t$ = $T$`, then $t$ is
+ equivalent to $T$.
+- If a path $p$ has a singleton type `$q$.type`, then
+ `$p$.type $\equiv q$.type`.
+- If $O$ is defined by an object definition, and $p$ is a path
+ consisting only of package or object selectors and ending in $O$, then
+ `$O$.this.type $\equiv p$.type`.
+- Two [compound types](#compound-types) are equivalent if the sequences
+ of their component are pairwise equivalent, and occur in the same order, and
+ their refinements are equivalent. Two refinements are equivalent if they
+ bind the same names and the modifiers, types and bounds of every
+ declared entity are equivalent in both refinements.
+- Two [method types](#method-types) are equivalent if they have
+ equivalent result types,
+ both have the same number of parameters, and corresponding parameters
+ have equivalent types. Note that the names of parameters do not
+ matter for method type equivalence.
+- Two [polymorphic method types](#polymorphic-method-types) are equivalent if
+ they have the same number of type parameters, and, after renaming one set of
+ type parameters by another, the result types as well as lower and upper bounds
+ of corresponding type parameters are equivalent.
+- Two [existential types](#existential-types)
+ are equivalent if they have the same number of
+ quantifiers, and, after renaming one list of type quantifiers by
+ another, the quantified types as well as lower and upper bounds of
+ corresponding quantifiers are equivalent.
+- Two [type constructors](#type-constructors) are equivalent if they have the
+ same number of type parameters, and, after renaming one list of type
+ parameters by another, the result types as well as variances, lower and upper
+ bounds of corresponding type parameters are equivalent.
+
+
+[^3]: A congruence is an equivalence relation which is closed under formation
+of contexts
+
### Conformance
-\label{sec:conformance}
-The conformance relation $(\conforms)$ is the smallest
+The conformance relation $(<:)$ is the smallest
transitive relation that satisfies the following conditions.
-\begin{itemize}
-\item Conformance includes equivalence. If $T \equiv U$ then $T \conforms U$.
-\item For every value type $T$,
- $\mbox{\code{scala.Nothing}} \conforms T \conforms \mbox{\code{scala.Any}}$.
-\item For every type constructor $T$ (with any number of type parameters),
- $\mbox{\code{scala.Nothing}} \conforms T \conforms \mbox{\code{scala.Any}}$. %@M
+
+- Conformance includes equivalence. If $T \equiv U$ then $T <: U$.
+- For every value type $T$, `scala.Nothing <: $T$ <: scala.Any`.
+- For every type constructor $T$ (with any number of type parameters),
+ `scala.Nothing <: $T$ <: scala.Any`.
-\item For every class type $T$ such that $T \conforms
- \mbox{\code{scala.AnyRef}}$ and not $T \conforms \mbox{\code{scala.NotNull}}$
- one has $\mbox{\code{scala.Null}} \conforms T$.
-\item A type variable or abstract type $t$ conforms to its upper bound and
- its lower bound conforms to $t$.
-\item A class type or parameterized type conforms to any of its
- base-types.
-\item A singleton type \lstinline@$p$.type@ conforms to the type of
- the path $p$.
-\item A singleton type \lstinline@$p$.type@ conforms to the type $\mbox{\code{scala.Singleton}}$.
-\item A type projection \lstinline@$T$#$t$@ conforms to \lstinline@$U$#$t$@ if
- $T$ conforms to $U$.
-\item A parameterized type ~\lstinline@$T$[$T_1 \commadots T_n$]@~ conforms to
- ~\lstinline@$T$[$U_1 \commadots U_n$]@~ if
- the following three conditions hold for $i = 1 \commadots n$.
- \begin{itemize}
- \item
- If the $i$'th type parameter of $T$ is declared covariant, then $T_i \conforms U_i$.
- \item
- If the $i$'th type parameter of $T$ is declared contravariant, then $U_i \conforms T_i$.
- \item
- If the $i$'th type parameter of $T$ is declared neither covariant
- nor contravariant, then $U_i \equiv T_i$.
- \end{itemize}
-\item A compound type ~\lstinline@$T_1$ with $\ldots$ with $T_n$ {$R\,$}@~ conforms to
- each of its component types $T_i$.
-\item If $T \conforms U_i$ for $i = 1 \commadots n$ and for every
- binding $d$ of a type or value $x$ in $R$ there exists a member
- binding of $x$ in $T$ which subsumes $d$, then $T$ conforms to the
- compound type ~\lstinline@$U_1$ with $\ldots$ with $U_n$ {$R\,$}@.
-\item The existential type ~\lstinline@$T$ forSome {$\,Q\,$}@ conforms to
- $U$ if its skolemization (\sref{sec:existential-types})
- conforms to $U$.
-\item The type $T$ conforms to the existential type ~\lstinline@$U$ forSome {$\,Q\,$}@
- if $T$ conforms to one of the type instances (\sref{sec:existential-types})
- of ~\lstinline@$U$ forSome {$\,Q\,$}@.
-\item If
- $T_i \equiv T'_i$ for $i = 1 \commadots n$ and $U$ conforms to $U'$
- then the method type $(p_1:T_1 \commadots p_n:T_n) U$ conforms to
- $(p'_1:T'_1 \commadots p'_n:T'_n) U'$.
-\item The polymorphic type
-$[a_1 >: L_1 <: U_1 \commadots a_n >: L_n <: U_n] T$ conforms to the polymorphic type
-$[a_1 >: L'_1 <: U'_1 \commadots a_n >: L'_n <: U'_n] T'$ if, assuming
-$L'_1 \conforms a_1 \conforms U'_1 \commadots L'_n \conforms a_n \conforms U'_n$
-one has $T \conforms T'$ and $L_i \conforms L'_i$ and $U'_i \conforms U_i$
-for $i = 1 \commadots n$.
-%@M
-\item Type constructors $T$ and $T'$ follow a similar discipline. We characterize $T$ and $T'$ by their type parameter clauses
-$[a_1 \commadots a_n]$ and
-$[a'_1 \commadots a'_n ]$, where an $a_i$ or $a'_i$ may include a variance annotation, a higher-order type parameter clause, and bounds. Then, $T$ conforms to $T'$ if any list $[t_1 \commadots t_n]$ -- with declared variances, bounds and higher-order type parameter clauses -- of valid type arguments for $T'$ is also a valid list of type arguments for $T$ and $T[t_1 \commadots t_n] \conforms T'[t_1 \commadots t_n]$. Note that this entails that:
- \begin{itemize}
- \item
- The bounds on $a_i$ must be weaker than the corresponding bounds declared for $a'_i$.
- \item
- The variance of $a_i$ must match the variance of $a'_i$, where covariance matches covariance, contravariance matches contravariance and any variance matches invariance.
- \item
- Recursively, these restrictions apply to the corresponding higher-order type parameter clauses of $a_i$ and $a'_i$.
- \end{itemize}
-
-\end{itemize}
+- For every class type $T$ such that `$T$ <: scala.AnyRef` and not
+ `$T$ <: scala.NotNull` one has `scala.Null <: $T$`.
+- A type variable or abstract type $t$ conforms to its upper bound and
+ its lower bound conforms to $t$.
+- A class type or parameterized type conforms to any of its base-types.
+- A singleton type `$p$.type` conforms to the type of the path $p$.
+- A singleton type `$p$.type` conforms to the type `scala.Singleton`.
+- A type projection `$T$#$t$` conforms to `$U$#$t$` if $T$ conforms to $U$.
+- A parameterized type `$T$[$T_1$ , … , $T_n$]` conforms to
+ `$T$[$U_1$ , … , $U_n$]` if
+ the following three conditions hold for $i \in \{ 1 , \ldots , n \}$:
+ #. If the $i$'th type parameter of $T$ is declared covariant, then
+ $T_i <: U_i$.
+ #. If the $i$'th type parameter of $T$ is declared contravariant, then
+ $U_i <: T_i$.
+ #. If the $i$'th type parameter of $T$ is declared neither covariant
+ nor contravariant, then $U_i \equiv T_i$.
+- A compound type `$T_1$ with $\ldots$ with $T_n$ {$R\,$}` conforms to
+ each of its component types $T_i$.
+- If $T <: U_i$ for $i \in \{ 1 , \ldots , n \}$ and for every
+ binding $d$ of a type or value $x$ in $R$ there exists a member
+ binding of $x$ in $T$ which subsumes $d$, then $T$ conforms to the
+ compound type `$U_1$ with $\ldots$ with $U_n$ {$R\,$}`.
+- The existential type `$T$ forSome {$\,Q\,$}` conforms to
+ $U$ if its [skolemization](#existential-types)
+ conforms to $U$.
+- The type $T$ conforms to the existential type `$U$ forSome {$\,Q\,$}`
+ if $T$ conforms to one of the [type instances](#existential-types)
+ of `$U$ forSome {$\,Q\,$}`.
+- If
+ $T_i \equiv T'_i$ for $i \in \{ 1 , \ldots , n\}$ and $U$ conforms to $U'$
+ then the method type $(p_1:T_1 , \ldots , p_n:T_n) U$ conforms to
+ $(p'_1:T'_1 , \ldots , p'_n:T'_n) U'$.
+- The polymorphic type
+ $[a_1 >: L_1 <: U_1 , \ldots , a_n >: L_n <: U_n] T$ conforms to the
+ polymorphic type
+ $[a_1 >: L'_1 <: U'_1 , \ldots , a_n >: L'_n <: U'_n] T'$ if, assuming
+ $L'_1 <: a_1 <: U'_1 , \ldots , L'_n <: a_n <: U'_n$
+ one has $T <: T'$ and $L_i <: L'_i$ and $U'_i <: U_i$
+ for $i \in \{ 1 , \ldots , n \}$.
+- Type constructors $T$ and $T'$ follow a similar discipline. We characterize
+ $T$ and $T'$ by their type parameter clauses
+ $[a_1 , \ldots , a_n]$ and
+ $[a'_1 , \ldots , a'_n ]$, where an $a_i$ or $a'_i$ may include a variance
+ annotation, a higher-order type parameter clause, and bounds. Then, $T$
+ conforms to $T'$ if any list $[t_1 , \ldots , t_n]$ -- with declared
+ variances, bounds and higher-order type parameter clauses -- of valid type
+ arguments for $T'$ is also a valid list of type arguments for $T$ and
+ $T[t_1 , \ldots , t_n] <: T'[t_1 , \ldots , t_n]$. Note that this entails
+ that:
+ - The bounds on $a_i$ must be weaker than the corresponding bounds declared
+ for $a'_i$.
+ - The variance of $a_i$ must match the variance of $a'_i$, where covariance
+ matches covariance, contravariance matches contravariance and any variance
+ matches invariance.
+ - Recursively, these restrictions apply to the corresponding higher-order
+ type parameter clauses of $a_i$ and $a'_i$.
+
A declaration or definition in some compound type of class type $C$
-_subsumes_ another
-declaration of the same name in some compound type or class type $C'$, if one of the following holds.
-\begin{itemize}
-\item
-A value declaration or definition that defines a name $x$ with type $T$ subsumes
-a value or method declaration that defines $x$ with type $T'$, provided $T \conforms T'$.
-\item
-A method declaration or definition that defines a name $x$ with type $T$ subsumes
-a method declaration that defines $x$ with type $T'$, provided $T \conforms T'$.
-\item
-A type alias
-$\TYPE;t[T_1 \commadots T_n]=T$ subsumes a type alias $\TYPE;t[T_1 \commadots T_n]=T'$ if %@M
-$T \equiv T'$.
-\item
-A type declaration ~\lstinline@type $t$[$T_1 \commadots T_n$] >: $L$ <: $U$@~ subsumes %@M
-a type declaration ~\lstinline@type $t$[$T_1 \commadots T_n$] >: $L'$ <: $U'$@~ if $L' \conforms L$ and %@M
-$U \conforms U'$.
-\item
-A type or class definition that binds a type name $t$ subsumes an abstract
-type declaration ~\lstinline@type t[$T_1 \commadots T_n$] >: L <: U@~ if %@M
-$L \conforms t \conforms U$.
-\end{itemize}
-
-The $(\conforms)$ relation forms pre-order between types,
-i.e.\ it is transitive and reflexive. _least upper bounds_ and _greatest lower bounds_ of a set of types
+_subsumes_ another declaration of the same name in some compound type or class
+type $C'$, if one of the following holds.
+
+- A value declaration or definition that defines a name $x$ with type $T$
+ subsumes
+ a value or method declaration that defines $x$ with type $T'$, provided
+ $T <: T'$.
+- A method declaration or definition that defines a name $x$ with type $T$
+ subsumes a method declaration that defines $x$ with type $T'$, provided
+ $T <: T'$.
+- A type alias
+ `type $t$[$T_1$ , … , $T_n$] = $T$` subsumes a type alias
+ `type $t$[$T_1$ , … , $T_n$] = $T'$` if $T \equiv T'$.
+- A type declaration `type $t$[$T_1$ , … , $T_n$] >: $L$ <: $U$` subsumes
+ a type declaration `type $t$[$T_1$ , … , $T_n$] >: $L'$ <: $U'$` if
+ $L' <: L$ and $U <: U'$.
+- A type or class definition that binds a type name $t$ subsumes an abstract
+ type declaration `type t[$T_1$ , … , $T_n$] >: L <: U` if
+ $L <: t <: U$.
+
+
+The $(<:)$ relation forms pre-order between types,
+i.e.\ it is transitive and reflexive. _least upper bounds_ and
+_greatest lower bounds_ of a set of types
are understood to be relative to that order.
-\paragraph{Note} The least upper bound or greatest lower bound
-of a set of types does not always exist. For instance, consider
-the class definitions
-\begin{lstlisting}
+
+> **Note**: The least upper bound or greatest lower bound
+> of a set of types does not always exist. For instance, consider
+> the class definitions
+
+~~~~~~~~~~~~~~~~~~~~~ {.scala}
class A[+T] {}
-class B extends A[B]
-class C extends A[C]
-\end{lstlisting}
-Then the types ~\lstinline@A[Any], A[A[Any]], A[A[A[Any]]], ...@~ form
-a descending sequence of upper bounds for \code{B} and \code{C}. The
-least upper bound would be the infinite limit of that sequence, which
-does not exist as a Scala type. Since cases like this are in general
-impossible to detect, a Scala compiler is free to reject a term
-which has a type specified as a least upper or greatest lower bound,
-and that bound would be more complex than some compiler-set
-limit\footnote{The current Scala compiler limits the nesting level
-of parameterization in such bounds to be at most two deeper than the maximum
-nesting level of the operand types}.
-
-The least upper bound or greatest lower bound might also not be
-unique. For instance \code{A with B} and \code{B with A} are both
-greatest lower of \code{A} and \code{B}. If there are several
-least upper bounds or greatest lower bounds, the Scala compiler is
-free to pick any one of them.
+class B extends A[B]
+class C extends A[C]
+~~~~~~~~~~~~~~~~~~~~~
+
+> Then the types `A[Any], A[A[Any]], A[A[A[Any]]], ...` form
+> a descending sequence of upper bounds for `B` and `C`. The
+> least upper bound would be the infinite limit of that sequence, which
+> does not exist as a Scala type. Since cases like this are in general
+> impossible to detect, a Scala compiler is free to reject a term
+> which has a type specified as a least upper or greatest lower bound,
+> and that bound would be more complex than some compiler-set
+> limit [^4].
+>
+> The least upper bound or greatest lower bound might also not be
+> unique. For instance `A with B` and `B with A` are both
+> greatest lower of `A` and `B`. If there are several
+> least upper bounds or greatest lower bounds, the Scala compiler is
+> free to pick any one of them.
+
+
+[^4]: The current Scala compiler limits the nesting level
+ of parameterization in such bounds to be at most two deeper than the
+ maximum nesting level of the operand types
+
+
### Weak Conformance
-In some situations Scala uses a more genral conformance relation. A
+In some situations Scala uses a more general conformance relation. A
type $S$ _weakly conforms_
-to a type $T$, written $S \conforms_w
-T$, if $S \conforms T$ or both $S$ and $T$ are primitive number types
+to a type $T$, written $S <:_w
+T$, if $S <: T$ or both $S$ and $T$ are primitive number types
and $S$ precedes $T$ in the following ordering.
-\begin{lstlisting}
-Byte $\conforms_w$ Short
-Short $\conforms_w$ Int
-Char $\conforms_w$ Int
-Int $\conforms_w$ Long
-Long $\conforms_w$ Float
-Float $\conforms_w$ Double
-\end{lstlisting}
+
+~~~~~~~~~~~~~~~~~~~~
+Byte $<:_w$ Short
+Short $<:_w$ Int
+Char $<:_w$ Int
+Int $<:_w$ Long
+Long $<:_w$ Float
+Float $<:_w$ Double
+~~~~~~~~~~~~~~~~~~~~
A _weak least upper bound_ is a least upper bound with respect to
weak conformance.
@@ -946,23 +941,21 @@ weak conformance.
Volatile Types
--------------
-
-
-Type volatility approximates the possibility that a type parameter or abstract type instance
-of a type does not have any non-null values. As explained in
-(\sref{sec:paths}), a value member of a volatile type cannot appear in
-a path.
+Type volatility approximates the possibility that a type parameter or abstract
+type instance
+of a type does not have any non-null values. A value member of a volatile type
+cannot appear in a [path](#paths).
A type is _volatile_ if it falls into one of four categories:
-A compound type ~\lstinline@$T_1$ with $\ldots$ with $T_n$ {$R\,$}@~
+A compound type `$T_1$ with with $T_n$ {$R\,$}`
is volatile if one of the following two conditions hold.
-#. One of $T_2 \commadots T_n$ is a type parameter or abstract type, or
+#. One of $T_2 , \ldots , T_n$ is a type parameter or abstract type, or
#. $T_1$ is an abstract type and and either the refinement $R$
or a type $T_j$ for $j > 1$ contributes an abstract member
to the compound type, or
-#. one of $T_1 \commadots T_n$ is a singleton type.
+#. one of $T_1 , \ldots , T_n$ is a singleton type.
Here, a type $S$ _contributes an abstract member_ to a type $T$ if
@@ -971,13 +964,13 @@ A refinement $R$ contributes an abstract member to a type $T$ if $R$
contains an abstract declaration which is also a member of $T$.
A type designator is volatile if it is an alias of a volatile type, or
-if it designates a type parameter or abstract type that has a volatile type as its
-upper bound.
+if it designates a type parameter or abstract type that has a volatile type as
+its upper bound.
-A singleton type \lstinline@$p$.type@ is volatile, if the underlying
+A singleton type `$p$.type` is volatile, if the underlying
type of path $p$ is volatile.
-An existential type ~\lstinline@$T$ forSome {$\,Q\,$}@~ is volatile if
+An existential type `$T$ forSome {$\,Q\,$}` is volatile if
$T$ is volatile.
@@ -989,25 +982,25 @@ _Type erasure_ is a mapping from (possibly generic) types to
non-generic types. We write $|T|$ for the erasure of type $T$.
The erasure mapping is defined as follows.
-- The erasure of an alias type is the erasure of its right-hand side. %@M
+- The erasure of an alias type is the erasure of its right-hand side.
- The erasure of an abstract type is the erasure of its upper bound.
-- The erasure of the parameterized type \lstinline@scala.Array$[T_1]$@ is
- \lstinline@scala.Array$[|T_1|]$@.
-- The erasure of every other parameterized type $T[T_1 \commadots T_n]$ is $|T|$.
-- The erasure of a singleton type \lstinline@$p$.type@ is the
+- The erasure of the parameterized type `scala.Array$[T_1]$` is
+ `scala.Array$[|T_1|]$`.
+- The erasure of every other parameterized type $T[T_1 , \ldots , T_n]$ is $|T|$.
+- The erasure of a singleton type `$p$.type` is the
erasure of the type of $p$.
-- The erasure of a type projection \lstinline@$T$#$x$@ is \lstinline@|$T$|#$x$@.
+- The erasure of a type projection `$T$#$x$` is `|$T$|#$x$`.
- The erasure of a compound type
- ~\lstinline@$T_1$ with $\ldots$ with $T_n$ {$R\,$}@ is the erasure of the intersection dominator of
- $T_1 \commadots T_n$.
-- The erasure of an existential type ~\lstinline@$T$ forSome {$\,Q\,$}@
- is $|T|$.
-
-The _intersection dominator_ of a list of types $T_1 \commadots
-T_n$ is computed as follows.
-Let $T_{i_1} \commadots T_{i_m}$ be the subsequence of types $T_i$
+ `$T_1$ with $\ldots$ with $T_n$ {$R\,$}` is the erasure of the intersection
+ dominator of $T_1 , \ldots , T_n$.
+- The erasure of an existential type `$T$ forSome {$\,Q\,$}` is $|T|$.
+
+The _intersection dominator_ of a list of types $T_1 , \ldots , T_n$ is computed
+as follows.
+Let $T_{i_1} , \ldots , T_{i_m}$ be the subsequence of types $T_i$
which are not supertypes of some other type $T_j$.
-If this subsequence contains a type designator $T_c$ that refers to a class which is not a trait,
+If this subsequence contains a type designator $T_c$ that refers to a class
+which is not a trait,
the intersection dominator is $T_c$. Otherwise, the intersection
dominator is the first element of the subsequence, $T_{i_1}$.
View
6 16-references.md
@@ -0,0 +1,6 @@
+References
+==========
+
+<!-- this is deliberately empty, and must be at the very end of the
+ document as pandoc will inject all citation information here.
+-->
View
17 README.md
@@ -62,6 +62,14 @@ code fragment.
### Macro replacements:
+- While MathJAX just support LaTeX style command definition, it is recommended
+ to not use this as it will likely cause issues with preparing the document
+ for PDF or ebook distribution.
+- `\SS` (which I could not find defined within the latex source) seems to be
+ closest to `\mathscr{S}`
+- `\TYPE` is equivalent to `\boldsymbol{type}'
+- As MathJAX has no support for slanted font (latex command \sl), so in all
+ instances this should be replaced with \mathit{}
- The macro \U{ABCD} used for unicode character references can be
replaced with \\uABCD.
- The macro \URange{ABCD}{DCBA} used for unicode character ranges can be
@@ -92,4 +100,11 @@ syntax
#. first entry
#. ...
- #. last entry
+ #. last entry
+
+
+Finding rendering errors
+------------------------
+
+- MathJAX errors will appear within the rendered DOM as span elements with
+ class `mtext` and style attribute `color: red` applied.
View
5 build.sh
@@ -4,7 +4,8 @@ cat 01-title.md \
02-preface.md \
03-lexical-syntax.md \
04-identifiers-names-and-scopes.md \
- 05-types.md > build/ScalaReference.md
+ 05-types.md \
+ 16-references.md > build/ScalaReference.md
# 06-basic-declarations-and-definitions.md \
# 07-classes-and-objects.md \
# 08-expressions.md \
@@ -24,7 +25,7 @@ pandoc -f markdown \
--number-sections \
--bibliography=Scala.bib \
--template=resources/scala-ref-template.html5 \
- --mathjax \
+ --mathjax='http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML' \
-o build/ScalaReference.html \
build/ScalaReference.md
View
20 resources/ScalaReference.js
@@ -0,0 +1,20 @@
+$(function() {
+
+ var popoutTOC = $('<div>');
+ popoutTOC.attr('id', 'popoutTOC');
+
+ var popoutTOChead = $('<span class="head">Jump to...</span>');
+ popoutTOChead.appendTo(popoutTOC);
+
+ var content = $('<div class="links">');
+ $('#TOC > *').clone().appendTo(content);
+ content.appendTo(popoutTOC);
+ var enter = function() { content.css('display', 'block') };
+ var exit = function() { content.css('display', 'none') };
+
+ popoutTOC.hover(enter, exit);
+
+ // disabled for now, until better styled
+ // popoutTOC.appendTo($('body'));
+
+})
View
2 resources/scala-ref-template.html5
@@ -26,6 +26,8 @@ $endif$
$for(css)$
<link rel="stylesheet" href="$css$">
$endfor$
+ <script type="text/javascript" src="https://ajax.googleapis.com/ajax/libs/jquery/1.8.2/jquery.min.js"></script>
+ <script type="text/javascript" src="resources/ScalaReference.js"></script>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
tex2jax: {
View
20 resources/style.css
@@ -36,7 +36,9 @@ code {
/* examples */
ol[type="1"] {
list-style-type: none;
- margin-left: 0;
+ margin-left: 3em;
+ margin-right: 3em;
+ padding: 0;
}
ol[type="1"] li {
@@ -48,4 +50,20 @@ ol[type="1"] li {
ol[type="1"] li:before {
content: "Example ";
+}
+
+#popoutTOC {
+ position: fixed;
+ top: 0;
+ left: 0;
+ margin: 0;
+ padding: 0;
+}
+
+#popoutTOC .head {
+
+}
+
+#popoutTOC .links {
+ display: none;
}

0 comments on commit bb53357

Please sign in to comment.