feat: validate Terms used as parameter types are appropriate (into #2309) #2345

acl-cqc · 2025-06-16T21:18:13Z

PR into #2309, of which I think this should be part. Rule out e.g. BoundedNat's as parameters!

Note the converse - is it a valid argument? - is basically done by validate as anything is a valid argument (for some parameter).

Could do with some tests, but proptest gets us some of the way.

acl-cqc · 2025-06-16T21:19:36Z

hugr-core/src/types/type_param.rs

-            }
-            (Term::Tuple(es1), Term::Tuple(es2)) => {
-                es1.len() == es2.len() && es1.iter().zip(es2).all(|(e1, e2)| e1.is_supertype(e2))
+            (


So we can drop this clause too, it's only there to provide a place for the comment...

acl-cqc · 2025-06-16T21:20:29Z

hugr-core/src/types/type_param.rs

@@ -308,7 +333,7 @@ impl Term {

                check_typevar_decl(var_decls, *idx, cached_decl)
            }
-            Term::RuntimeType { .. } => Ok(()),
+            Term::RuntimeType(_) => Ok(()),


driveby. Hmmm, and could do the next line too. I'm surprised the old code is legal...

codecov · 2025-06-16T21:20:52Z

Codecov Report

Attention: Patch coverage is 79.16667% with 5 lines in your changes missing coverage. Please review.

Project coverage is 82.14%. Comparing base (c401c30) to head (1bf35d8).

Files with missing lines	Patch %	Lines
hugr-core/src/types/type_param.rs	85.71%	3 Missing ⚠️
hugr-core/src/types/poly_func.rs	33.33%	0 Missing and 2 partials ⚠️

Additional details and impacted files

@@                    Coverage Diff                     @@
##           zrho/core-merge-arg-param    #2345   +/-   ##
==========================================================
  Coverage                      82.13%   82.14%           
==========================================================
  Files                            241      241           
  Lines                          43936    43949   +13     
  Branches                       39765    39778   +13     
==========================================================
+ Hits                           36086    36101   +15     
+ Misses                          5862     5858    -4     
- Partials                        1988     1990    +2

Flag	Coverage Δ
python	`85.30% <ø> (ø)`
rust	`81.81% <79.16%> (+0.01%)`	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

zrho · 2025-06-17T08:49:40Z

hugr-core/src/types/type_param.rs

+                _,
+            ) => {
+                // This is not a type at all, so it's not a supertype of anything.
+                false


I don't see the problem with this relation being reflexive.

More than that it's helpful for it to be reflexive: Say you have a variable v. If this variable stands for a static type, we should have v ⊆ v, since whatever static type it stands for, it is a subtype of itself. Since we don't know if v does stand for a static type, we should have v ⊆ v for all variables. But we also should have that replacing variables with concrete terms preserves the subtyping relation. Which then forces t ⊆ t for every term t.

Why don't we know if v stands for a static type? Consider

(declare-ctr foo (param ?t core.static) (param ?v ?t) core.static)

Re. the (param ?v ?t), see other comment

Say you have a variable v. If this variable stands for a static type, we should have v \subseteq v`

I think we should conclude that v \subseteq v this is true only if the bound on v is StaticType...I mean, my gut feeling is that if we find variables here, we should be calling (recursing) is_supertype using the cached_decl. Possibly on both sides?? (That is, only if we go with dependent types.)

Here ?v has type ?t.

Suppose ?v ⊆ ?v is false. We then instantiate ?t with core.static. Now ?v ⊆ ?v becomes true. That appears to me to violate the principle of least surprise. So ?v ⊆ ?v should be true. ⊆ should also be preserved by instantiating. We instantiate ?t with core.nat. Then ?v ⊆ ?v should remain true. Instantiate ?v with 5 then 5 ⊆ 5 should also hold.

Ultimately this is a huge distraction. Subtyping will go away ideally anyway. If we have reflexivity, we don't need additional information, the relation behaves well with substitution, and nothing breaks.

Arrgh. So.... given your above foo, I could instantiate ?t with RuntimeType and then ?v with Qubit....which seems ok. But could I instantiate ?t with Qubit? (Or even a classical runtime type, doesn't have to be quantum). Then there would be no valid/possible instantiations of ?v...right?

If we instantiate ?t with BoundedNatType then ?v would have to be a BoundedNat. But if we instantiate ?t with some e.g. BoundedNat(5), then ?v would....following your suggestion of reflexivity...have to be BoundedNat(5) as well?

So my suggestion that a variable is a type (with "subtypes") only if it's bounded by static type doesn't make sense - rather, I'd need to check that it's bounded such that it cannot be a Runtime. Which would need a different type hierarchy and (I speculate) be unworkable, yeah.

So if reflexivity is the way out of this then...ok (I appreciate as you say that subtyping is gonna go away)...but I worry users (writers of polymorphic functions, say) are gonna shoot themselves in the foot here because they don't understand the shape of the gun. At the moment I can't figure it out so I am looking for my steel-toecapped boots...

Ok, thanks Lukas - that's helpful. I realized about ?t=Qubit too. I guess I am not too worried about is_supertype - as you say, it will go as we get rid of subtyping (or rather, it will become constraint implication!). I'm more worried about footgun's like (param ?t (BoundedNat 5))....

Regarding:

Suppose ?v ⊆ ?v is false. We then instantiate ?t with core.static. Now ?v ⊆ ?v becomes true. That appears to me to violate the principle of least surprise.

I'm less sure of this. I think many things can become true when you instantiate something with something else. Rather, given only the definition of ?t (and no particular instantiation), we should be able to figure out the things that are true for all instantiations. Additional things may become true for particular instantiations.

So in old hugr-core, you'd never really have the situation where you had instantiated ?t but still had ?v "free" - so you'd never be asking questions about what was true for all ?v but for a fixed ?t. This because you provide values for all TypeArgs at once (and they were not allowed to refer to each other). I think that invariant is now disappearing - you can Term::Apply(Term::Apply(t, ...args1...), ...args2...) right?

Apply can only apply symbols and not other terms. So the invariant still holds.

I think where I'm heading is that while your foo is ok/good, IIUC, it has the property that for any possible instantiation of ?t, there is at least some legal ?v. Whereas in something like this:

(declare-ctr foo3 (param ?t core.static) (param ?u ?t) (param ?v ?u) core.static)

Are there legal instantiations? Definitely if ?t = core.static then there are (e.g. ?u = RuntimeType + ?v = Qubit)

But if ?t = RuntimeType then there are possible values for ?u e.g. Qubit or RuntimeInt but no possible values for ?v (whatever ?u is)

Ok, let's pick, oh, ?t = FloatType. Then ?u = Float(5.0) or any other float. But then there are no sensible values for ?v - unless we allow reflexive ones, but I don't think you are proposing Term::Float : Term::Float (it's not in the code), and to me these just seem a bit silly.

Similarly if ?t = ListType(....) then ?u = List(...) is the only possibility and again there is no possible ?v

So, is there any ?t != core.static which admits instantiation of foo3?

Yes, there are instantiations with ?t != core.static. Say we have

(declare-ctr a core.static) (declare-ctr b a) (declare-ctr c b)

Then (foo3 a b c) is a valid instantiation. Less contrived examples:

(core.order_hint.key 2) : core.meta : core.static

(arithmetic.int.const 6 1337) : (core.const (arithmetic.int.types.int 6)) : core.static

Right - so my foo3 is rather bogus but only given the flat two-level hierarchy we have ATM

zrho · 2025-06-17T08:51:56Z

hugr-core/src/types/type_param.rs

+            | Term::Float(_)
+            | Term::List(_)
+            | Term::Tuple(_)
+            | Term::Variable(_) => Err(SignatureError::InvalidTypeParam(self.clone())),


A variable can be a static type!

(declare-ctr pair (param ?t core.static) (param ?first ?t) (param ?second ?t) core.static)

Ok isn't this pair here basically dependent types? That kind of example is something we deliberately tried to avoid in Hugr "v1". Are you sure you are not opening the door to undecidability and all kinds of trouble here?

It is a very restricted form of dependent types. We don’t have higher order functions in the static language, no recursion, etc. And it’s quite necessary to give types to some things we want (e.g. the load constant op or the call direct op).

(declare-op core.load_const (param ?t core.type) (param ?c (core.const ?t)) (core.fn [] [?t])) (declare-op core.call_direct (param ?inputs (core.list core.type)) (param ?outputs (core.list core.type)) (param ?f (core.const (core.fn ?inputs ?outputs))) (core.fn ?inputs ?outputs))

We don't have higher order functions in the static language, no recursion

Ok....I mean, custom constructors look a bit like that, admittedly they are very simple, so are we sure they don't provide enough of that?

quite necessary to give types to some things we want, e.g. the load constant op

Ah, so in Hugr the "wire type" (EdgeKind::Const) depends on the type argument, but the other type arguments do not, so the "two level" system happens to be just expressive enough. But in hugr-model that "wire" is another type arg. Hmmm.

I admit this does make the checking more complicated. One would need to check each type parameter given only the preceding ones (to avoid cyclic dependencies), say. But it's not a disaster. Hmmmm.

The "two level" system is only expressive enough because we special cased a lot of things (like the constant one), and even for custom ops we use Rust code to compute signatures whenever they're even slightly non-trivial. The dependent types allow us to capture much more without resorting to escape hatches like that.

The custom constructors don't introduce issues since they don't reduce. Aliases could though, and should therefore be restricted to be non-recursive.

Ok, thanks - seems reasonable

…*earlier* parameters

acl-cqc changed the title ~~feat: validate Terms used as parameter types are appropriate (into~~ feat: validate Terms used as parameter types are appropriate (into #2309) Jun 16, 2025

acl-cqc changed the base branch from main to zrho/core-merge-arg-param June 16, 2025 21:18

acl-cqc commented Jun 16, 2025

View reviewed changes

acl-cqc requested a review from zrho June 16, 2025 21:28

acl-cqc marked this pull request as ready for review June 16, 2025 21:28

acl-cqc requested a review from a team as a code owner June 16, 2025 21:28

zrho reviewed Jun 17, 2025

View reviewed changes

zrho added 21 commits June 17, 2025 17:38

...Type suffix for TypeParam variants.

4430a3e

Merge TypeArg and TypeParam.

e270162

Implement functions.

593bb6a

Docs.

a972d2a

Adjust Arbitrary instance to avoid infinite recursion.

b0b8507

Import no longer needs to distinguish between type params and args.

e17e918

JSON compatibility layer in Rust.

1f62ea4

Added proptest for Term::contains.

d1404b9

Fix Term::contains.

ea05c57

Taking the opportunity to have nicer field names.

e4cde0b

Formatting.

377eb27

Update feature gated code.

ae48d57

Hash change in snapshot test.

3ff1d5c

Another hash in a snapshot.

5bfcb55

Tuple fields.

af19410

Instantiate Terms with From and new_*.

79066ce

Lints and link to const issue.

4a9171a

TermVar.

b2e7b6c

Lints.

be931d9

Extension resolution on Terms.

ba71b19

Formatting.

7c521f3

zrho added 5 commits June 17, 2025 17:42

Rename check_type_arg to check_term_type.

d52193a

Use .into

903da0c

Formatting

bba7e72

Lints.

4008375

Typo, is_supertype, Term::Runtime.

c401c30

zrho force-pushed the zrho/core-merge-arg-param branch from b322c2e to c401c30 Compare June 17, 2025 16:42

acl-cqc mentioned this pull request Jun 17, 2025

feat!: Merge TypeParam and TypeArg into one Term type in Rust #2309

Merged

acl-cqc added 8 commits June 17, 2025 18:24

Add validate_param

b0d58b7

is_supertype need only deal with types

9d19ba5

update proptest

67bcc63

Allow variables as parameter types, so validate cached_decls against …

b6dfde2

…*earlier* parameters

Allow invariant case for variables

a0996c7

fix corner case of non-type variable

dfc9444

Missing RuntimeType: StaticType case

7d08db6

Handle variables by is_cached_static

1bf35d8

acl-cqc force-pushed the acl/validate_param branch from e1d39a7 to 1bf35d8 Compare June 17, 2025 17:25

Base automatically changed from zrho/core-merge-arg-param to main June 17, 2025 17:42

feat: validate Terms used as parameter types are appropriate (into #2309) #2345

Are you sure you want to change the base?

feat: validate Terms used as parameter types are appropriate (into #2309) #2345

Uh oh!

Conversation

acl-cqc commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

acl-cqc Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

acl-cqc Jun 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

acl-cqc Jun 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

acl-cqc Jun 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

zrho Jun 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

acl-cqc commented Jun 16, 2025 •

edited

Loading

acl-cqc Jun 16, 2025 •

edited

Loading

codecov bot commented Jun 16, 2025 •

edited

Loading

acl-cqc Jun 17, 2025 •

edited

Loading

acl-cqc Jun 17, 2025 •

edited

Loading

acl-cqc Jun 17, 2025 •

edited

Loading

zrho Jun 17, 2025 •

edited

Loading