-
Notifications
You must be signed in to change notification settings - Fork 14
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Constraints #105
Comments
Here's a realistic example that generates some non-trivial constraints. For the following I'll assume that I also need some array comprehension syntax. I'm not sure whether that has been discussed before, but I mean something like:
where
Constraints are generated by a bounds-check rule:
This rule generates two constraints. I've used the "models" turnstile rather than "proves" for such constraints; this is meant to indicate that we aren't proving the claims within this proof system, but we still expect them to be true (and we will later check that with constraint solving or checking). Here's the code, which constructs an array from an existing one, with the elements in reverse order.
A proof of type correctness is as follows. Let
The use of the BOUND rule generates two constraints, marked with (*). It's fairly easy to see that both are true, given that After that is a fairly typical use of the APP rule. The MINUS-INT rule is just the axiom giving the signature of (-). The SUB and RANGE-* rules are more interesting, because we have that n:{0..} but we need n:{..}. SUB invokes the subtype relation, and RANGE-LB1 lets us essentially remove a lower bound that we don't need. Similarly, we can also remove an upper bound we don't need (leaving the other bound in place) using RANGE-UB2 and connecting the two subtyping steps with TRANS. This example also shows that there is no real chicken-and-egg problem with the use of {..} as an argument to its own bounds. The problem is in trying to describe
|
As regards the solving of these constraints, we could try using a third party solver of some sort or try to find some way ourselves. Unfortunately, bounds propagation where variables may appear in the bounds doesn't work well in the case that a variable is multiplied by something whose sign is indeterminate. The reason for this is that we can't tell whether the upper and lower bounds should swap places or not due to the multiplication, and we can't find out by comparing things immediately because we are dealing with variables not numbers. In the case of linear formulas, or formulas involving non-negative integers, we can apply the bounds propagation method. That is the case above, where we generated the following constraints:
Since
which in turn becomes
which simplifies to
which is true because
the final step of which is true because |
As another example we can look at append. I'll define another new construct for this, similar to an if-then-else:
The new construct, We can then define:
The constraints we would generate when type checking the array accesses are:
We can solve these using the method above, after adjusting the range of |
A more detailed example of solving. This function returns a segment of an array starting at a given position and with a given length. The dependent argument types allow us to ensure this function is total.
This time we get the constraint
where This one is interesting to solve because we need to eliminate more than one variable. We do this in dependency order - first We first eliminate
Then we do the same for
The second part of this turns into
So this constraint is also true. |
At some point we're going to encounter constraints that aren't part of the type of any individual value, like this example:
In some cases these can be reformulated into individual types, but this can make their expression less straightforward and is not always possible.
Nevertheless, we should probably avoid diving headlong into constraint solvers until we have some very compelling motivating examples.
The text was updated successfully, but these errors were encountered: