Add a type parameter to TypeF for contracts #2078
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
The TypeF recursion scheme is parametrized by a number of types: the type of Nickel types, the type of enum rows and the type of record rows. There is one more Rust type that can be stored in a TypeF: a contract. It's currently hardcoded to be a `RichTerm`, which is fine because we never want to use another Rust type to store something else With the development of the experimental bytecode interpreter, we are changing the representation of terms. Because we want to keep mailine Nickel operational during the transition, we have to copy paste all the `typ` module somewhere else, replacing `RichTerm` with the type of the new AST. There is an alternative: as `TypeF` is already parametrized by a bunch of things, why not also parametrize the type of what's stored inside `TypeF::Contract`? This adds a bit more complexity, and requires an additional closure when mapping on or recursing into a `Type`. But the price doesn't seem too big. There is an unexpected benefit: in fact, we do store something else than a `RichTerm`! During typechecking, we need to store an additional environment alongside a contract in order to properly compute contract equality. This led to having an additional constructor `GenericUnifType::Contract`, that must be handled separately than concrete types. When converting from a `Type` to a `UnifType`, the node `TypeF::Flat` is converted to`GenericUnifType::Contract`, and all typechecking functions then assume the invariant that they will never encounter a `TypeF::Flat`. But the Rust type system can't guarantee it. There's also a bespoke runtime error for that (although we're pretty sure it can't happen), a bunch of `debug_assert`, etc. We can in fact kill two birds with one stone: by parametrizing `TypeF`, we can now instantiate it with `(RichTerm, Environment)` for unification types. No need for runtime invariants or ad-hoc treatment anymore. Doing so, we also rename `TypeF::Flat` to `TypeF::Contract`, the latter being a historical but bad name.
|
Bencher Report| Branch | 2078/merge |
| Testbed | ubuntu-latest |
⚠️ WARNING: The following Measure does not have a Threshold. Without a Threshold, no Alerts will ever be generated!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-thresholdsCLI flag.
Click to view all benchmark results
| Benchmark | Latency | nanoseconds (ns) |
|---|---|---|
| fibonacci 10 | 📈 view plot | 486,400.00 |
| foldl arrays 50 | 📈 view plot | 1,697,700.00 |
| foldl arrays 500 | 📈 view plot | 6,655,300.00 |
| foldr strings 50 | 📈 view plot | 7,044,900.00 |
| foldr strings 500 | 📈 view plot | 62,522,000.00 |
| generate normal 250 | 📈 view plot | 44,732,000.00 |
| generate normal 50 | 📈 view plot | 2,083,700.00 |
| generate normal unchecked 1000 | 📈 view plot | 3,367,300.00 |
| generate normal unchecked 200 | 📈 view plot | 756,840.00 |
| pidigits 100 | 📈 view plot | 3,217,500.00 |
| pipe normal 20 | 📈 view plot | 1,509,600.00 |
| pipe normal 200 | 📈 view plot | 10,409,000.00 |
| product 30 | 📈 view plot | 825,310.00 |
| scalar 10 | 📈 view plot | 1,519,200.00 |
| sum 30 | 📈 view plot | 823,440.00 |
jneem
approved these changes
Oct 24, 2024
| @@ -1678,15 +1657,16 @@ fn walk_type<V: TypecheckVisitor>( | |||
| // Currently, the parser can't generate unbound type variables by construction. Thus we | |||
| // don't check here for unbound type variables again. | |||
| | TypeF::Var(_) | |||
| // An enum type can't contain a flat type inside. | |||
| // An enum type can't contain a contract. | |||
| // TODO: the assertion above isn't true anymore (ADTs). Need fixing? | |||
There was a problem hiding this comment.
$ nickel typecheck <<< "[| 'Foo (5 : String) |]"
$ # OKYup, needs fixing 🙃
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.
The TypeF recursion scheme is parametrized by a number of (Rust) types: the type of Nickel types, the type of enum rows and the type of record rows. There is one more Rust type that can be stored in a TypeF: a contract. It's currently hardcoded to be a
RichTerm, which is fine because we never want to use another Rust type to store something elseWith the development of the experimental bytecode interpreter, we are changing the representation of terms. Because we want to keep mailine Nickel operational during the transition, we have to copy paste all the
typmodule somewhere else, replacingRichTermwith the type of the new AST.There is an alternative: as
TypeFis already parametrized by a bunch of things, why not also parametrize the type of what's stored insideTypeF::Contract? This adds a bit more complexity, and requires an additional closure when mapping on or recursing into aType. But the price doesn't seem too high, and we can reuse the same implementation for both mainline Nickel and bytecode Nickel.There is an unexpected benefit: in fact, we do store something else than a
RichTerm! During typechecking, we need to store an additional environment alongside a contract in order to properly compute contract equality. This led to having an additional constructorGenericUnifType::Contract, that must be handled separately from concrete types. When converting from aTypeto aUnifType, the nodeTypeF::Flatis converted toGenericUnifType::Contract, and all typechecking functions then assume the invariant that they will never encounter aTypeF::Flat. But the Rust type system can't guarantee it. There's also a bespoke runtime error for that (although we're pretty sure it can't happen), a bunch ofdebug_assert, etc.We can thus kill two birds with one stone: by parametrizing
TypeF, we can now instantiate it with(RichTerm, Environment)for unification types. No need for runtime invariants or ad-hoc treatment anymore.Doing so, we also rename
TypeF::FlattoTypeF::Contract, the former being a historical but bad name.