diff --git a/docs/docs/reference/new-types/dependent-function-types-spec.md b/docs/docs/reference/new-types/dependent-function-types-spec.md index ca73a94d5ea9..9159d4b51df2 100644 --- a/docs/docs/reference/new-types/dependent-function-types-spec.md +++ b/docs/docs/reference/new-types/dependent-function-types-spec.md @@ -3,14 +3,14 @@ layout: doc-page title: "Dependent Function Types - More Details" --- -Initial implementation in (#3464)[https://github.com/lampepfl/dotty/pull/3464]. +Initial implementation in [#3464](https://github.com/lampepfl/dotty/pull/3464) ## Syntax FunArgTypes ::= InfixType | ‘(’ [ FunArgType {‘,’ FunArgType } ] ‘)’ - | '(' TypedFunParam {',' TypedFunParam } ')' - TypedFunParam ::= id ':' Type + | ‘(’ TypedFunParam {',' TypedFunParam } ‘)’ + TypedFunParam ::= id ‘:’ Type Dependent function types associate to the right, e.g. `(s: S) ⇒ (t: T) ⇒ U` is the same as `(s: S) ⇒ ((t: T) ⇒ U)`. @@ -39,9 +39,9 @@ documentation](https://dotty.epfl.ch/docs/reference/dropped-features/limit22.htm ## Examples -- (depfuntype.scala)[https://github.com/lampepfl/dotty/blob/0.10.x/tests/pos/depfuntype.scala] +- [depfuntype.scala](https://github.com/lampepfl/dotty/blob/master/tests/pos/depfuntype.scala) -- (eff-dependent.scala)[https://github.com/lampepfl/dotty/blob/0.10.x/tests/run/eff-dependent.scala] +- [eff-dependent.scala](https://github.com/lampepfl/dotty/blob/master/tests/run/eff-dependent.scala) ### Type Checking diff --git a/docs/docs/reference/new-types/match-types.md b/docs/docs/reference/new-types/match-types.md index 8c6e0bb60123..72f836f0182f 100644 --- a/docs/docs/reference/new-types/match-types.md +++ b/docs/docs/reference/new-types/match-types.md @@ -74,7 +74,7 @@ if `Ci = [Xs] => P => T` and there are minimal instantiations `Is` of the type v T' = [Xs := Is] T ``` An instantiation `Is` is _minimal_ for `Xs` if all type variables in `Xs` that appear -covariantly and nonvariantly in `Is` are as small as possible and all type variables in `Xs` that appear contravariantly in `Is` are as large as possible. Here, "small" and "large" are understood wrt `<:`. +covariantly and nonvariantly in `Is` are as small as possible and all type variables in `Xs` that appear contravariantly in `Is` are as large as possible. Here, "small" and "large" are understood with respect to `<:`. For simplicity, we have omitted constraint handling so far. The full formulation of subtyping tests describes them as a function from a constraint and a pair of types to either _success_ and a new constraint or _failure_. In the context of reduction, the subtyping test `S <: [Xs := Is] P` is understood to leave the bounds of all variables @@ -88,8 +88,8 @@ if ``` Match(S, C1, ..., Cn) can-reduce i, T ``` -and, for `j` in `1..i-1`: `C_j` is disjoint from `C_i`, or else `S` cannot possibly match `C_j`. -See the section on overlapping patterns for an elaboration of "disjoint" and "cannot possibly match". +and, for `j` in `1..i-1`: `Cj` is disjoint from `Ci`, or else `S` cannot possibly match `Cj`. +See the section on [overlapping patterns](#overlapping-patterns) for an elaboration of "disjoint" and "cannot possibly match". ## Subtyping Rules for Match Types @@ -97,11 +97,11 @@ The following rules apply to match types. For simplicity, we omit environments a The first rule is a structural comparison between two match types: ``` - Match(S, C1, ..., Cn) <: Match(T, D1, ..., Dm) + Match(S, C1, ..., Cm) <: Match(T, D1, ..., Dn) ``` ` `if ``` - S <: T, m <= n, Ci <: Di for i in 1..n + S <: T, m >= n, Ci <: Di for i in 1..n ``` I.e. scrutinees and corresponding cases must be subtypes, no case re-ordering is allowed, but the subtype can have more cases than the supertype. @@ -160,7 +160,7 @@ Assuming this extension, we can then try to typecheck as usual. E.g. to typechec Typechecking the second case hits a snag, though. In general, the assumption `x.type <: B` is not enough to prove that `M[x.type]` reduces to `2`. However we can reduce `M[x.type]` to `2` if the types `A` and `B` do not overlap. -So correspondence of match terms to match types is feasible only in the case of non-overlapping patterns. +So correspondence of match terms to match types is feasible only in the case of non-overlapping patterns (see next section about [overlapping patterns](#overlapping-patterns)) For simplicity, we have disregarded the `null` value in this discussion. `null` does not cause a fundamental problem but complicates things somewhat because some forms of patterns do not match `null`. @@ -172,10 +172,10 @@ A complete defininition of when two patterns or types overlap still needs to be - A final class `C` overlaps with a trait `T` only if `C` extends `T` directly or indirectly. - A class overlaps with a sealed trait `T` only if it overlaps with one of the known subclasses of `T`. - An abstract type or type parameter `A` overlaps with a type `B` only if `A`'s upper bound overlaps with `B`. - - A union type `A_1 | A_2` overlaps with `B` only if `A_1` overlaps with `B` or `A_2` overlaps with `B`. - - An intersection type `A_1 & A_2` overlaps with `B` only if both `A_1` and `A_2` overlap with `B`. - - If `C[X_1, ..., X_n]` is a case class, then the instance type `C[A_1, ..., A_n]` overlaps with the instance type `C[B_1, ..., B_n]` only if for every index `i` in `1..n`, - if `X_i` is the type of a parameter of the class, then `A_i` overlaps with `B_i`. + - A union type `A1 | ... | An` overlaps with `B` only if at least one of `Ai` for `i` in `1..n` overlaps with `B`. + - An intersection type `A1 & ... & An` overlaps with `B` only if all of `Ai` for `i` in `1..n` overlap with `B`. + - If `C[X1, ..., Xn]` is a case class, then the instance type `C[A1, ..., An]` overlaps with the instance type `C[B1, ..., Bn]` only if for every index `i` in `1..n`, + if `Xi` is the type of a parameter of the class, then `Ai` overlaps with `Bi`. The last rule in particular is needed to detect non-overlaps for cases where the scrutinee and the patterns are tuples. I.e. `(Int, String)` does not overlap `(Int, Int)` since `String` does not overlap `Int`.