flix
feat: add safe upgrade check
Adds the isSafe predicate.
Related to https://github.com/flix/flix/issues/9525 Related to https://github.com/flix/flix/issues/11436 Related to https://github.com/flix/flix/issues/9524 Related to https://github.com/flix/flix/pull/9730
@magnus-madsen tentative review? I still need add tests and such but so far this is what I have adapted from the old implementation.
EDIT: I just want to make sure that it seem sensible so far.
Looks alright to me. I believe the code represents what we want to check, and the tests cover what I would expect. A minor note, I would really like for the test names to actually describe what is being tested — which property? I am mostly concerned that if anyone has to change this in the future they have to spend extra time discerning what is failing.
I have made the isSubset predicate recursively defined which holds in the case for concrete types but not for polymorphic return types. Intuitively it should hold that if "you can do less than before" then it is okay.
I will use the names original and upgrade for types that first have type original and is then upgraded to upgrade.
Consider the types
original : (Int32 -> Int32 \ {A, B, C}) -> Int32 -> Int32 \ {A, B, C}
upgrade : (Int32 -> Int32 \ {A, B}) -> Int32 -> Int32 \ {A, B, C}
This upgrade should be fine since we can construct the same transcript regardless of the upgraded type:
def f(g: Int32 -> Int32 \ {A, B}, x: Int32) Int32 \ {A, B, C} =
if (false)
g(x)
else
// do A, B, C effects
0
Note that the definition of f will result in the same transcript even if g has effects {A, B, C}.
Now consider the types
original : (a -> Int32 \ {A, B, C}) -> a -> Int32 \ {A, B, C}
upgrade : (a -> Int32 \ {A, B}) -> a -> Int32 \ {A, B, C}
We can do the same trick again:
def f(g: a -> Int32 \ {A, B}, x: a) Int32 \ {A, B, C} =
if (false)
g(x)
else
// do A, B, C effects
0
But now consider the types
original : (a -> b \ {A, B, C}) -> a -> b \ {A, B, C}
upgrade : (a -> b \ {A, B}) -> a -> b \ {A, B, C}
There is no way to construct an element of type b unless we have the witness (a -> b \ {A, B}). Yes, we can have the effect set {A, B, C} in the return type but not without using g which changes the transcript after the upgrade since it does strictly less than before. However, my "hope" is that this last case should be okay to upgrade to even though we cannot construct a proof. Why? In the original version, it could perform any of {A, B, C}, however, it wanted in addition to the {A, B, C} inherited by the lambda. In the upgrade version it still performs the {A, B, C} as before but only inherits {A, B} which is still strictly less than before. This is what the recursive definition allows. Note that we can define the function as
def f(g: a -> b \ {A, B}, x: a): b \ {A, B, C} =
// do A, B, C effects
g(x)
Lastly, how does this interact with effect variables?
original : (a -> b \ {A, B, C, ef}) -> a -> b \ {A, B, C, ef}
upgrade : (a -> b \ {A, B, ef}) -> a -> b \ {A, B, C, ef}
This should be fine by the same token as above since it just means that the lambda is invoked (not necessarily on a reachable path) but there is no way to obtain ef without doing so. Additionally, it is still free to perform {A, B, C} with and without the lambda.
original : (a -> b \ {A, B, C, ef}) -> a -> b \ {A, B, C, ef}
upgrade : (a -> b \ {A, B, C}) -> a -> b \ {A, B, C}
This does still not allow the function to ignore the lambda since there is no way to construct an element of b without it, and it is still free to perform {A, B, C} regardless of the lambda.
Lastly, note that the following cannot happen since the types are no longer equal (which would allow it to completely ignore the lambda):
original : (a -> Int32 \ {A, B, C, ef}) -> a -> Int32 \ {A, B, C, ef}
upgrade : (a -> Int32 \ {A, B, C}) -> a -> Int32 \ {A, B, C}
Maybe for now the correct approach is to use a definition that 100% satisfies the formal definition (i.e., no recursive relation) and then later we can see if can add more flexibility by extending it this way.
@jaschdoc @AStenbaek Does this implement exactly what is in the paper? No more, and no less?
Can both of you also take a look at Scheme.lessThanEqual and tell me if it is relevant/related.
Can both of you also take a look at
Scheme.lessThanEqualand tell me if it is relevant/related.
It seems relevant. IIRC, we used Scheme.equal in the last prototype, so indirectly we also used Scheme.lessThanEqual. Why are we not able to use lessThanEqual for the upgrade relation (i.e., the upgrade must be less than or equal to the old version)? @AStenbaek
EDIT: I'm not actually sure we can use Scheme.lessThanEqual since we want equality for all types except the effect sets (we also just used == to check equality of types, not Scheme.lessThanOrEqual).
The current version implements exactly the relation in the paper. It seems, however, that we should be able to use Scheme.leq for the effect subset check. That would hopefully also allow parameters to decrease in effects.
Should we add the ignored tests as negative tests? This version intentionally does not handle changes in the parameters (in the subset relation).
Should we add the ignored tests as negative tests? This version intentionally does not handle changes in the parameters (in the subset relation).
What do you mean? Sorry I don't understand.
@AStenbaek Also see if you can answer the question about Scheme.isLessEqual.
In relation to Scheme.leq. It looks to me like this is the relation we want in the generalize rule. I am not convinced this will work for subset, at least when we have base-effects, since it looks to me like this function is about instantiating variables, but I may be wrong.