# Replace SubtypeOperator #697

Closed
opened this Issue Nov 7, 2016 · 3 comments

Projects
None yet
1 participant
Member

### DavePearce commented Nov 7, 2016

 We now know that `SubtypeOperator` is very broken and causes many problems. The question is: can we replace it? Or, to put it another way: do we know the algorithm for implementing subtyping in Whiley? At this stage, I'm not completely sure that we do (though @richdougherty has been making progress). Here are related discussions: #645 --- Dealing with uninhabited and non-contractive types. #678 --- Thoughts on simplifying types. #619 --- A good (though incomplete) list of simplification rules. In #645, I've identified three aspects of the subtyping problem. But, none of these phases resolve issues related to equivalence or subsumption between recursive types: Equivalence. Determining that two recursive types are, in fact, equivalent. This is problematic in the case of equivalent types with different amounts of unrolling. Subsumption. This is just a more general form of the equivalence problem. In the VMCAI paper, a fundamental subtype operator over atoms was provided. This was easy to implement. However, for "recursive atoms", this operator is somehow harder (though I'm not sure exactly how much harder). Considering the equivalence problem, consider these two types in Whiley: ```type A_List is null | { int data, A_List next } type B_List is null | { int data, null | { int data, B_List next } next } ``` These two types are equivalent. However, a simple rewrite-based approach to simplification will not be able to determine this. In the existing `SubtypeOperator` implementation, a subtype "relation" is used to resolve this where all subtypes are initially considered as true. As an example of the subsumption problem, consider these: ```type A_List is null | { int data, A_List next } type B_List is null | { any data, B_List next } ``` Now, imagine simplifying `A_List & !B_list` This should give `void`, but it requires establishing that `A_List <: B_List`. Or, does it? We can expand this example using DeMorgan's laws as follows. ```(null | { int data, X next }) & !(null | { int data, X next }) ``` Push`!` through union, to give: ```(null | { int data, X next }) & !null & !{ int data, X next } ``` Then, distribute `&` over `|`, to give: ```(null & !null & !{ int data, X next }) | ({ int data, X next } & !null & !{ int data, X next }) ``` At this point, it does indeed collapse down to `void`. Question: can we construct a subsumption example which doesn't work with simple rewrites? NOTE: in the above derivation we slightly cheated because I implicitly merged the two heads of the automata (i.e. `A_List` and `B_List`).
Member

### DavePearce commented Nov 7, 2016 • edited Edited 1 time DavePearce edited Nov 7, 2016 (most recent)

 Answer (to subsumption question): yes, I think so. Here is one: `A_Ref&!B_Ref` where we have: ```type A_Ref is &A_List type B_Ref is &B_List ``` The term `A_Ref & !B_Ref` is challenging because there are no local rewrites to apply. In particular, we cannot push intersections safely through references. That is, `&T1 & &T2` is `void` if `T1 != T2`, not `&(T1 & T2)`. A similar example may be possible with function types... Note: It's interesting to ponder the situation if we only had primitives and records. Perhaps in that special case, subsumption examples could never arise. If so, that suggests that reference types `&T` have a special property which necessitates non-local reasoning. Additional: Perhaps reference types break the properties required even in the non-recursive case? (i.e. the algorithm from the VMCAI paper).

Closed

Member

### DavePearce commented Nov 27, 2016 • edited Edited 1 time DavePearce edited Dec 1, 2016 (most recent)

 Some additional (re)reading: Covariance and Contravariance: a fresh look at an old issue, Giuseppe Castagna. PDF Semantic Subtyping for Imperative Object-Oriented Languages, Davide Ancona, Andrea Corradi. PDF Semantic Subtyping for Objects and Classes, Ornela Dardha, Daniele Gorla and Daniele Varacca. PDF Semantic Subtyping: Dealing Set-Theoretically with Function, Union, Intersection, and Negation Types, ALAIN FRISCH, et al. (This doesn't seem to address the question of how to simplify types into DNF?)

Closed

Member

### DavePearce commented Aug 29, 2017

 This is now resolved, with the new implementation of `CoerciveSubtypeOperator`.