Repository navigation
Support comparing and subtyping of recursive types - #3610
Conversation
|
|
||
| struct TypeComparator { | ||
| std::unordered_set<std::pair<HeapType, HeapType>> cache; | ||
| bool cmp(Type a, Type b); |
There was a problem hiding this comment.
Please add a comment explaining what the resulting bools here mean.
Lower down I see a call to this replaces bool HeapType::operator< so perhaps this could be operator< or be called lessThan?
| return false; | ||
| } | ||
| cache.insert({a, b}); | ||
| return cmp(*getHeapTypeInfo(a), *getHeapTypeInfo(b)); |
There was a problem hiding this comment.
I'm not sure I follow what cache does. Trying to understand from the code, on the one hand if (x,y) are in the cache then we return true. However right here we insert (x,y) into the cache regardless of the result, that is, we may end up returning false. So it is not purely caching the function result - is that right?
There was a problem hiding this comment.
Oh, I think I see, it's not a cache of the results, but a recursion guard. Perhaps cache => seen?
Also a comment on the return when something is found in cache/seen could explain why the result does not matter in that case. It's not immediately obvious to me why the result is deterministic in that case.
There was a problem hiding this comment.
Yeah, sorry, this code could use more comments in general. Will fix it up.
| return false; | ||
| } | ||
| cache.insert({a, b}); | ||
| return cmp(*getHeapTypeInfo(a), *getHeapTypeInfo(b)); |
There was a problem hiding this comment.
Oh, I think I see, it's not a cache of the results, but a recursion guard. Perhaps cache => seen?
Also a comment on the return when something is found in cache/seen could explain why the result does not matter in that case. It's not immediately obvious to me why the result is deterministic in that case.
|
It looks like I will have to handle printing recursive types in this PR as well if I want the test suite to pass. Marking draft for now while I work on that. |
|
@kripken I addressed your comments and added support for recursive type names so that the CI would pass. I'm not sure that last part is actually necessary after your related work on getting types into the name section, though. |
When the type section is emitted, types with an equal amount of references are ordered by an arbitrary measure of simplicity, which previously would infinitely recurse on structurally equivalent recursive types. Similarly, calculating whether an recursive type was a subtype of another recursive type could have infinitely recursed. This PR avoids infinite recursions in both cases by switching the algorithms from using normal inductive recursion to using coinductive recursion. The difference is that while the inductive algorithms assume the relations do not hold for a pair of HeapTypes until they have been exhaustively shown to hold, the coinductive algorithms assume the relations hold unless a counterexample can be found. There are additional algorithms that will need to be switched from inductive to coinductive recursion, such as the type name generation and least upper bound generation, but these two presented a good starting point and are sufficient to get some interesting programs working end-to-end. Also includes small drive-by cleanups in some related code.
de72fd9 to
49eb543
Compare
|
Rebased on top of the related work, which did indeed make the name generation stuff unnecessary. But since I already had it written, I updated the lit test to not have any type names to have it test the name generation instead. |
When the type section is emitted, types with an equal amount of references are
ordered by an arbitrary measure of simplicity, which previously would infinitely
recurse on structurally equivalent recursive types. Similarly, calculating
whether an recursive type was a subtype of another recursive type could have
infinitely recursed. This PR avoids infinite recursions in both cases by
switching the algorithms from using normal inductive recursion to using
coinductive recursion. The difference is that while the inductive algorithms
assume the relations do not hold for a pair of HeapTypes until they have been
exhaustively shown to hold, the coinductive algorithms assume the relations hold
unless a counterexample can be found.
There are additional algorithms that will need to be switched from inductive to
coinductive recursion, such as
the type name generation andleast upper boundgeneration, but these two presented a good starting point and are sufficient to
get some interesting programs working end-to-end.
Also includes small drive-by cleanups in some related code.