Values and constants

[zrho]

I'm currently trying to figure out how to deal with constants and Values. Values appear to occupy a strange conceptual place. In Tierkreis they made a lot of sense: we were specifying a single language with one particular semantics, and the Tierkreis Value is the data structure that is sent around. HUGR doesn't have one semantics. A value that flows along a hugr edge might be an int in an llvm register, or a serialised data structure to be sent over the network like in Tierkreis, or represent an Yb171 ion that at the very moment sits in some machine somewhere in Colorado. In my mind, runtime values in hugr are something that can't be accessed directly but rather only talked about indirectly, e.g. by creating a graph through which the value must flow. I don't know if that description makes sense, so I'd happily elaborate.

The significance for hugr comes from const nodes. At the moment, Const nodes together with LoadConst nodes take a Value and put it on a wire. Adopting the world view described above, what does it even mean to put a Value on a wire? An LLVM program does not have Values, and a qubit can definitely never be a Value. It makes sense when you think of the Const /LoadConst nodes taking in a description of how to construct a value; so Value is not the value itself, but a blueprint.

But at that point, Values and const nodes become redundant in the format, since we already have the language of terms (i.e. Types, TypeArgs and TypeParams when suitably combined like in #1405) which can specify compile time values. To put an integer on a wire, we can use an operation that takes an integer as a parameter. Similarly, we have products, sums, custom named types, string literals, etc for statically known data.

Const nodes serve an additional purpose: a single Const node can be referenced by multiple ConstLoad operations throughout a graph. But we also have a mechanism for this for terms via AliasDefn and AliasDecl nodes. They currently only work for types, but since the difference between types and terms is quite blurry already, we could make them work for arbitrary terms.

[ss2165]

I agree with the conceptual problems you highlight. Value does not represent runtime values. It can only represent compile-time values. However, it can currently express much more than the values expressible as TypeArgs.

Would it help to instead reframe Value and Const as Literal and LiteralOp?

[zrho]

So Values can express two things that aren't in TypeArgs:

• Values can contain nested Hugrs. We could instead extend TypeArgs with the ability to reference a function by name that is defined in the file. That way there is only one graph in a file.
• Values can also contain some opaque stuff hidden behind a Box<dyn ...> and some typetag magic to make them serialisable specifically as JSON. That of course does not serialise well to anything else. If TypeArg has type constructors instead, we can - together with sum types, product types, int literals and string literals - describe quite a few custom data types.

[ss2165]

Value is also used by constant folding, which is extensible. I agree that the typetag stuff is not great, and there's a bunch of issues about that that need addressing. But it would be good to preserve the functionality of having constant folding over extension types. Do you envision that being done over TypeArgs too?

[zrho]

Constant folding is something that happens within the compiler and doesn't need to be exposed necessarily. The constant folder is free to take TypeArg, parse it into whatever internal representation is most convenient, and spit out a TypeArg in the end. That ensures that extension values are always expressible in a regular way, accessible to serialisation, a text format, type checking, etc. It also frees up the constant folder to internally use a different lattice that might not be values directly.

[acl-cqc]

Ok lots of good stuff here but lots of points.

• One goal of Value specifically was to include custom extension values. We cannot assume these can be built by sums, products and literals....can we?!?!
• Whilst serialization to JSON isn't great (and the implementation/specification of how values are serialized, i.e. via typetag, is...another matter ;-) ), we hoped that this would allow runtimes that don't understand how to implement an extension at runtime, to use this JSON as a fallback, i.e. so long as said extension values are just passed through without being operated on.
• The idea that only some runtime values can appear in static values is (intended to be) captured by that Values must be "Copyable" i.e. no qubits. Of course it's not quite right to equate/conflate "can be captured statically" and "copyable", but the idea is that "loading" a Constant equals copying the static value into whatever runtime structure is necessary.
  • Indeed, this was one use of the "equatable" TypeBound that we removed (@ss2165) - TypeParam's must be Equatable (no floats) so we can tell when two node-operations are equal, which goes further than what we require for Constants. (Of course, then there is the Opaque backdoor...)
• It might be interesting to type-parametrize Const by a Value, but doesn't this lead to dependent types? I.e. the type of the output edge of the (load)Const is not the Value (TypeParam) but the type of the Value. I.e. one could say that the Const is parametrized by [Type(Copyable), **Value whose type is the previous**] and we don't have any mechanism to express such dependencies ATM (a deliberate design decision to rule out such). You're gonna suggest a constraint "typevariable A is the type of typevariable B"....
  • If we did that, then yes we could generalize Alias (which ATM is only types not other static values) and use that as an alternative to Const.
• Re. getting rid of Value::Function (and replacing that with something that's "name of a function in the Hugr") - if we don't care about being able to have nested Hugrs (to avoid scoping/namespacing issues and aid compositionality, locality of rewrites etc.) then we just drop Value::Function altogether and use the LoadFunction that we have already which does exactly this (identifying the function to load via an edge rather than a name)
  • Also (a minor point but) in a Tierkreis context, the runtime implementation is not as uniform - either (a) runtime function values now have to be either a Hugr/graph or a reference to a function in the current Hugr, or (b) to make its runtime-value output, "loadConstant" has to copy not the static value (a function name) but the FuncDefn from the containing Hugr.

[acl-cqc]

So perhaps rather than "function name" we could have some kind of Value for specifying an "output port of node in this hugr"? That would kind of unify LoadConstant with LoadFunction so we'd be able to drop the latter. Of course we'd then want such "outport" Values would then show up as targets of edges leaving said outport (?!), and we still lose the ability to nest Hugrs

[zrho]

Value for specifying an "output port of node in this hugr"

Here be dragons. We definitely do not want static values to depend on runtime values. Now we could of course restrict this to "static edges", but then why not just refer to the FuncDefn node directly. (I think the "static edges" are a design flaw anyway)

[acl-cqc]

Yah, I was thinking static outports only, and indeed there can only be one of those (at most). So referring to a node would kind-of be ok, but it'd be good to integrate this with edges, so I can easily see all the consumers of my static outport (/referees to this FuncDefn node) together.

[zrho]

Or you might see it as an argument why Call nodes shouldn't refer to FuncDefns by edge but by node as well. Currently we use edges for this, likely so that the graph can be used to navigate between definitions and usages. Static edges are already different in many ways to value edges, needing special cased treatment. When FuncDefns can be referred to by terms, which aren't nodes in a graph and therefore don't have ports themselves, we need some additional mechanism to keep track of the def/use chains. At that point we might as well use that one also for, e.g., Call nodes referring to FuncDefns.

Having references to FuncDefns in terms obviates the need for an additional mechanism for Call nodes to refer to FuncDefns. They would just take a parameter whose type guarantees that the parameter refers to a runtime function. Similarly for LoadFunction, etc.

[acl-cqc]

likely so that the graph can be used to navigate between definitions and usages

Indeed. I think if you can preserve that then the rest sounds good to me.

[zrho]

If the extension values can be represented as JSON, they can be represented by products, sums, literals and lists. We could even add tierkreis-like structs and enums with named fields and variants at some point to make it closer to JSON. Add to that custom type constructors, and it's quite expressive.

You refer to loading a constant by copying its static value into whatever runtime structure is necessary. That captures it quite nicely: the static value isn't the runtime structure, but it is a description from which we can build the runtime structure.

Regarding the type of the const node: yes, dependent types would be one solution to this. Another would be to not have a single constant node, but have nodes for the different data types. For instance, an llvm extension would have a const-f32 node, which takes a static f32 as parameter and has an output edge with an llvm.f32 on it. Compound values can then be built by composing graphs. Doing this is already necessary for compound values that contain a runtime value. I actually quite like that approach, and it doesn't even need a lot of special support. If it proves too limiting or tedious, one can always add back some sort of generic constant node.

I do not see how Value::Function would be necessary to have nested hugrs. We have local function definitions, and we can relax the restriction that only builtin ops may have child nodes (which I strongly encourage). Also could you rephrase your point on Tierkreis? I can't seem to parse it.

[acl-cqc]

If the extension values can be represented as JSON, they can be represented by products, sums, literals and lists. We could even add tierkreis-like structs and enums with named fields and variants at some point to make it closer to JSON. Add to that custom type constructors, and it's quite expressive.

I like the first point, although does JSON really have sums (you mean by enclosing any value in a singleton dict with a string "tag"?), and indeed we might find we wanted a struct/record. If e.g. adding a static struct/record type with named (unordered) fields is enough to satisfy (existing) JSON users then I could probably go with that ;). Note that one use of Opaque is to wrap external (potential third-party) libraries, though, so they are more likely to have JSON serialization already; do we want to mangle arbitrary JSON into some Hugr version?

(And yes, there's some kind of custom type constructor that says, I assert the stuff inside here has the type I say, without having to declare a schema of what goes inside the constructor.)

Regarding the type of the const node: yes, dependent types would be one solution to this. Another would be to not have a single constant node, but have nodes for the different data types. For instance, an llvm extension would have a const-f32 node, which takes a static f32 as parameter and has an output edge with an llvm.f32 on it. Compound values can then be built by composing graphs. Doing this is already necessary for compound values that contain a runtime value. I actually quite like that approach, and it doesn't even need a lot of special support. If it proves too limiting or tedious, one can always add back some sort of generic constant node.

So if I want a constant that's a list of (a tuple of 3 and "foo") and (a tuple of 4 and "bar") then I have four constants, plus two make-tuples, plus a make-singleton-list and a list-append (or an empty list and two list appends)? I think we've leant against this because the make-tuples, make-singleton-list, and list-append are all runtime ops. We can fold the values into a TypeArg::List of TypeArg::Tuples (assuming separation of TypeArg::Sequence into those two), but then we can't put the result into a constant node...?

I do not see how Value::Function would be necessary to have nested hugrs. We have local function definitions, and we can relax the restriction that only builtin ops may have child nodes (which I strongly encourage).

Nested Hugr as in a node that contains another Hugr as a Value, rather than being parent to the nodes of the other Hugr in the hierarchy. If you have a standalane Hugr, "nesting" it inside a node in an outer Hugr preserves node indices, whereas putting it into the hierarchy beneath another node requires renumbering everything. (I don't mean that renumbering is terrible and must be avoided, just to explain what I mean by "nested Hugr".) @ss2165 do we still need these nested Hugrs? I think the original need for them stemmed from before we had local/scoped definitions but

Also could you rephrase your point on Tierkreis? I can't seem to parse it.

Sorry, that was a bit jumbled. ATM a TierkreisValue (used for both serialization/protobuf, and internal runtime values) can be a Graph, with its own nodes and edges. Something here may have to change - maybe that becomes an Arc, maybe plus an index of the node to consider root (so you can refer to a subtree of a Hugr elsewhere without duplicating it); and/or we add other forms of Graph value besides "owning your own Graph". It's purely an implementation thing, and the increase in complexity is not massive, so not very important.

[zrho]

because the make-tuples, make-singleton-list, and list-append are all runtime ops

Are you constructing a runtime value?

[zrho]

My comparison between our terms and JSON was purely in terms of expressiveness. I don't know how wise it would be to actually make that correspondence more formal. The way in which to specify arbitrary extension data is quite a difficult area, with many tradeoffs.

We could just use JSON for it. The binary format would then need to either store JSON strings, or have their own encoding of JSON values (doable). Similar for the text format. But if we do that we lose the ability to inspect any value without having access to the code that implements the extension. MLIR does make this tradeoff, and arguably even more so, since attributes can be [almost] arbitrary strings in the text format and arbitrary bytestrings in the binary format.

But we already have a system that can encode structured data (terms, the unified Type/TypeArg/TypeParam thing). Terms have a type system, and so operations can specify the shape of their parameters declaratively as a type. Via dependency and constraints, the parameters can participate in the type checking/inference process. When no custom constraints are required, all of this is possible declaratively with no additional code. Much of what is custom validation code in MLIR would just be type checking.

By using terms we can also do stuff like referring to a FuncDefn. Sure, the JSON can have a string or int in there that refers to the function somehow, but unless we deserialise it to whatever custom representation, and then make the custom representation sufficiently transparent for the compiler, we do not know that these strings or ints refer to functions. A generic way to rename/reindex functions and adjust references to it is then impossible.

[acl-cqc]

Are you constructing a runtime value?

Yes - the only possible target of the edge from a Const node is a LoadConstant which produces a runtime value.

I think perhaps it's important to say that I don't think we are interested in Hugrs that do not encode runtime computations. (Even if these are trivial computations like "load this constant"). The static language is there to tell us about what the runtime bits might do.

[zrho]

My mental model of HUGR has been converging more and more to a subset of DLNL (https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf). DLNL as a linear language and a non-linear language, where the non-linear language has dependent types. It's not entirely precise, and we restrict the dependency more than DLNL does, but I think it is very helpful to put it in this context.

For our purposes, think of the linear language as the runtime values. Operations are functions in the linear language, and a dataflow graph describes how to compose operations in the linear language (if you like categorical semantics, the dataflow graph is a string diagram for the symmetric monoidal category underlying the linear language). The non-linear language is the language of parameters/arguments/types/statically known values/terms; whatever you want to call them.

A linear value may depend on non-linear values, but not the other way around. For us this means that runtime values may depend on static values, but static values may not depend on runtime values. A runtime vector whose length depends on a static parameter is fine. A static parameter that embeds a qubit is not.

Now DLNL allows to take a linear value e of linear type A and make it into a non-linear value G(e) of non-linear type G(A), as long as e has type A in an empty linear context. The linear context in our case is given by (value) edges. So every FuncDefn that has no (value) edges crossing its boundary (we always enforce this anyway, right?) can be quoted as a non-linear value. This is what I mean with referring to a FuncDefn by name inside a term.

[acl-cqc]

Static language = exclusively non-linear, all evaluation by substitution (no "operations"), fine.

Runtime language includes static language but adds linear, ok. Maybe exclusively linear, if we can convert flexibly enough, but note we need to be able to have runtime-only operations operating on non-linear values, the results are not part of the static language (I think the fact that these have incoming edges means they aren't?), but are still nonlinear.

So every FuncDefn that has no (value) edges crossing its boundary (we always enforce this anyway, right?)

We enforce only static edges into a FuncDefn e.g. so you can have mutually recursive functions (FuncDefn A contains call with edge from FuncDefn B).

can be quoted as a non-linear value. This is what I mean with referring to a FuncDefn by name inside a term.

Ok, so maybe not using naming. I think the issues that need addressing here then are how this reference is represented particularly wrt. edges (which we want for rewriting, for example).

[zrho]

The runtime language is a priori a different language to the static language. It is non-linear in the sense of "not necessarily linear", just like a non-abelian group might still have elements that commute. So it can still have values that can be copied (semantically this is copy nodes, but we can see edges that have multiple input ports in them as syntactic sugar).

We can then make the runtime language and the static language interact. One of these interactions is quoting a runtime function as a static term, for instance by its name/static port/node id/nesting. Another interaction is closer to the discussion of constant nodes: given values of the static language, how do we produce runtime values? If we have a canonical translation from static values into runtime ones, this could just be a single const node, taking a static value as a parameter and producing a runtime value. I don't know if we really want such a canonical translation. We can still do without, as alluded to above.

[acl-cqc]

Spoke briefly with @ss2165 and it seems we may not care about supporting "nested Hugrs" (as opposed to subtrees) anymore (perhaps that requirement may have originated before we had nested/scoped definitions?). That significantly frees up the design space. Still curious as to how the "translation from static values into runtime ones" would work for FuncDefn nodes into consts. Quoting from elsewhere:

Sure, the JSON can have a string or int in there that refers to the function somehow, but unless we deserialise it to whatever custom representation, and then make the custom representation sufficiently transparent for the compiler, we do not know that these strings or ints refer to functions. A generic way to rename/reindex functions and adjust references to it is then impossible.

Yes, having a way for opaque/extension Values to be able to refer to nodes in the Hugr does seem useful.

[zrho]

Still curious as to how the "translation from static values into runtime ones" would work for FuncDefn nodes into consts.

We'd have a static value that refers to a FuncDefn. This could be by name, by node id, or by static port. This is then a static value. The parameters of the FuncDefn become function arguments via the static function type.

Let me illustrate this on examples. We don't have good notation for this, so let me borrow the type theoretic notation of DLNL to write down concrete examples. Say we have a quantum cnot function. In the runtime language, cnot has type $\text{QBit} \otimes \text{QBit} \multimap \text{QBit} \otimes \text{QBit}$. Now we refer to cnot in a term of the static language. This is done via the $G$ modality, and is possible since cnot does not close over any runtime value. So we get a compile time term of type $G(\text{QBit} \otimes \text{QBit} \multimap \text{QBit} \otimes \text{QBit})$.

Static parameters to runtime functions can be expressed with $\Pi$-types of the compile time language. Consider for example a function qft that takes a natural $n$ and an array of $n$ qubits, and then performs QFT on it. This function would then have type $\Pi_{n : \mathbb{N}} G(\text{Array}(\text{QBit}, n) \multimap \text{Array}(\text{QBit}, n))$ when expressed as a term. In particular, I first need to apply it to a static natural in order to use it.

Note that this can still remain in a very tractable fragment of dependent types since qft in the term language would be a uninterpreted function symbol for the purposes of the type system.

[acl-cqc]

Now we refer to cnot in a term of the static language. This is done via the $G$ modality, and is possible since cnot does not close over any runtime value. So we get a compile time term of type $G(\text{QBit} \otimes \text{QBit} \multimap \text{QBit} \otimes \text{QBit})$.

Ok, so we have a Term referring to that FuncDefn node, as FuncDefn's necessarily never depend on runtime values. The compile-time term thus has a "type" much the same as that of the "static" outport, an EdgeKind::Function much as you describe...

I guess we then parametrize Call by the function, rather than having this "static edge", too. But edges have the advantage of being able to, say, quickly see that a function has no uses (or only one use), and/or whether it's recursive. So we'd probably want some kind of indexing over static terms so you can see uses; or can these static "references" to nodes be integrated into portgraph???

[zrho]

One thing I am not yet quite sure about is whether it is best to separate runtime and static types. Is the type of runtime naturals the same as the type of static naturals? DLNL has universes $U_i$ for the non-linear language and $L_i$ for the linear language. Since we're not a proof assistant, type in type is fine, so in our case that would be a static universe $U$ and a runtime universe $L$ such that $L: U$ and $U: U$.

I have a vague feeling that the copyable/all bounds, and the split between Type on one side and TypeArg/TypeParam on the other both try to do something in that direction, but I don't quite see it clearly.

[acl-cqc]

I have a vague feeling that the copyable/all bounds, and the split between Type on one side and TypeArg/TypeParam on the other both try to do something in that direction, but I don't quite see it clearly.

I'm pretty sure they do; we try to separate kinds (à la TypeParam) from Types from runtime-values, but I agree it gets pretty baroque and hence probably does not work out quite as cleanly as one would like. Would be good to make this more precise.

[acl-cqc]

I do like a three-level stratification though:

1. TypeParams are types of variables in the static language, i.e. they describe:
2. TypeArgs (including Types) are values in the static language; those that are Types, can describe:
3. Values in the runtime language (not really represented, although some are Values)

These are roughly just kinds - types - values, but the boundaries get broken down a bit by the extension system....

[zrho]

Yeah, that's how I've come to read it. The boundaries between TypeParam and TypeArg break down even further though with polymorphism and types lifted to kinds. A TypeParam that is a fixed length array suddenly depends on a TypeArg describing its length. That's why I went with a single Term in the model.

[acl-cqc]

The boundaries....break down even further....with...types lifted to kinds

I.e. where we allow parametrization by a (static/constant) value of a type defined by an extension.

Yes, fair point.

1. I should stress that this is/was a backdoor - I would prefer not to design the system around this, rather, this is the escape hatch if you really want to do something crazy that doesn't fit in the system.
2. Note that we no longer have TypeParam::Opaque; since feat!: replace opaque type arguments with String #1328, now we just have TypeParam::String.

Hence, I'd really love to try to make this stratification clearer, rather than merge the levels together and lose it altogether. (I admit your unified-Term might suddenly start to look more appealing if we had Haskell GADTs. Ho hum....)

[zrho]

This is an idea on how to express something like const nodes without having to have runtime values. Consider the following operation:

(define-operation core.const
  (forall ?runtime type)
  (forall ?static static)
  (forall ?ext ext-set)
  (param ?value ?static)
  (where (core.make-const ?runtime ?static ?ext ?value))
  (fn [] [?runtime] ?ext))

This operation produces a runtime value of type ?runtime from a static parameter ?value of type ?static. The core.make-const constraint indicates the requirement that it must be known to be possible to create a runtime value from the given static value. Moreover it can control that producing the value is only possible in the context of some extension.

[zrho]

The result of a conversation with @acl-cqc: hugr-model already has a static type (quote t) for every runtime type t. A term of type (quote t) is a static description of how to produce a runtime value of type t. This can be combined with custom constructors to create a nice mechanism for constants.

The quote type is currently used for function definitions: A function definition does not merely define a single function, i.e. a single value of type (fn ?ins ?outs ?exts), but it defines a "factory" that can instantiate a fresh copy of the function every time it is mentioned. We therefore give the function definition a type of the form (quote (fn ?ins ?outs ?exts)).

We can use quote types for more: a static description of how to produce a runtime value, after all, is exactly what we want to do with constants! So we could define a constant operation as follows:

(declare-operation core.const
  (forall ?t type)
  (param ?c (quote ?t))
  (fn [] [?t] (ext)))

But how do we produce terms of type (quote ?t), apart from functions? Here's where custom constructor declarations come in. Via constructor declarations, we can create new terms. We can use this to create new terms of quoted types:

(declare-ctr arith.u64-const (param ?v nat) (quote arith.u64))
(declare-ctr arith.u32-const (param ?v nat) (quote arith.u32))
(declare-ctr quantum.comp-basis (param ?v bool) (quote quantum.qubit))
(declare-ctr quantum.hadamard-basis (param ?v bool) (quote quantum.qubit))
(declare-ctr tierkreis.protobuf-graph (param ?protobuf bytes) (quote tierkreis.graph))

To make this work with the extension sets system, the quote type would need to be adjusted to take an additional parameter: Then (quote t e) would be the static type of descriptions of how to produce a runtime value of type t in a context that supports the extension set e.