Skip to content
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

Fix and improve contract generation optimization for static types #2017

Merged
merged 5 commits into from
Aug 6, 2024

Conversation

yannham
Copy link
Member

@yannham yannham commented Jul 30, 2024

Fixes #2014.

Motivation

This PR fixes a number of issues with the optimization of contract generation from a static type annotation. This optimization has been introduced to take advantage of the guarantees of static typing to simplify the generated contract and elide a number of useless checks at run-time.

However, the original optimization is too agressive: it turns any non-function type in a positive position to Dyn.

Contracts in negative position must be kept around, because they check what's come from the (potentially untyped) external world inside the function: the fact that a function is statically typed doesn't ensure it'll be called with the
right arguments. Basic contracts in positive position can be elided though: if a function has been statically checked to be of type Number -> Number, we know that it'll always return a Number at runtime, and we can simplify the contract to Number -> Dyn (which is further specialized to an implementation that doesn't check anything on the codomain). Alas, this isn't true for more complex types in positive positions.

Unsoundness

The first issue is that a type constructor in positive position can hide negative contracts inside. Typically, take let functions: Array (Number -> Number) in (std.array.at 0 functions) "a". The application is untyped, and wrongly passes a string to a function of the array. However, the current optimization will turn this contract to just Dyn at runtime and get rid of entirely, because there's an Array _ in positive position, and won't blame at runtime (might get a primop dynamic type error, or nothing, depending what exactly does the function). The elision is only valid if _ doesn't contain any arrow type, which it does, in this example.

Another issue stems from the sealing/unsealing symmetry of polymorphic row contracts. Take let id : forall r. {foo : Number; r} -> {foo : Number; r} = fun x => x in id {foo = 1, bar = 2}. The current version would return {foo = 1}, with the bar field missing. The issue is that the second {foo : Number; r} is a record type in positive position, which currently gets entirely elided, giving forall r. {foo : Number; r} -> Dyn as an optimized contract. The argument contract seals anything else than foo in the record's tail, but there's no dual contract to unseal it anymore, such that bar stays sealed in the tail forever and thus invisible.

This commit implements a more complicated strategy, but which is hopefully correct. Instead of getting rid of type constructor in positive positions, we try to simplify their content as well, and only if the content is simplified down to Dyn (or {; Dyn} for record rows, etc.), we get rid of the entire constructor. Otherwise, we try to pay only for the necessary checks. For example, {foo : Number, bar : Number -> Number} now gets simplified to {bar : Number -> Dyn; Dyn} instead of just Dyn before (which was incorrect).

The full simplification rules around polymorphic row contracts are a bit intricate and are detailed in the documentation of the corresponding methods.

@github-actions github-actions bot temporarily deployed to pull request July 30, 2024 15:21 Inactive
@github-actions github-actions bot temporarily deployed to pull request July 31, 2024 11:03 Inactive
This commit fixes a number of issues with the optimization of contract
generation from a static type annotation. It's been introduced to take
advantage of the guarantees of static typing to simplify the generated
contract and elide a number of useless checks at run-time.

However, this optimization was too agressive as implemented: it just
turned any non-function type in a positive position to `Dyn`. Indeed,
contracts in negative position must be kept around, because they check
what's come from the (potentially untyped) external world: the fact that
a function is statically typed doesn't ensure it'll be called with the
right arguments.

The first issue is that a negative contract can hide inside something
else than an arrow type. Typically, take `let functions: Array (Number
-> Number) in (std.array.at 0 functions) "a"`. The application is
untyped, and wrongly pass a string to a function of the array. However,
the current optimization code will turn this contract to just `Dyn` at
runtime and get rid of entirely, because there's an `Array _` in
positive position. This is only valid if `_` doesn't contain any arrow
type, which it does, in this example.

Another issue stems from the sealing/unsealing symmetry of polymorphic
row contracts. Take `let id : forall r. {foo : Number; r} -> {foo :
Number; r} = fun x => x in id {foo = 1, bar = 2}`. The current version
would return `{foo = 1}`, with the `bar` field missing. The issue is
that the second `{foo : Number; r}` is a record type in positive
position, which currently gets entirely elided, giving `forall r. {foo :
Number; r} -> Dyn` as an optimized contract. The argument contract seals
anything else than `foo` in the record's tail, but there's no dual
contract to unseal it anymore, such that it just becomes invisible.

This commit implements a more complicated strategy, but which is
hopefully correct. Instead of getting rid of type constructor in
positive positions, we try to simplify their content as well, and only
if the content is simplified down to `Dyn` (or `{; Dyn}` for record
rows, etc.), we get rid of the entire constructor. Otherwise, we try to
pay only for necessary checks. For example, `{foo : Number, bar : Number
-> Number}` now gets simplified to `{bar : Number -> Dyn; Dyn}` instead
of just `Dyn` before (which was incorrect).

The full simplification rules around polymorphic row contracts are a bit
intricate and are properly detailed in the documentation of the
corresponding methods.
@yannham yannham force-pushed the fix/polymorphic-rows-tail-disappears branch from c2e36b4 to 82d7d71 Compare August 1, 2024 09:22
@github-actions github-actions bot temporarily deployed to pull request August 1, 2024 09:25 Inactive
Copy link
Contributor

github-actions bot commented Aug 1, 2024

🐰Bencher

ReportTue, September 10, 2024 at 09:02:44 UTC
Projectnickel
Branch2017/merge
Testbedubuntu-latest

⚠️ WARNING: The following Measure does not have a Threshold. Without a Threshold, no Alerts will ever be generated!

  • Latency (latency)

Click here to create a new Threshold
For more information, see the Threshold documentation.
To only post results if a Threshold exists, set the --ci-only-thresholds CLI flag.

Click to view all benchmark results
BenchmarkLatencyLatency Results
nanoseconds (ns)
fibonacci 10➖ (view plot)486,120.00
pidigits 100➖ (view plot)3,129,800.00
product 30➖ (view plot)794,220.00
scalar 10➖ (view plot)1,472,500.00
sum 30➖ (view plot)786,110.00

Bencher - Continuous Benchmarking
View Public Perf Page
Docs | Repo | Chat | Help

@yannham yannham requested a review from jneem August 1, 2024 09:35
@yannham yannham marked this pull request as ready for review August 1, 2024 09:36
@yannham yannham added this to the Next minor (1.8) milestone Aug 5, 2024
@yannham
Copy link
Member Author

yannham commented Aug 5, 2024

@jneem if you have a chance to take a look - I'd like to include this in the 1.8 release (given the severity of the bug that is fixed)

core/src/typ.rs Outdated Show resolved Hide resolved
core/src/typ.rs Outdated Show resolved Hide resolved
core/src/typ.rs Outdated Show resolved Hide resolved
core/src/typ.rs Outdated Show resolved Hide resolved
core/src/typ.rs Outdated Show resolved Hide resolved
core/stdlib/internals.ncl Outdated Show resolved Hide resolved
Co-authored-by: jneem <joeneeman@gmail.com>
@github-actions github-actions bot temporarily deployed to pull request August 5, 2024 16:39 Inactive
@github-actions github-actions bot temporarily deployed to pull request August 5, 2024 16:45 Inactive
@yannham yannham added this pull request to the merge queue Aug 6, 2024
Merged via the queue into master with commit 2754065 Aug 6, 2024
6 checks passed
@yannham yannham deleted the fix/polymorphic-rows-tail-disappears branch August 6, 2024 14:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Record row polymorphism can be destructive
2 participants