From 025dc51c2eef7e7ea302465ff05d04d6fd4e7173 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sun, 8 Dec 2019 19:24:43 +0900 Subject: Coherence checking for coercions This change improves the relaxed ambiguous path condition of coercions (#9743) to check that any circular inheritance path of `C >-> C` is definitionally equal to the identity function of the class `C`. Moreover, for a new inheritance path `p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not report the ambiguity of `p` and `q` if they have a common element, that is to say: `p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2` for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`. In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be checked; thus, checking the ambiguity of `p` and `q` is redundant with them. If the new mechanism does not report any ambiguous path, the inheritance graph must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]: 1. for any circular path `p : C >-> C`, `p` is definitionally equal to the identity function, and 2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible. [Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95, LNCS, vol 1158, Springer, 1996, pp 1-15. [Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance, In: POPL '97, ACM, 1997, pp 292-301. --- doc/changelog/07-commands-and-options/11258-coherence.rst | 10 ++++++++++ doc/sphinx/addendum/implicit-coercions.rst | 6 ++++++ 2 files changed, 16 insertions(+) create mode 100644 doc/changelog/07-commands-and-options/11258-coherence.rst (limited to 'doc') diff --git a/doc/changelog/07-commands-and-options/11258-coherence.rst b/doc/changelog/07-commands-and-options/11258-coherence.rst new file mode 100644 index 0000000000..f04a120417 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11258-coherence.rst @@ -0,0 +1,10 @@ +- **Changed:** + The :cmd:`Coercion` command has been improved to check the coherence of the + inheritance graph. It checks whether a circular inheritance path of `C >-> C` + is convertible with the identity function or not, then report it as an + ambiguous path if it is not. The new mechanism does not report ambiguous + paths that are redundant with others. For example, checking the ambiguity of + `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will + not be reported + (`#11258 `_, + by Kazuhiko Sakaguchi). diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c3b197288f..19b33f0d90 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -165,6 +165,12 @@ Declaring Coercions convertible with existing ones when they have coercions that don't satisfy the uniform inheritance condition. + .. warn:: ... is not definitionally an identity function. + + If a coercion path has the same source and target class, that is said to be + circular. When a new circular coercion path is not convertible with the + identity function, it will be reported as ambiguous. + .. cmdv:: Local Coercion @qualid : @class >-> @class Declares the construction denoted by :token:`qualid` as a coercion local to -- cgit v1.2.3