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

Functional mode polymorphism #3395

Open
wants to merge 2 commits into
base: ageorges.mode-polymorphism-instantiate
Choose a base branch
from

Conversation

ageorg29
Copy link
Contributor

This PR integrates mode levels into type checking, and implements mode polymorphism, and introduces a new flag that turns on various degrees of the feature:

-extension mode_polymorphism_alpha

enables mode polymorphism, while

-extension mode_polymorphism_beta

enables levels, but applies generalize_structure rather than generalize, and therefore does not infer polymorphic modes.

The PR involves:

  1. updating the level of mode whenever the level of a type is updating
  2. generalizing a mode variable when a type is generalized
  3. copying mode variables in the same manner as type variables are copied (this can be either an instantiation of a mode variable, a deep and exact copy, or an exact copy of the generic parts of a mode).

To implement copying, the existing copy scope in btype.ml is extended to include the mode copy scope.

Finally, new mode variables are allocated either at level 0 --- whenever a mode variable should not be generalized, such as allocation modes --- or at the current level.
NB: the curry mode of a function with multiple arguments (i.e. m0 in (a @ m1 -> b -> c) @ m0) is set to level 0.

Some notable invariants:

  • modes in typedtree.ml should always be at level 0. To guarantee this invariant, typecore.ml allocates new mode variables above the inferred generic ones using newvar_above_if_nonzero.
  • generic mode variables should (almost) never be mutated: that means regular calls to zap_to_X do nothing on generic mode variables. There are two exceptions: (1) if the mode_polymorphism_alpha extension is not turned on, generic modes are zapped during remove_mode_and_jkind_variables, and (2) polymorphic mode variables are printed as their zapped versions. To zap generic mode variables, use zap_to_X_force.

Since generic mode variables are no longer zapped, it is important to instead determine the level 0 modes they might point to. If a mode occurs only in covariant positions to other modes in the typed expression, it is zapped to floor, if it occurs only in contravariant positions to other modes in the typed expression, it is zapped to ceiling, and if it occurs in both, it is zapped to legacy.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant