-
Notifications
You must be signed in to change notification settings - Fork 90
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
Contract elision for static types #1671
Merged
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jneem
approved these changes
Oct 9, 2023
Co-authored-by: jneem <joeneeman@gmail.com>
yannham
force-pushed
the
optimization/contract-elision
branch
from
October 10, 2023 08:02
7d2622c
to
4561e88
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Context
As part of #1622, metrics show that the base used for benchmarks is performing an awful lot of array contract applications and their derived subcontracts, in particular polymorphic contracts. This is probably due to the usage of stdlib functions, which are all typed with a polymorphic type.
Indeed, consider
std.record.map
, whose type isforall a b. (a -> b) -> Array a -> Array b
. If we apply it to a 5000 elements array, this will cause the execution of 20 000 small contracts: one to seal all elements of the array argument witha
, one to unseal the same elements whenf
is applied (corresponding to_a_ -> b
), one sealing the result of the application tob
(theb
ina -> _b_
), and finally one that will map the unsealing key over the resulting array.What's sad is that the function is statically typechecked. Thus, under the assumption that the type system is reasonably behaved (blame safety), the polymorphic contract can never blame. In the same spirit, it's not useful to check anything on the return value of the function: the typechecker already proves that it must be
Array b
.I discussed contract elision rules in #285, which is a bit different, but related. This PR follows the same idea overall: use the guarantees of the static type system to elide some of the dynamic checks.
Content
This PR applies the following rewriting when generating the contract coming from a static type annotation:
forall
in positive position are removed, and their bound variable is substituted forDyn
. That is,forall a b. (a -> b) -> Array a -> Array b
is rewritten to(Dyn -> Dyn) -> Array Dyn -> Array Dyn
.Dyn
as well. Indeed, according to blame safety, a well-typed function can never be blamed, thus positive occurrences of contracts can never fail. For map, we get after this second transformation(Dyn -> Dyn) -> Array Dyn -> Dyn
Those optimizations are coupled with the following specializations, which aren't restricted to static type annotations:
Dyn -> Dyn
is specialied tofunc_dyn
,Dyn -> T
tofunc_dom T
, etc. That is, the general function contract is specialized when the domain, the codomain or both areDyn
, to eschew useless checks.Array Dyn
is specialized to a constant-time contract$array_dyn
which just checks that its argument is an array (indeed,$array $dyn
maps$dyn
and is thus linear time - not when applied, thanks to lazy array contracts, but still when the array is finally forced){_ : Dyn}
and{_ | Dyn}
are specialized to$dict_dyn
.Those two changes combined give even better results: once the type has been rewritten, many specialized version of builtin contracts can be used. On our
map
example, the final contract becomes$func $func_dyn ($func_dom $array_dyn)
. This contract only checks that the first argument tomap
is a function and the second is an array, all in constant time. From4n
contract checks, we are now consistently applying 3 checks (we still check thatmap
is a function, which is useless - but it's not very important and can be improved upon later).Result
Tested on the codebase of #1622, this gave a consistent 50% reduction in running time, which is encouraging. I will test it on kav (#1667) as well.