Skip to content

Polymorphic top-level Hugrs #709

Open
@acl-cqc

Description

@acl-cqc

Preliminary: note #1733 added the ability to substitute across the nodes/body of the Hugr, rather than just the Types of a Hugr; and #1934 applies this across a subtree copied from a polymorphic funcdefn to a monomorphic callsite.

Here we want a standalone structure of a Hugr+TypeParams, with a validate method (and maybe other Hugr(View/Mut)-like methods), i.e. calling some new Hugr::validate_with_type_params (and Hugr::validate just calls that with the empty list).

Maybe also a method that "instantiates" it to just a Hugr.


This will(EDIT: might!) 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. So perhaps maintain that the outer TypeParams are not visible inside any inner FuncDefns.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions