mirror of
https://github.com/dart-lang/sdk
synced 2024-09-05 16:41:07 +00:00
Remove docs/language/informal/subtyping.md, which is now in the language repo
Change-Id: I9ccea6c780f2b47a0097e462f8d395aca565b0f4 Reviewed-on: https://dart-review.googlesource.com/c/87703 Reviewed-by: Bob Nystrom <rnystrom@google.com>
This commit is contained in:
Leaf Petersen
parent
f69aabdb62
commit
a862e8645a
|
|
@ -1,474 +0,0 @@
|
|||
# Dart 2.0 Static and Runtime Subtyping
|
||||
|
||||
leafp@google.com
|
||||
|
||||
**Status**: This document is now background material.
|
||||
For normative text, please consult the language specification.
|
||||
|
||||
This is intended to define the core of the Dart 2.0 static and runtime subtyping
|
||||
relation.
|
||||
|
||||
|
||||
## Types
|
||||
|
||||
The syntactic set of types used in this draft are a slight simplification of
|
||||
full Dart types.
|
||||
|
||||
The meta-variables `X`, `Y`, and `Z` range over type variables.
|
||||
|
||||
The meta-variables `T`, `S`, `U`, and `V` range over types.
|
||||
|
||||
The meta-variable `C` ranges over classes.
|
||||
|
||||
The meta-variable `B` ranges over types used as bounds for type variables.
|
||||
|
||||
As a general rule, indices up to `k` are used for type parameters and type
|
||||
arguments, `n` for required value parameters, and `m` for all value parameters.
|
||||
|
||||
The set of types under consideration are as follows:
|
||||
|
||||
- Type variables `X`
|
||||
- Promoted type variables `X & T` *Note: static only*
|
||||
- `Object`
|
||||
- `dynamic`
|
||||
- `void`
|
||||
- `Null`
|
||||
- `Function`
|
||||
- `Future<T>`
|
||||
- `FutureOr<T>`
|
||||
- Interface types `C`, `C<T0, ..., Tk>`
|
||||
- Function types
|
||||
- `U Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`
|
||||
- `U Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})`
|
||||
|
||||
We leave the set of interface types unspecified, but assume a class hierarchy
|
||||
which provides a mapping from interfaces types `T` to the set of direct
|
||||
super-interfaces of `T` induced by the superclass declaration, implemented
|
||||
interfaces, and mixins of the class of `T`. Among other well-formedness
|
||||
constraints, the edges induced by this mapping must form a directed acyclic
|
||||
graph rooted at `Object`.
|
||||
|
||||
The types `Object`, `dynamic` and `void` are all referred to as *top* types, and
|
||||
are considered equivalent as types (including when they appear as sub-components
|
||||
of other types). They exist as distinct names only to support distinct errors
|
||||
and warnings (or absence thereof).
|
||||
|
||||
The type `X & T` represents the result of a type promotion operation on a
|
||||
variable. In certain circumstances (defined elsewhere) a variable `x` of type
|
||||
`X` that is tested against the type `T` (e.g. `x is T`) will have its type
|
||||
replaced with the more specific type `X & T`, indicating that while it is known
|
||||
to have type `X`, it is also known to have the more specific type `T`. Promoted
|
||||
type variables only occur statically (never at runtime).
|
||||
|
||||
Given the current promotion semantics the following properties are also true:
|
||||
- If `X` has bound `B` then for any type `X & T`, `T <: B` will be true.
|
||||
- Promoted type variable types will only appear as top level types: that is,
|
||||
they can never appear as sub-components of other types, in bounds, or as
|
||||
part of other promoted type variables.
|
||||
|
||||
|
||||
## Notation
|
||||
|
||||
We use `S[T0/Y0, ..., Tk/Yk]` for the result of performing a simultaneous
|
||||
capture-avoiding substitution of types `T0, ..., Tk` for the type variables
|
||||
`Y0, ..., Yk` in the type `S`.
|
||||
|
||||
|
||||
## Type equality
|
||||
|
||||
We say that a type `T0` is equal to another type `T1` (written `T0 === T1`) if
|
||||
the two types are structurally equal up to renaming of bound type variables,
|
||||
and equating all top types.
|
||||
|
||||
TODO: make these rules explicit.
|
||||
|
||||
|
||||
## Algorithmic subtyping
|
||||
|
||||
By convention the following rules are intended to be applied in top down order,
|
||||
with exactly one rule syntactically applying. That is, rules are written in the
|
||||
form:
|
||||
|
||||
```
|
||||
Syntactic criteria.
|
||||
- Additional condition 1
|
||||
- Additional or alternative condition 2
|
||||
```
|
||||
|
||||
and it is the case that if a subtyping query matches the syntactic criteria for
|
||||
a rule (but not the syntactic criteria for any rule preceeding it), then the
|
||||
subtyping query holds iff the listed additional conditions hold.
|
||||
|
||||
This makes the rules algorithmic, because they correspond in an obvious manner
|
||||
to an algorithm with an acceptable time complexity, and it makes them syntax
|
||||
directed because the overall structure of the algorithm corresponds to specific
|
||||
syntactic shapes. We will use the word _algorithmic_ to refer to this property.
|
||||
|
||||
The runtime subtyping rules can be derived by eliminating all clauses dealing
|
||||
with promoted type variables.
|
||||
|
||||
|
||||
### Rules
|
||||
|
||||
We say that a type `T0` is a subtype of a type `T1` (written `T0 <: T1`) when:
|
||||
|
||||
- **Reflexivity**: `T0` and `T1` are the same type.
|
||||
- *Note that this check is necessary as the base case for primitive types, and
|
||||
type variables but not for composite types. In particular, algorithmically
|
||||
a structural equality check is admissible, but not required
|
||||
here. Pragmatically, non-constant time identity checks here are
|
||||
counter-productive*
|
||||
|
||||
- **Right Top**: `T1` is a top type (i.e. `Object`, `dynamic`, or `void`).
|
||||
|
||||
- **Left Bottom**: `T0` is `Null`
|
||||
|
||||
- **Left FutureOr**: `T0` is `FutureOr<S0>`
|
||||
- and `Future<S0> <: T1`
|
||||
- and `S0 <: T1`
|
||||
|
||||
- **Type Variable Reflexivity 1**: `T0` is a type variable `X0` or a
|
||||
promoted type variables `X0 & S0` and `T1` is `X0`.
|
||||
- *Note that this rule is admissible, and can be safely elided if desired*
|
||||
|
||||
- **Type Variable Reflexivity 2**: Promoted`T0` is a type variable `X0` or a
|
||||
promoted type variables `X0 & S0` and `T1` is `X0 & S1`
|
||||
- and `T0 <: S1`.
|
||||
- *Note that this rule is admissible, and can be safely elided if desired*
|
||||
|
||||
- **Right Promoted Variable**: `T1` is a promoted type variable `X1 & S1`
|
||||
- and `T0 <: X1`
|
||||
- and `T0 <: S1`
|
||||
|
||||
- **Right FutureOr**: `T1` is `FutureOr<S1>` and
|
||||
- either `T0 <: Future<S1>`
|
||||
- or `T0 <: S1`
|
||||
- or `T0` is `X0` and `X0` has bound `S0` and `S0 <: T1`
|
||||
- or `T0` is `X0 & S0` and `S0 <: T1`
|
||||
|
||||
- **Left Promoted Variable**: `T0` is a promoted type variable `X0 & S0`
|
||||
- and `S0 <: T1`
|
||||
|
||||
- **Left Type Variable Bound**: `T0` is a type variable `X0` with bound `B0`
|
||||
- and `B0 <: T1`
|
||||
|
||||
- **Function Type/Function**: `T0` is a function type and `T1` is `Function`
|
||||
|
||||
- **Interface Compositionality**: `T0` is an interface type `C0<S0, ..., Sk>`
|
||||
and `T1` is `C0<U0, ..., Uk>`
|
||||
- and each `Si <: Ui`
|
||||
|
||||
- **Super-Interface**: `T0` is an interface type with super-interfaces `S0,...Sn`
|
||||
- and `Si <: T1` for some `i`
|
||||
|
||||
- **Positional Function Types**: `T0` is
|
||||
`U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn, [Vn+1 xn+1, ..., Vm xm])`
|
||||
- and `T1` is
|
||||
`U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sp yp, [Sp+1 yp+1, ..., Sq yq])`
|
||||
- and `p >= n`
|
||||
- and `m >= q`
|
||||
- and `Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk]` for `i` in `0...q`
|
||||
- and `U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]`
|
||||
- and `B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk]` for `i` in `0...k`
|
||||
- where the `Zi` are fresh type variables with bounds `B0i[Z0/X0, ..., Zk/Xk]`
|
||||
|
||||
- **Named Function Types**: `T0` is
|
||||
`U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn, {Vn+1 xn+1, ..., Vm xm})`
|
||||
- and `T1` is
|
||||
`U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn, {Sn+1 yn+1, ..., Sq yq})`
|
||||
- and `{yn+1, ... , yq}` subsetof `{xn+1, ... , xm}`
|
||||
- and `Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk]` for `i` in `0...n`
|
||||
- and `Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk]` for `i` in `n+1...q`, `yj = xi`
|
||||
- and `U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]`
|
||||
- and `B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk]` for `i` in `0...k`
|
||||
- where the `Zi` are fresh type variables with bounds `B0i[Z0/X0, ..., Zk/Xk]`
|
||||
|
||||
*Note: the requirement that `Zi` are fresh is as usual strictly a requirement
|
||||
that the choice of common variable names avoid capture. It is valid to choose
|
||||
the `Xi` or the `Yi` for `Zi` so long as capture is avoided*
|
||||
|
||||
|
||||
## Derivation of algorithmic rules
|
||||
|
||||
This section sketches out the derivation of the algorithmic rules from the
|
||||
interpretation of `FutureOr` as a union type, and promoted type bounds as
|
||||
intersection types, based on standard rules for such types that do not satisfy
|
||||
the requirements for being algorithmic.
|
||||
|
||||
|
||||
### Non-algorithmic rules
|
||||
|
||||
The non-algorithmic rules that we derive from first principles of union and
|
||||
intersection types are as follows:
|
||||
|
||||
Left union introduction:
|
||||
- `FutureOr<S> <: T` if `Future<S> <: T` and `S <: T`
|
||||
|
||||
Right union introduction:
|
||||
- `S <: FutureOr<T>` if `S <: Future<T>` or `S <: T`
|
||||
|
||||
Left intersection introduction:
|
||||
- `X & S <: T` if `X <: T` or `S <: T`
|
||||
|
||||
Right intersection introduction:
|
||||
- `S <: X & T` if `S <: X` and `S <: T`
|
||||
|
||||
The only remaining non-algorithmic rule is the variable bounds rule:
|
||||
|
||||
Variable bounds:
|
||||
- `X <: T` if `X extends B` and `B <: T`
|
||||
|
||||
All other rules are algorithmic.
|
||||
|
||||
Note: We believe that bounds can be treated simply as uses of intersections,
|
||||
which could simplify this presentation.
|
||||
|
||||
|
||||
### Preliminaries
|
||||
|
||||
**Lemma 1**: If there is any derivation of `FutureOr<S> <: T`, then there is a
|
||||
derivation ending in a use of left union introduction.
|
||||
|
||||
Proof. By induction on derivations. Consider a derivation of `FutureOr<S> <:
|
||||
T`.
|
||||
|
||||
If the last rule applied is:
|
||||
- Top type rules are trivial.
|
||||
|
||||
- Null, Function and interface rules can't apply.
|
||||
|
||||
- Left union introduction rule is immediate.
|
||||
|
||||
- Right union introduction. Then `T` is of the form `FutureOr<T0>`, and either
|
||||
- we have a sub-derivation of `FutureOr<S> <: Future<T0>`
|
||||
- by induction we therefore have a derivation ending in left union
|
||||
introduction, so by inversion we have:
|
||||
- a derivation of `Future<S> <: Future<T0> `, and so by right union
|
||||
introduction we have `Future<S> <: FutureOr<T0>`
|
||||
- a derivation of `S <: Future<T0> `, and so by right union
|
||||
introduction we have `S <: FutureOr<T0>`
|
||||
- by left union introduction, we have `FutureOr<S> <: FutureOr<T0>`
|
||||
- QED
|
||||
- we have a sub-derivation of `FutureOr<S> <: T0`
|
||||
- by induction we therefore have a derivation ending in left union
|
||||
introduction, so by inversion we have:
|
||||
- a derivation of `Future<S> <: T0 `, and so by right union
|
||||
introduction we have `Future<S> <: FutureOr<T0>`
|
||||
- a derivation of `S <: T0 `, and so by right union
|
||||
introduction we have `S <: FutureOr<T0>`
|
||||
- by left union introduction, we have `FutureOr<S> <: FutureOr<T0>`
|
||||
- QED
|
||||
|
||||
- Right intersection introduction. Then `T` is of the form `X & T0`, and
|
||||
- we have sub-derivations `FutureOr<S> <: X` and `FutureOr<S> <: T0`
|
||||
- By induction, we can get derivations of the above ending in left union
|
||||
introduction, so by inversion we have derivations of:
|
||||
- `Future<S> <: X`, `S <: X`, `Future<S> <: T0`, `S <: T0`
|
||||
- so we have derivations of `S <: X`, `S <: T0`, so by right
|
||||
intersection introduction we have
|
||||
- `S <: X & T0`
|
||||
- so we have derivations of `Future<S> <: X`, `Future<S> <: T0`, so by right
|
||||
intersection introduction we have
|
||||
- `Future<S> <: X & T0`
|
||||
- so by left union introduction, we have a derivation of `FutureOr<S> <: X & T0`
|
||||
- QED
|
||||
|
||||
Note: The reverse is not true. Counter-example:
|
||||
|
||||
Given arbitrary `B <: A`, suppose we wish to show that `(X extends FutureOr<B>)
|
||||
<: FutureOr<A>`. If we apply right union introduction first, we must show
|
||||
either:
|
||||
- `X <: Future<A>`
|
||||
- only variable bounds rule applies, so we must show
|
||||
- `FutureOr<B> <: Future<A>`
|
||||
- Only left union introduction applies, so we must show both of:
|
||||
- `Future<B> <: Future<A>` (yes)
|
||||
- `B <: Future<A>` (no)
|
||||
- `X <: A`
|
||||
- only variable bounds rule applies, so we must show that
|
||||
- `FutureOr<B> <: A`
|
||||
- Only left union introduction applies, so we must show both of:
|
||||
- `Future<B> <: Future<A>` (no)
|
||||
- `B <: Future<A>` (yes)
|
||||
|
||||
On the other hand, the derivation via first applying the variable bounds rule is
|
||||
trivial.
|
||||
|
||||
Note though that we can also not simply always apply the variable bounds rule
|
||||
first. Counter-example:
|
||||
|
||||
Given `X extends Object`, it is trivial to derive `X <: FutureOr<X>` via the
|
||||
right union introduction rule. But applying the variable bounds rule doesn't
|
||||
work.
|
||||
|
||||
**Lemma 2**: If there is any derivation of `S <: X & T`, then there is
|
||||
derivation ending in a use of right intersection introduction.
|
||||
|
||||
Proof. By induction on derivations. Consider a derivation D of `S <: X & T`.
|
||||
|
||||
If last rule applied in D is:
|
||||
- Bottom types are trivial.
|
||||
|
||||
- Function and interface type rules can't apply.
|
||||
|
||||
- Right intersection introduction then we're done.
|
||||
|
||||
- Left intersection introduction. Then `S` is of the form `Y & S0`, and either
|
||||
- we have a sub-derivation of `Y <: X & T`
|
||||
- by induction we therefore have a derivation ending in right intersection
|
||||
introduction, so by inversion we have:
|
||||
- a derivation of `Y <: X `, and so by left intersection
|
||||
introduction we have `Y & S0 <: X`
|
||||
- a derivation of `Y <: T `, and so by left intersection
|
||||
introduction we have `Y & S0 <: T`
|
||||
- by right intersection introduction, we have `Y & S0 <: X & T`
|
||||
- QED
|
||||
- we have a sub-derivation of `S0 <: X & T`
|
||||
- by induction we therefore have a derivation ending in right intersection
|
||||
introduction, so by inversion we have:
|
||||
- a derivation of `S0 <: X `, and so by left intersection
|
||||
introduction we have `Y & S0 <: X`
|
||||
- a derivation of `S0 <: T `, and so by left intersection
|
||||
introduction we have `Y & S0 <: T`
|
||||
- by right intersection introduction, we have `Y & S0 <: X & T`
|
||||
- QED
|
||||
|
||||
- Left union introduction. Then `S` is of the form `FutureOr<S0>`, and
|
||||
- we have sub-derivations `Future<S0> <: X & T` and `S0 <: X & T`
|
||||
- By induction, we can get derivations of the above ending in right intersection
|
||||
introduction, so by inversion we have derivations of:
|
||||
- `Future<S0> <: X`, `S0 <: X`, `Future<S0> <: T`, `S0 <: T`
|
||||
- so we have derivations of `S0 <: X`, `Future<S0> <: X`, so by left
|
||||
union introduction we have
|
||||
- `FutureOr<S0> <: X`
|
||||
- so we have derivations of `S0 <: T`, `Future<S0> <: T`, so by left
|
||||
union introduction we have
|
||||
- `FutureOr<S0> <: T`
|
||||
- so by right intersection introduction, we have a derivation of `FutureOr<S0> <: X & T`
|
||||
- QED
|
||||
|
||||
**Conjecture 1**: `FutureOr<A> <: FutureOr<B>` is derivable iff `A <: B` is
|
||||
derivable.
|
||||
|
||||
Showing that `A <: B => FutureOr<A> <: FutureOr<B>` is easy, but it is not
|
||||
immediately clear how to tackle the opposite direction.
|
||||
|
||||
**Lemma 3**: Transitivity of subtyping is admissible. Given derivations of `A <: B`
|
||||
and `B <: C`, there is a derivation of `A <: C`.
|
||||
|
||||
Proof sketch: The proof should go through by induction on sizes of derivations,
|
||||
cases on pairs of rules used. For any pair of rules used, we can construct a
|
||||
new derivation of the desired result using only smaller derivations.
|
||||
|
||||
**Observation 1**: Given `X` with bound `S`, we have the property that for all
|
||||
instances of `X & T`, `T <: S` will be true, and hence `S <: M => T <: M`.
|
||||
|
||||
|
||||
### Algorithmic rules
|
||||
|
||||
Consider `T0 <: T1`.
|
||||
|
||||
|
||||
#### Union on the left
|
||||
|
||||
By lemma 1, if `T0` is of the form `FutureOr<S0>` and there is any derivation of
|
||||
`T0 <: T1`, then there is a derivation ending with a use of left union
|
||||
introduction so we have the rule:
|
||||
|
||||
- `T0` is `FutureOr<S0>`
|
||||
- and `Future<S0> <: T1`
|
||||
- and `S0 <: T1`
|
||||
|
||||
|
||||
#### Identical type variables
|
||||
|
||||
If `T0` and `T1` are both the same unpromoted type variable, then subtyping
|
||||
holds by reflexivity. If `T0` is a promoted type variable `X0 & S0`, and `T0`
|
||||
is `X0` then it suffices to show that `X0 <: X0` or `S0 <: X0`, and the former
|
||||
holds immediately. This justifies the rule:
|
||||
|
||||
- `T0` is a type variable `X0` or a promoted type variables `X0 & S0` and `T1`
|
||||
is `X0`.
|
||||
|
||||
If `T0` is `X0` or `X0 & S0` and `T1` is `X0 & S1`, then by lemma 1 it suffices
|
||||
to show that `X0 & S0 <: X0` and `X0 & S0 <: S1`. The first holds immediately
|
||||
by reflexivity on the type variable, so it is sufficient to check `T0 <: S1`.
|
||||
|
||||
- `T0` is a type variable `X0` or a promoted type variables `X0 & S0` and `T1`
|
||||
is `X0 & S1`
|
||||
- and `T0 <: S1`.
|
||||
|
||||
*Note that neither of the previous rules are required to make the rules
|
||||
algorithmic: they are merely useful special cases of the next rule.*
|
||||
|
||||
|
||||
#### Intersection on the right
|
||||
|
||||
By lemma 2, if `T1` is of the `X1 & S1` and there is any derivation of `T0 <:
|
||||
T1`, then there is a derivation ending with a use of right intersection
|
||||
introduction, hence the rule:
|
||||
|
||||
- `T1` is a promoted type variable `X1 & S1`
|
||||
- and `T0 <: X1`
|
||||
- and `T0 <: S1`
|
||||
|
||||
|
||||
#### Union on the right
|
||||
|
||||
Suppose `T1` is `FutureOr<S1>`. The rules above have eliminated the possibility
|
||||
that `T0` is of the form `FutureOr<S0`. The only rules that could possibly
|
||||
apply then are right union introduction, left intersection introduction, or the
|
||||
variable bounds rules. Combining these yields the following preliminary
|
||||
disjunctive rule:
|
||||
|
||||
- `T1` is `FutureOr<S1>` and
|
||||
- either `T0 <: Future<S1>`
|
||||
- or `T0 <: S1`
|
||||
- or `T0` is `X0` and `X0` has bound `S0` and `S0 <: T1`
|
||||
- or `T0` is `X0 & S0` and `X0 <: T1` and `S0 <: T1`
|
||||
|
||||
The last disjunctive clause can be further simplified to
|
||||
- or `T0` is `X0 & S0` and `S0 <: T1`
|
||||
|
||||
since the premise `X0 <: FutureOr<S1>` can only derived either using the
|
||||
variable bounds rule or right union introduction. For the variable bounds rule,
|
||||
the premise `B0 <: T1` is redundant with `S0 <: T1` by observation 1. For right
|
||||
union introduction, `X0 <: S1` is redundant with `T0 <: S1`, since if `X0 <: S1`
|
||||
is derivable, then `T0 <: S1` is derivable by left union introduction; and `X0
|
||||
<: Future<S1>` is redundant with `T0 <: Future<S1>`, since if the former is
|
||||
derivable, then the latter is also derivable by left intersection introduction.
|
||||
So we have the final rule:
|
||||
|
||||
- `T1` is `FutureOr<S1>` and
|
||||
- either `T0 <: Future<S1>`
|
||||
- or `T0 <: S1`
|
||||
- or `T0` is `X0` and `X0` has bound `S0` and `S0 <: T1`
|
||||
- or `T0` is `X0 & S0` and `S0 <: T1`
|
||||
|
||||
|
||||
#### Intersection on the left
|
||||
|
||||
Suppose `T0` is `X0 & S0`. We've eliminated the possibility that `T1` is
|
||||
`FutureOr<S1>`, the possibility that `T1` is `X1 & S1`, and the possibility that
|
||||
`T1` is any variant of `X0`. The only remaining rule that applies is left
|
||||
intersection introduction, and so it suffices to check that `X0 <: T1` and `S0
|
||||
<: T1`. But given the remaining possible forms for `T1`, the only rule that can
|
||||
apply to `X0 <: T1` is the variable bounds rule, which by observation 1 is
|
||||
redundant with the second premise, and so we have the rule:
|
||||
|
||||
`T0` is a promoted type variable `X0 & S0`
|
||||
- and `S0 <: T1`
|
||||
|
||||
|
||||
#### Type variable on the left
|
||||
|
||||
Suppose `T0` is `X0`. We've eliminated the possibility that `T1` is
|
||||
`FutureOr<S1>`, the possibility that `T1` is `X1 & S1`, and the possibility that
|
||||
`T1` is any variant of `X0`. The only rule that applies is the variable bounds
|
||||
rule:
|
||||
|
||||
`T0` is a type variable `X0` with bound `B0`
|
||||
- and `B0 <: T1`
|
||||
|
||||
This eliminates all of the non-algorithmic rules: the remainder are strictly
|
||||
algorithmic.
|
||||
Loading…
Reference in a new issue