Add record constructor to subtyping #2007

Eckaos · 2024-07-25T12:22:54Z

No description provided.

Eckaos · 2024-07-25T12:31:44Z

@yannham What I did here is pretty much unify for record rows. It miss TailVar, Constant, etc...
Do you know how to reconstruct a GenericUnifType from GenericUnifRecordRows. For the time being, I reconstruct it from the data I have. I may have reconstruct the type with the wrong levels.

yannham · 2024-07-25T13:18:21Z

core/src/typecheck/unif.rs

@@ -1599,7 +1599,7 @@ impl Unify for UnifRecordRows {
 }

 #[derive(Clone, Copy, Debug)]
-enum RemoveRowError {
+pub enum RemoveRowError {


Is there a reason to make this symbol public? Public means that it's accessible to other crates. I think most of those symbols are specific to nickel-lang-core, or even to typecheck.

In the mod.rs file, rust does not know what is RemoveRowError. It says it is not accessible.

In which file? typecheck/mod.rs?

Right, because it's a parent of unif. Then you can use pub(super) instead of pub, which is more restricted and doesn't make this a public symbol of nickel-lang-core. The latter has more consequences, because it means it impacts e.g. semantic versioning (if we change the name of this trait, it's a breaking change). While it stays internal, we can do whatever we want 🙂

yannham · 2024-07-25T13:25:52Z

Do you know how to reconstruct a GenericUnifType from GenericUnifRecordRows.

The best, if those record rows are coming from destructuring a unif type to begin with, is to keep the original var_levels around so that you can reconstruct the original type.

If this type is modified, or generated, or coming from some type inference transformation, you can just use UnifType::concrete (or GenericUnifType::concrete), the method with a lowercase c (and not the constructor Concrete), which takes care of updating and filling the levels accordingly.

Eckaos · 2024-07-26T16:37:48Z

The commit 58af17d break stuff about record.
Left to do :

Comments
Fix the problem about records
Fix warning

Eckaos · 2024-07-31T16:12:34Z

The problem about records wasn't real, it was just a simple problem about reporting error correctly.
Another problem arose. It is about lsp/nls/tests/inputs/hover_field_typed_block_regression_1574.ncl, it give a new snapshot and I don't know why. @yannham

If my fix does work, the work left to do is to :

Add documentation
Update comments
Add tests
Remove subsumption function in typecheck/mod.rs

yannham

As a first review, the approach looks good. We can think about how to de-depulicate the code between subsume and unify later on. Maybe the code comments still need to be put at the right place and updated a bit, they've been mostly copy pasted or so it seems.

core/src/typecheck/subtyping.rs

Eckaos · 2024-08-05T10:35:17Z

To de-duplicate the code between is_subsumed_by and unify, we can just call unify where we need in is_subsumed_by. The cost, I see, will be the cost of pattern matching + function call (depends on what optimization the rust compiler will do). Or we could abstract cases that are the same in is_subsumed_by and unify into another function. The cost, I see here, will be pattern matching + function call in the two functions (depends on what optimization the rust compiler will do). @yannham

yannham · 2024-08-05T12:23:31Z

To de-duplicate the code between is_subsumed_by and unify, we can just call unify where we need in is_subsumed_by.

I'm not sure to understand what you mean here. For example, when subsuming record types, we do the same general work but we still recursively calls is_subsumed_by on each component, so we can't just replace the whole case by a call to unify. Indeed, I think we need to have a core function that is generic how it calls itself recursively. It's certainly doable, but we can do that in a second step.

P.S: it could be good to have tests for more complicated record types: types with tails, record types with subsumption acting on several components, etc.

Eckaos · 2024-08-06T11:40:46Z

I was talking about cases where we do exactly the same work (with Constant and UnifVar etc...). In those cases, we can call unify from is_subsumed_by.
The other alternative was to factor out a function which does only cases where it is the same result for unify and is_subsumed_by and then call it from unify and is_subsumed_by when needed.

…en there is a record/dictionary subsumption)

Co-authored-by: Yann Hamdaoui <yann.hamdaoui@gmail.com>

github-actions · 2024-08-06T13:33:40Z

Bencher

Report	Fri, September 6, 2024 at 15:27:59 UTC
Project	nickel
Branch	2007/merge
Testbed	ubuntu-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

Benchmark	Latency	Latency Results nanoseconds (ns)
fibonacci 10	➖ (view plot)	504,530.00
pidigits 100	➖ (view plot)	3,192,200.00
product 30	➖ (view plot)	796,650.00
scalar 10	➖ (view plot)	1,496,400.00
sum 30	➖ (view plot)	793,290.00

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

Eckaos · 2024-08-07T14:04:22Z

I don't understand why cargo and the continuous integration pipeline give me an error about the lsp. @yannham

jneem · 2024-08-07T14:09:13Z

It's because the lsp snapshot tests have changed -- you've changed docs in the stdlib and so the hover text in the lsp is different. Running cargo test -p nickel-lang-lsp and cargo insta review locally should let you update the snapshots.

yannham · 2024-08-07T16:19:16Z

It's because the lsp snapshot tests have changed -- you've changed docs in the stdlib and so the hover text in the lsp is different. Running cargo test -p nickel-lang-lsp and cargo insta review locally should let you update the snapshots.

I don't see any change to the stdlib. Also, the diff of the snapshot is dubious - we now get an additional monomorphic type with _a coming first in the LSP output. So it seems this PR has changed something related to either how TypecheckVisitor is called, or to the apparent type of values, etc.

yannham

Overall looks good, but the LSP regression is suspicious.

core/src/typecheck/subtyping.rs

yannham · 2024-08-08T17:06:28Z

core/src/typecheck/subtyping.rs

+//! Type subsumption
+/// Type subsumption is generally used when we change from inference mode to checking mode.


Suggested change

//! Type subsumption

/// Type subsumption is generally used when we change from inference mode to checking mode.

//! Type subsumption

//!

/// Type subsumption is generally used when we change from inference mode to checking mode.

yannham · 2024-08-08T17:06:53Z

core/src/typecheck/subtyping.rs

@@ -0,0 +1,244 @@
+//! Type subsumption
+/// Type subsumption is generally used when we change from inference mode to checking mode.
+/// Currently, there is one subtyping relations :


Here, and below, you should continue to use //! instead of ///, because it's part of the top-level module documentation.

doc/manual/typing.md

...ts/snapshots/main__lsp__nls__tests__inputs__hover_field_typed_block_regression_1574.ncl.snap

Co-authored-by: Yann Hamdaoui <yann.hamdaoui@gmail.com>

yannham · 2024-09-05T16:22:58Z

I'm taking over this PR for the foreseeable future, unless @Eckaos thinks he has the time to bring it down the finish line.

This commit performs minor cosmetic improvements in the code handling subtyping, mostly around comments and function interfaces.

The support of subtyping for record types makes some types to be instantiated earlier than before. Given the way terms are visited, when writing something like `let f = std.array.map in ..`, `std.array.map` used to be inferred to be of a polymorphic type `forall a b. ...` and then only was instantiated (because record access is inferred, while the bound expression is checked). With the new implementation, it is instantiated as part of the subsumption rule, meaning that it'll appear differently on the LSP. All in all, both version of the data shown by the LSP (before this change and after) are meaningful, in some sense. The polymorphic type is still shown when it's part of the metadata anyway, in addition to the inferred monomorphic type. This also doesn't change which expressions are accepted or not. It's more of an artifact of when we visit terms, before or after instantiation and how those visits are intertwined with `check` and `infer`. It's not easy to revert to the previous state of affairs, and it's in fact not necessarily a good thing either: in the example above, the LSP would also show a polymorphic type for `f` - the one of `map` - while in fact `f` has a monomorphic type, so you couldn't use it in different contexts (say on an `Array Number` and later on a `Array String`). The current version is showing the real monomorphic nature of `f`.

yannham · 2024-09-06T15:20:12Z

After some thorough investigation, I think I understand what's happening and I convinced myself that it makes sense (although in the test case it adds a bit of noise, it's also more correct in some cases - see the commit message). It an artifact of when we visit the term compared to when the types are instantiated, more or less.

yannham reviewed Jul 25, 2024

View reviewed changes

Eckaos requested a review from yannham July 31, 2024 16:17

yannham reviewed Aug 1, 2024

View reviewed changes

core/src/typecheck/subtyping.rs Outdated Show resolved Hide resolved

core/src/typecheck/subtyping.rs Outdated Show resolved Hide resolved

Eckaos marked this pull request as ready for review August 6, 2024 13:19

Eckaos and others added 13 commits August 6, 2024 15:23

Initial draft without Constant and TailVar

da2e4af

Restrict visibility of RemoveErrorRow to super

5897969

Create trait Subsume for UnifType and UnifRecordRows

186ca8d

Fix problem about {a: Type}<: {a:Type;b:Type} that was not accepted

f795609

Copy comments (general comment on subsumption and closing a record wh…

4c74bb6

…en there is a record/dictionary subsumption)

Fix problem (it was error reporting...)

f832319

Rename trait

3e6b4b6

Co-authored-by: Yann Hamdaoui <yann.hamdaoui@gmail.com>

Correct spelling in comments

ca781bb

Co-authored-by: Yann Hamdaoui <yann.hamdaoui@gmail.com>

Rename trait impl

6e95840

Rename trait

c9e4f5a

Update comments

0dbc986

Remove subsumption function from typecheck/mod.rs

49f6bdf

Add test

b09a6d6

yannham force-pushed the subtyping/record_constructor branch from e55fce5 to b09a6d6 Compare August 6, 2024 13:26

Eckaos added 3 commits August 7, 2024 15:21

Add documentation

de31fce

Rename trait (for clippy)

264e067

Add tests

4afcad2

Eckaos requested a review from yannham August 7, 2024 14:04

Modify snapshot lsp

34ad290

yannham requested changes Aug 8, 2024

View reviewed changes

Eckaos and others added 5 commits August 9, 2024 14:55

Update comments core/src/typecheck/subtyping.rs

e739173

Co-authored-by: Yann Hamdaoui <yann.hamdaoui@gmail.com>

Update doc/manual/typing.md

90f33ea

Co-authored-by: Yann Hamdaoui <yann.hamdaoui@gmail.com>

Modify comment

fa5e76a

Modify comment

5405ee2

Revert lsp snapshot

edae4f2

yannham self-assigned this Sep 5, 2024

yannham added 2 commits September 6, 2024 17:00

Cosmetic improvements

f9fba13

This commit performs minor cosmetic improvements in the code handling subtyping, mostly around comments and function interfaces.

yannham approved these changes Sep 6, 2024

View reviewed changes

yannham enabled auto-merge September 6, 2024 15:21

yannham added this pull request to the merge queue Sep 6, 2024

Merged via the queue into tweag:master with commit 273ae0f Sep 6, 2024
6 checks passed

BrewTestBot mentioned this pull request Sep 9, 2024

nickel 1.8.0 Homebrew/homebrew-core#184055

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add record constructor to subtyping #2007

Add record constructor to subtyping #2007

Eckaos commented Jul 25, 2024

Eckaos commented Jul 25, 2024

yannham Jul 25, 2024

Eckaos Jul 25, 2024 •

edited

Loading

yannham Jul 25, 2024

yannham Jul 25, 2024 •

edited

Loading

yannham commented Jul 25, 2024 •

edited

Loading

Eckaos commented Jul 26, 2024 •

edited

Loading

Eckaos commented Jul 31, 2024 •

edited

Loading

yannham left a comment

Eckaos commented Aug 5, 2024 •

edited

Loading

yannham commented Aug 5, 2024

Eckaos commented Aug 6, 2024

github-actions bot commented Aug 6, 2024 •

edited

Loading

Eckaos commented Aug 7, 2024

jneem commented Aug 7, 2024

yannham commented Aug 7, 2024

yannham left a comment

yannham Aug 8, 2024

yannham Aug 8, 2024

yannham commented Sep 5, 2024

yannham commented Sep 6, 2024 •

edited

Loading

		//! Type subsumption
		/// Type subsumption is generally used when we change from inference mode to checking mode.

Add record constructor to subtyping #2007

Add record constructor to subtyping #2007

Conversation

Eckaos commented Jul 25, 2024

Eckaos commented Jul 25, 2024

yannham Jul 25, 2024

Choose a reason for hiding this comment

Eckaos Jul 25, 2024 • edited Loading

Choose a reason for hiding this comment

yannham Jul 25, 2024

Choose a reason for hiding this comment

yannham Jul 25, 2024 • edited Loading

Choose a reason for hiding this comment

yannham commented Jul 25, 2024 • edited Loading

Eckaos commented Jul 26, 2024 • edited Loading

Eckaos commented Jul 31, 2024 • edited Loading

yannham left a comment

Choose a reason for hiding this comment

Eckaos commented Aug 5, 2024 • edited Loading

yannham commented Aug 5, 2024

Eckaos commented Aug 6, 2024

github-actions bot commented Aug 6, 2024 • edited Loading

Bencher

Eckaos commented Aug 7, 2024

jneem commented Aug 7, 2024

yannham commented Aug 7, 2024

yannham left a comment

Choose a reason for hiding this comment

yannham Aug 8, 2024

Choose a reason for hiding this comment

yannham Aug 8, 2024

Choose a reason for hiding this comment

yannham commented Sep 5, 2024

yannham commented Sep 6, 2024 • edited Loading

Eckaos Jul 25, 2024 •

edited

Loading

yannham Jul 25, 2024 •

edited

Loading

yannham commented Jul 25, 2024 •

edited

Loading

Eckaos commented Jul 26, 2024 •

edited

Loading

Eckaos commented Jul 31, 2024 •

edited

Loading

Eckaos commented Aug 5, 2024 •

edited

Loading

github-actions bot commented Aug 6, 2024 •

edited

Loading

yannham commented Sep 6, 2024 •

edited

Loading