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

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

Open
acl-cqc opened this issue Nov 21, 2023 · 3 comments
Open

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

acl-cqc opened this issue Nov 21, 2023 · 3 comments

Comments

@acl-cqc
Copy link
Contributor

acl-cqc commented Nov 21, 2023

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

  • A method to apply a substitution (i.e. [TypeArg]) across the nodes/body of the Hugr, rather than just the Type of a Hugr as we have now;
  • Some way to deploy the former - possibilities include
    • Adding [TypeArg] to insert_hugr and other related methods
    • A method on a FuncDefn-rooted Hugr that produces a new Hugr (rooted at either a monomorphic-FuncDefn or perhaps a DFG)
    • A standalone container of a Hugr+TypeParams that instantiates to just a Hugr
      The former involves the bulk of coding; the latter probably not much coding but much more deciding. I'm not separating the two yet though because the former is useless without the latter (without some way to use it).

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
Copy link
Contributor Author

acl-cqc commented Apr 8, 2024

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.

  • Should include an instantiate method that (given TypeArgs correct for all its TypeParams) produces a non-polymorphic Hugr. This is itself a bunch of work. (Partial instantiation probably not required)
  • Given No polymorphic closures #904, unclear whether you can have a "polymorphic top level hugr" (with some TypeParams) whose root node is a FuncDefn (binding more TypeParams). If so, then we'll have a limited form of DeBruijn (which was removed in No polymorphic closures #904), and we'll need to pass two sets of TypeParams through validation (the current set, replaced on entry to each FuncDefn, and the outermost "top-level" ones from the wrapper)

@acl-cqc
Copy link
Contributor Author

acl-cqc commented Apr 9, 2024

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
Copy link
Contributor Author

acl-cqc commented May 13, 2024

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)

@acl-cqc acl-cqc changed the title Polymorphic top-level Hugrs Polymorphic top-level Hugrs / Substitution across nodes of Hugr May 13, 2024
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

No branches or pull requests

1 participant