{"action":"created","issue":{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/697","repository_url":"https://api.github.com/repos/Whiley/WhileyCompiler","labels_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/697/labels{/name}","comments_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/697/comments","events_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/697/events","html_url":"https://github.com/Whiley/WhileyCompiler/issues/697","id":187623117,"number":697,"title":"Can we replace SubtypeOperator?","user":{"login":"DavePearce","id":484459,"avatar_url":"https://avatars.githubusercontent.com/u/484459?v=3","gravatar_id":"","url":"https://api.github.com/users/DavePearce","html_url":"https://github.com/DavePearce","followers_url":"https://api.github.com/users/DavePearce/followers","following_url":"https://api.github.com/users/DavePearce/following{/other_user}","gists_url":"https://api.github.com/users/DavePearce/gists{/gist_id}","starred_url":"https://api.github.com/users/DavePearce/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DavePearce/subscriptions","organizations_url":"https://api.github.com/users/DavePearce/orgs","repos_url":"https://api.github.com/users/DavePearce/repos","events_url":"https://api.github.com/users/DavePearce/events{/privacy}","received_events_url":"https://api.github.com/users/DavePearce/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-11-07T04:29:01Z","updated_at":"2016-11-07T04:37:22Z","closed_at":null,"body":"We now know that `SubtypeOperator` is very broken and causes many problems.  \r\n\r\n**The question is**: _can we replace it?_  Or, to put it another way: _do we know the algorithm for implementing subtyping in Whiley_?\r\n\r\nAt this stage, I'm not completely sure that we do (though @richdougherty has been making progress).  Here are related discussions:\r\n\r\n- #645 --- Dealing with uninhabited and non-contractive types.\r\n\r\n- #678 --- Thoughts on simplifying types.\r\n\r\n- #619 --- A good (though incomplete) list of simplification rules.\r\n\r\nIn #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:\r\n\r\n- **Equivalence**.  Determining that two recursive types are, in fact, equivalent.  This is problematic in the case of equivalent types with different amounts of unrolling.\r\n\r\n- **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).\r\n\r\nConsidering the equivalence problem, consider these two types in Whiley:\r\n<pre>\r\ntype A_List is null | { int data, A_List next }\r\ntype B_List is null | { int data, null | { int data, B_List next } next }\r\n</pre>\r\n\r\nThese 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.\r\n\r\nAs an example of the subsumption problem, consider these:\r\n<pre>\r\ntype A_List is null | { int data, A_List next }\r\ntype B_List is null | { any data, B_List next }\r\n</pre>\r\n\r\nNow, 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.\r\n<pre>\r\n(null | { int data, X next }) & !(null | { int data, X next })\r\n</pre>\r\n\r\nPush`!` through union, to give:\r\n\r\n<pre>\r\n(null | { int data, X next }) & !null & !{ int data, X next }\r\n</pre>\r\n\r\nThen, distribute `&` over `|`, to give:\r\n\r\n<pre>\r\n(null & !null & !{ int data, X next }) | ({ int data, X next } & !null & !{ int data, X next })\r\n</pre>\r\n\r\nAt this point, it does indeed collapse down to `void`.\r\n\r\n**Question:** _can we construct a subsumption example which doesn't work with simple rewrites?_\r\n\r\n**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`)."},"comment":{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/comments/258745731","html_url":"https://github.com/Whiley/WhileyCompiler/issues/697#issuecomment-258745731","issue_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/697","id":258745731,"user":{"login":"DavePearce","id":484459,"avatar_url":"https://avatars.githubusercontent.com/u/484459?v=3","gravatar_id":"","url":"https://api.github.com/users/DavePearce","html_url":"https://github.com/DavePearce","followers_url":"https://api.github.com/users/DavePearce/followers","following_url":"https://api.github.com/users/DavePearce/following{/other_user}","gists_url":"https://api.github.com/users/DavePearce/gists{/gist_id}","starred_url":"https://api.github.com/users/DavePearce/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DavePearce/subscriptions","organizations_url":"https://api.github.com/users/DavePearce/orgs","repos_url":"https://api.github.com/users/DavePearce/repos","events_url":"https://api.github.com/users/DavePearce/events{/privacy}","received_events_url":"https://api.github.com/users/DavePearce/received_events","type":"User","site_admin":false},"created_at":"2016-11-07T04:37:22Z","updated_at":"2016-11-07T04:37:22Z","body":"**Answer** (to subsumption question): _yes, I think so_.  Here is one: `A_Ref&!B_Ref` where we have:\r\n\r\n<pre>\r\ntype A_Ref is &A_List\r\ntype B_Ref is &B_List\r\n</pre>\r\n\r\nThe 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."}}
{"actor":{"display_login":"DavePearce"}}