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

Promote val_modalities to Stable #3391

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Promote val_modalities to Stable #3391

wants to merge 2 commits into from

Conversation

riaqn
Copy link
Contributor

@riaqn riaqn commented Dec 18, 2024

This PR promotes modalities on values descriptions and module declarations to Stable.

There are no longer behaviors controlled by mode_alpha, but maybe it's fine to keep it for future convenience.

I confirm that our internal code base builds without changes, with this PR.

@riaqn riaqn force-pushed the stable_val_modalities branch from 5b83bab to 36215ea Compare December 20, 2024 13:47
@riaqn riaqn force-pushed the stable_val_modalities branch from 36215ea to 7ff35ae Compare January 3, 2025 10:23
@riaqn riaqn marked this pull request as ready for review January 3, 2025 11:08
@riaqn riaqn requested a review from tdelvecchio-jsc January 3, 2025 11:08
Copy link
Contributor

@tdelvecchio-jsc tdelvecchio-jsc left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good.

Copy link
Contributor

@tdelvecchio-jsc tdelvecchio-jsc left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm currently running into an issue where

(* x.ml, with no mli *)
type t = T of unit

let t = T ()
let u = lazy t

(* y.ml *)
let _ @ uncontended = X.u

(* Error: This value is contended but expected to be uncontended. *)

I hypothesize (but have not checked) that this PR introduces this bug. Can you check?

@riaqn
Copy link
Contributor Author

riaqn commented Jan 6, 2025

This is #2967 missing a mode crossing spot. Will fix.

Since we will push u to stongest modality portable, that makes the implicit lazy closure fun () -> t portable, which makes t only available as contended in the closure, which makes the returns of the closure contended and thus the whole lazy is at contended.

@riaqn
Copy link
Contributor Author

riaqn commented Jan 6, 2025

Well I just realized that the said mode crossing is already there for general variable lookup. What's missing is that the kind system don't know type t crosses contention. You can either try #3284, or maybe unsafely specify that it crosses contention?

Do you encounter similiar issues where such type t contains mutable fields? That might be more tricky to think about.

Copy link
Collaborator

@goldfirere goldfirere left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this should also update the documentation, now that we're putting the feature in stable.

@riaqn
Copy link
Contributor Author

riaqn commented Jan 6, 2025

@goldfirere Good point. Then we need documentation for portability and contention first, because val_modalities is mostly for them.

Also, we agreed to revise the new mode syntax so that @ is for modes and @@ for modalities. We need to do that revision before writing any documents.

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.

3 participants