Add disjointness reasoning for BbML #260
Conversation
|
|
||
|
|
||
| fun annohelper: Region[outer] ->{outer} @outer Pair[out Ref[Int, out outer], out Ref[Int, out Any]] | ||
| fun annohelper: [outer, T extends outer] -> Region[T] ->{T} Pair[out Ref[Int, out T], out Ref[Int, out Any]] |
There was a problem hiding this comment.
A more natural signature could be
| fun annohelper: [outer, T extends outer] -> Region[T] ->{T} Pair[out Ref[Int, out T], out Ref[Int, out Any]] | |
| fun annohelper: [outer, T] -> Region[T] ->{T | outer} Pair[out Ref[Int, out T], out Ref[Int, out outer]] |
Does it work? If it does, it would be good to add it to the test file (in addition to the existing one).
There was a problem hiding this comment.
No, it doesn't. We can only track the evidence that r2 <: ~outer, but not r2 <: ~T. So this code will be rejected.
There was a problem hiding this comment.
Why would we need r2 <: ~T here?
There was a problem hiding this comment.
The disjointness requirement is (T | outer) & r2 <: bot, i.e., (T & r2) | (outer & r2) <: bot. Then only the second subterm (outer & r2) <: bot can be solved. The equivalent one should be T & outer instead.
|
|
||
|
|
||
| fun annohelper: Region[outer] ->{outer} @outer Pair[out Ref[Int, out outer], out Ref[Int, out Any]] | ||
| fun annohelper: [outer, T extends outer] -> Region[T] ->{T} Pair[out Ref[Int, out T], out Ref[Int, out Any]] |
There was a problem hiding this comment.
Why do we have Any in Ref[Int, out Any]?
There was a problem hiding this comment.
Because the second reference returned by fork is located in r2. It is extruded after we leave the scope of r2. But it can be written as out ~outer.
There was a problem hiding this comment.
Yes, ~outer is what I meant in my other comment.
|
BTW, since you are modifying the way forall types are printed. Why not print them like in the source? Eg |
outervariables forfunctionspolymorphic typesThis PR is still being prepared, e.g., containing redundant code. Such problems will be addressed after the main problems are discussed in the meeting.