diff --git a/docs/language/informal/instantiate-to-bound.md b/docs/language/informal/instantiate-to-bound.md index d182dcb8574..091c50769b9 100644 --- a/docs/language/informal/instantiate-to-bound.md +++ b/docs/language/informal/instantiate-to-bound.md @@ -2,7 +2,7 @@ **Author**: eernst@ -**Version**: 0.5 (2018-01-11) +**Version**: 0.7 (2018-02-26) **Status**: Under implementation. @@ -191,40 +191,41 @@ _Up,m_ (*so each type variable is related to, that is, depends on, every type variable in its bound, possibly including itself*). Let _==>m_ be the transitive closure of _-->m_. For each _m_, let _Ui,m+1_, for _i_ in _1 .. k_, be determined -as follows: +by the following iterative process: -- Let _j_ be the lowest number such that - _Xj ==>m Xj_ (*that is, such that this - type variable is a member of a dependency cycle*). - Let _{Y1 .. Yp}_ be the the maximal subset - containing _Xj_ of _{X1 .. Xk}_ where - every pair is related: _Yq ==>m Yr_, for - all _q, r_ in _1 .. p_ (*i.e., this subset is a strongly connected - component in the dependency graph containing _Xj_*). - Then _Ui,m+1_ is the result of substituting, in - _Ui,m_, `Null` for every contravariant occurrence - of _Xj_, and `dynamic` for every covariant occurrence of - _Xj_, for all _i_ in _1 .. k_ such that _Xi_ is a - member of _{Y1 .. Yp}_; and _Ui,m+1_ is - _Ui,m_, for all other _i_ in _1 .. k_. - *That is, we update the bounds of type variables in the dependency cycle - such that the type variables in the dependency cycle are replaced by - `Null` or `dynamic`, depending on the variance of the location.* +1. If there exists a _j_ in _1 .. k_ such that + _Xj ==>m Xj_ + (*that is, if the dependency graph has a cycle*) + let _M1 .. Mp_ be the strongly connected components + (SCCs) with respect to _-->m_ + (*that is, the maximal subsets of _X1 .. Xk_ + where every pair of variables in each subset are related in both directions + by _==>m_; note that the SCCs are pairwise disjoint; also, they + are uniquely defined up to reordering, and the order does not matter*). + Let _M_ be the union of _M1 .. Mp_ + (*that is, all variables that participate in a dependency cycle*). + Let _i_ be in _1 .. k_. + If _Xi_ does not belong to _M_ then + _Ui,m+1 = Ui,m_. + Otherwise there exists a _q_ such that _Xi_ belongs to + _Mq_; _Ui,m+1_ is then obtained from _Ui,m_ + by replacing every covariant occurrence of a variable in _Mq_ by + `dynamic`, and replacing every contravariant occurence of a variable in + _Mq_ by `Null`. -- Otherwise, (*if no such dependency cycle exists*) let _j_ be the - lowest number such that _Xj_ occurs in - _Up,m_ for some _p_ and - _Xj -/->m Xq_ for all _q_ in _1..k_ - (*that is, _Uj,m_ is closed, that is, the current bound of - _Xj_ does not depend on any other type variables; but - _Xj_ is being depended on by the bounds of some other type - variables*). Then _Ui,m+1_ is the result of substituting, in - _Ui,m_, `Null` for every contravariant occurrence - of _Xj_, and _Uj,m_ for every covariant occurrence - of _Xj_, for all _i_ in _1 .. k_. +2. Otherwise, (*if no dependency cycle exists*) let _j_ be the lowest number + such that _Xj_ occurs in _Up,m_ for some _p_ and + _Xj -/->m Xq_ for all _q_ in _1..k_ + (*that is, _Uj,m_ is closed, that is, the current bound of + _Xj_ does not contain any type variables; but _Xj_ is + being depended on by the bound of some other type variable*). + Then, for all _i_ in _1 .. k_, _Ui,m+1_ is obtained from + _Ui,m_ by replacing every covariant occurrence of _Xj_ + by _Uj,m_, and replacing every contravariant occurrence of + _Xj_ by `Null`. -- Otherwise, (*when no dependencies exist*) terminate with the result - _<U1,m ..., Uk,m>_. +3. Otherwise, (*when no dependencies exist*) terminate with the result + _<U1,m ..., Uk,m>_. *This process will always terminate, because the total number of occurrences of type variables from _{X1 .. Xk}_ in @@ -259,6 +260,13 @@ applicable. ## Updates +* Feb 26th 2018, version 0.7: Revised cycle breaking algorithm for + F-bounded type variables to avoid specifying orderings that do not matter. + +* Feb 22nd 2018, version 0.6: Revised cycle breaking algorithm for + F-bounded type variables to replace all members by an extreme type, not + just one of them. + * Jan 11th 2018, version 0.5: Revised treatment of variance based on strongly connected components in the dependency graph.