CQCL / hugr

Hierarchical Unified Graph Representation for quantum and classical programs
https://crates.io/crates/hugr
Apache License 2.0
24 stars 7 forks source link

Polymorphic top-level Hugrs / Substitution across nodes of Hugr #709

Open acl-cqc opened 1 year ago

acl-cqc commented 1 year ago

EDIT: there are two kind-of sub-issues here:

This'll be useful for #978; in time for compilation/lowering (by template-extension, rather than type-erasure/interpretation à la Tierkreis/JVM); it offers new Hugr-construction methods (alluded to in #457); it potentially simplifies tests (which could use a type variable instead of pulling in some extension just to give a concrete leaf type - although use of USIZE_T is widespread enough we barely notice).

If we store binders separately from the Hugr nodes, then we need to be careful about additional variables bound by FuncDefn nodes, i.e. can these still see the outer binders? If so, we have a limited return of DeBruijn indices, and will probably need to pass a second &[TypeParam] around validate_subtree (and a first into validate) etc.

acl-cqc commented 7 months ago

So, probably this is some kind of a wrapper around (a Hugr and some TypeParams), that one can validate (-> calls Hugr::validate passing in those TypeParams) and other things.

acl-cqc commented 7 months ago

This'll also give us a way to do inference separately for subgraphs and thus a better solution to inserting a subgraph than that of test_validate_with_closure from #884

acl-cqc commented 6 months ago

It is just possible that maybe we could treat FuncDefn as the only binder with TypeParams. We would still need a method to apply a substitution across the Hugr (i.e. instantiate a FuncDefn-rooted Hugr to a monomorphic, e.g. DFG-rooted, Hugr)