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

Add Tierkreis extension spec after porting Tierkreis to HUGR #797

Open
ss2165 opened this issue Jan 9, 2024 · 0 comments
Open

Add Tierkreis extension spec after porting Tierkreis to HUGR #797

ss2165 opened this issue Jan 9, 2024 · 0 comments
Labels
spec Issues to do with the specification document(s)

Comments

@ss2165
Copy link
Member

ss2165 commented Jan 9, 2024

The section taken from the original hugr specification as part of #744:

Higher-order (Tierkreis) Extension

In some contexts, notably the Tierkreis runtime, higher-order
operations allow graphs to be valid dataflow values, and be executed.
These operations allow this.

  • CallIndirect: Call a function indirectly. Like Call, but the
    first input is a standard dataflow function type. This is essentially
    eval in Tierkreis.
  • catch: like CallIndirect, the first argument is of type
    Function[R]<I,O> and the rest of the arguments are of type I.
    However the result is not O but Sum(O,ErrorType)
  • parallel, sequence, partial? Note that these could be executed
    in first order graphs as straightforward (albeit expensive)
    manipulations of Graph structs/protobufs!

$\displaystyle{\frac{\mathrm{body} : [R] \textbf{Function}[R]([R] \textrm{Var}(I), [R] \textrm{Sum}(\textrm{Var}(I), \textrm{Var}(O))) \quad v : [R] \textrm{Var}(I)}{\textrm{loop}(\mathrm{body}, v) : [R] \textrm{Var}(O)}}$

loop - In order to run the body graph, we need the extensions
R that the graph requires, so
calling the loop function requires those same extensions. Since the
result of the body is fed into the input of the graph, it needs to have
the same extension requirements on its inputs and outputs. We require
that v is lifted to have extension requirement
R so that it matches the type
of input to the next iterations of the loop.

$\displaystyle{\frac{\Theta : [R] \textbf{Function}[R](\vec{X}, \vec{Y}) \quad \vec{x} : [R] \vec{X}}{\textbf{call\_indirect}(\Theta, \vec{x}) : [R] \vec{Y}}}$

CallIndirect - This has the same feature as loop: running a
graph requires its extensions.

$\displaystyle{\frac{}{\textbf{load\_const} \langle \textbf{Function}[R](\vec{I}, \vec{O}) \rangle (\mathrm{name}) : [\emptyset] \textbf{Function}[R](\vec{I}, \vec{O})}}$

load_const - For operations which instantiate a graph (load_const
and Call) the functions are given an extra parameter at graph
construction time which corresponds to the function type that they are
meant to instantiate. This type will be given by a typeless edge from
the graph in question to the operation, with the graph’s type added as
an edge weight.

@ss2165 ss2165 added the spec Issues to do with the specification document(s) label Jan 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
spec Issues to do with the specification document(s)
Projects
None yet
Development

No branches or pull requests

1 participant