-
Notifications
You must be signed in to change notification settings - Fork 6
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
feat: Emulate TypeBound
s on parameters via constraints.
#1624
base: main
Are you sure you want to change the base?
Conversation
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1624 +/- ##
==========================================
+ Coverage 85.50% 85.57% +0.06%
==========================================
Files 136 136
Lines 25252 25378 +126
Branches 22164 22290 +126
==========================================
+ Hits 21592 21716 +124
+ Misses 2456 2439 -17
- Partials 1204 1223 +19
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Sentry. |
f9e97a7
to
b9e75fc
Compare
This PR contains breaking changes to the public Rust API. cargo-semver-checks summary
|
@@ -938,7 +956,7 @@ impl<'a> Context<'a> { | |||
model::Term::FuncType { .. } => Err(error_unsupported!("`(fn ...)` as `TypeParam`")), | |||
|
|||
model::Term::ListType { item_type } => { | |||
let param = Box::new(self.import_type_param(*item_type)?); | |||
let param = Box::new(self.import_type_param(*item_type, TypeBound::Any)?); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not sure why this is any (also not covered by tests), is this a todo waiting for a list constraint?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The item type is nested within the list and since we only constrain parameters directly here, we can not express that the items of the list should be copyable. Therefore the TypeBound::Any
.
(where (copy ?t)) | ||
(where (discard ?t)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this looks like it could get quite verbose. Will we need to specify things that are copy
but not discard
? Even if we do, I feel that ought to be the more verbose specification. Ideally I guess I want to write:
- Nothing for things that are copyable and discardable
- "linear" or "not copy" for things that are such
- "affine" when I can't copy but can discard.
Is this just a handy syntax change or are we running in to subtyping problems again?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, I feel that the "sales blurb" in the description that "The translation in this PR requires the two to be used together since TypeBound does not have the facility to express one without the other. Once we move to constraints in hugr-core, that restriction would be lifted." misses the point. We could have had separate copy/discard/affine/etc. in TypeBound, but we discussed this and did not decide that we wanted it. So I see no reason to do so now.
Indeed, if we change our minds are decide we want to add this in the future, there is still an easy mechanism (right?) - we just add two new constraints (say copy
and discard
) alongside the old copyable
and then define that copyable
holds if both copy
and discard
hold (and that each of the latter/two hold if copyable
does), right? (so ok we need a cyclicity check in the constraint solver.) The problem would just be better naming, we can't really have both copy
and copyable
....
So (the more I think about it, the more) I think we should stick with one combined constraint rather than two for now.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, if we can find a decent name for the combined constraint, I'd be happy to go for that. Any ideas?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nonlinear
..?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm fine with nonlinear
. @acl-cqc ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Generally I would say this looks pretty good, but I vote for combining copy+discard, also a couple of other ideas (/confusions)...
@@ -46,6 +46,8 @@ struct Context<'a> { | |||
term_map: FxHashMap<model::Term<'a>, model::TermId>, | |||
/// The current scope for local variables. | |||
local_scope: Option<model::NodeId>, | |||
/// Constraints to be added to the local scope. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is local scope
== [Self::local_scope]
? Do we actually plan to modify the local scope by adding these? Or are these "Constraints to be added to those from the local scope" (i.e., extra constraints from somewhere else)? "Constraints in addition to those from the local scope" would be clearer still that we don't intend to mutate some list.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When exporting a PolyFuncType
, we gather constraints in local_constraints
. PolyFuncType
itself can not express constraints, but if one of the parameters takes a copyable type, local_constraints
is where we record the corresponding constraint for that parameter.
@@ -397,6 +397,8 @@ pub struct FuncDecl<'a> { | |||
pub name: &'a str, | |||
/// The static parameters of the function. | |||
pub params: &'a [Param<'a>], | |||
/// The constraints on the static parameters. | |||
pub constraints: &'a [TermId], |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good point (in the PR description) about separating these out! :)
@@ -408,6 +410,8 @@ pub struct AliasDecl<'a> { | |||
pub name: &'a str, | |||
/// The static parameters of the alias. | |||
pub params: &'a [Param<'a>], | |||
/// The constraints on the static parameters. | |||
pub constraints: &'a [TermId], |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So the alias also introduces more constraints. I'd say that might make it slightly more than an alias; I can't introduce constraints just anywhere (without an alias), can I?
And when we have Terms in hugr-core, Alias's are likely to disappear after import (as we can get sharing via TermId, right?) - are we sure we want/need this?
Or maybe the idea is that the constraints here are copied(+substituted) from/according-to the RHS of the alias (they are the constraints that must apply anyway, rather than the Alias being able to specify new ones to introduce). If so, let's be clear in the comment....
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, good catch. I can imagine some niche uses, but for now it's probably best to remove constraints on aliases. If we find a good use case and mental model for this, we can add them again.
} | ||
|
||
/// A parameter to a function or alias. | ||
/// | ||
/// Parameter names must be unique within a parameter list. | ||
/// Implicit and explicit parameters share a namespace. | ||
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] | ||
pub enum Param<'a> { | ||
/// An implicit parameter that should be inferred, unless a full application form is used | ||
pub struct Param<'a> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
+1 to this commoning up, amen.
I am a long way from convinced that we need implicit/explicit, but that's another issue and definitely not for this PR!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(nice that Constraints are now separate from Parameters here too! 👍 )
@@ -662,40 +670,42 @@ pub enum Term<'a> { | |||
/// | |||
/// `ctrl : static` | |||
ControlType, | |||
|
|||
/// Constraint that requires a runtime type to be copyable. | |||
CopyConstraint { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would not object to a general Term::Constraint { name: str, args: Vec<TermId> }
with the name looked up in data that is static for now (i.e. just the one/two constraints and none user-defined). It does kinda say that there will be more constraints coming, but with the data being static there is no possibility of adding them.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is a possibility and moreover a mechanism for adding them: Your Term::Constraint { name: str, args: Vec<TermId> }
is Term::Apply
/Term::ApplyFull
for a constructor that declares a constraint.
There are good arguments for keeping Term
as minimal as possible by defining anything that does not need special handling as a custom constructor in a standard extension. In particular it'd remove a bunch of boilerplate code. There's also arguments for having anything that is structurally important as builtin; for example adt
s since the control flow mechanism depends on it, or copyability constraints since they emerge just from the connectivity pattern of ports. I could go either way.
for param in decl.params { | ||
this.print_param(*param)?; | ||
} | ||
this.print_params(decl.params)?; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If we are sure we want constraints in Alias too (I argue against elsewhere), then it is true that everywhere you introduce params you also introduce constraints; maybe a struct ParamsAndConstraints<'a>
(maybe ConstrainedParams
?) would be useful, as it'd allow combining all these print_params(...); print_constraints(...)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree that we'd probably want to avoid constraints on aliases for now.
@@ -460,25 +446,37 @@ impl<'p, 'a: 'p> PrintContext<'p, 'a> { | |||
} | |||
} | |||
|
|||
fn print_params(&mut self, params: &'a [Param<'a>]) -> PrintResult<()> { | |||
for param in params { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nit: can you just params.iter().try_for_each(self.print_param)
(maybe .copied()
or something) ?
(where (copy ?t)) | ||
(where (discard ?t)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, I feel that the "sales blurb" in the description that "The translation in this PR requires the two to be used together since TypeBound does not have the facility to express one without the other. Once we move to constraints in hugr-core, that restriction would be lifted." misses the point. We could have had separate copy/discard/affine/etc. in TypeBound, but we discussed this and did not decide that we wanted it. So I see no reason to do so now.
Indeed, if we change our minds are decide we want to add this in the future, there is still an easy mechanism (right?) - we just add two new constraints (say copy
and discard
) alongside the old copyable
and then define that copyable
holds if both copy
and discard
hold (and that each of the latter/two hold if copyable
does), right? (so ok we need a cyclicity check in the constraint solver.) The problem would just be better naming, we can't really have both copy
and copyable
....
So (the more I think about it, the more) I think we should stick with one combined constraint rather than two for now.
(forall ?t type) | ||
(where (copy ?t)) | ||
(where (discard ?t)) | ||
[(@ foo.tuple ?t)] [(@ foo.tuple ?t) (@ foo.tuple ?t)] (ext)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What is foo.tuple
??
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's some arbitrary custom constructor to trigger a particular case in import/export for more test coverage. tuple
is for "historical" reasons since the example was different at first... Can rename it into something more nondescript.
This PR translates some
TypeBound
s inhugr-core
to constraints inhugr-model
. This translation only occurs on parameters that take a runtime type directly. We use two constraints to modelTypeBound::Copy
: thecopy
constraint guarantees that values of a type are copyable, while thediscard
constraint ensures that we can forget values of a type. The translation in this PR requires the two to be used together sinceTypeBound
does not have the facility to express one without the other. Once we move to constraints inhugr-core
, that restriction would be lifted.As a driveby change before the model stabilises, this PR also moves constraints out of the parameter lists into their own list. In its previous form this could have led to confusions about which parameter a local variable index refers to when a constraint is situated between two parameters in the list.
Closes #1637.