Function polymorphism

[acl-cqc]

Operations defined in resources are polymorphic over types.

Are functions (defined in Hugrs) also polymorphic? Or are they monomorphic?

This also determines what happens to type variables, i.e. ClassicTypeHashableType::Variable.

If functions are polymorphic, we need to indicate what type (variables) are bound by each function; and we should probably move Variable into Container, alongside Alias, reflecting that we can have variables that are constrained to each TypeTag.

If functions are monomorphic, then I think type variables can be removed from the SimpleType hierarchy - they exist only within the "YAML Type Scheme Interpreter", in its own internal representation of type schemes; the Hugr sees only that it passes some TypeArgs to the YSTI and gets back a Signature (sans variables).

[acl-cqc]

Another possibility is we (somehow) have only monomorphic graphs in core, but we have some kind of polymorphic graph type as an opaque type in the Tierkreis extension (with its own, internal, encoding of type variables - so probably repeating much of the core type system PLUS variables, but at least it keeps variables out of core).

Then either indirect_call includes type application (maybe even involving type-arg inference - fairly simple if it's not unification-based just "single substitution"); or there is a separate type_apply that takes one of the opaque polymorphic graphs and produces a "core" monomorphic ClassicType::Graph. In both cases, we are greatly assisted that computing a signature is a fallible operation implemented by extension binary code...

[acl-cqc]

Discussion today - I think this might be enough to mark the discussion "resolved" and convert to a tracking issue but I'll post here now:

• Allow Graph Types to declare their bound variables (and hugrs - if each hugr has a graph type describing itself, that'd do).
  • These can only occur (a) within the Graph Type binding them, (b) within the corresponding hugr too
• Type application can be explicit, but we could also make call nodes do some "inference" on a polymorphic Graph implicitly - nothing as complex as unification, just checking the substitution (instantiation) from the called graph's typeparams to the types of actual arguments is consistent. (No substitution/instantiation applied to argument types - they'd have to have explicit type_apply operations if req'd.) That is, we can implicitly infer some type_applys, but only some, rather than making them all explicit. IF we want.
  • I'm leaning towards making them all explicit...

Otherwise I think we are looking at:

• struct GraphType { inputs: TypeRow, outputs:TypeRow, resource_delta: ResourceSet }. ). Note no binders or free type variables here. This is the input to a call. That is, three tasks:
  • Remove static_input from AbstractSignature and add that as separate, special, thing for load_constant/call nodes only
  • Then rename AbstractSignature -> GraphType
  • Change OfDef::compute_signature, which currently returns a tuple of those three things, to return a GraphType
• Op signature is then a GraphType (possibly plus static input?); Node signature is a GraphType + static_input + input_resources.
• struct PolyGraph { params: List<TypeParam>, type: GraphType }, where the type may contain type variables referring to those params. This suggests variables have names that aren't strings. We could perhaps make params a Map from String if we want, but that goes against what we've done for Sum and Tuple. Note this PolyGraph describes the static_output of a FuncDefn or graph constant, i.e. is the thing in a Type::Graph.
  • Alternative is thus to make GraphType == PolyGraph, and enforce that the params list is empty whenever a PolyGraph is used as the signature of a node/op, but I think that's a bit ugly, and Graph::Type is far enough away from Node/Op that we can share a common struct between the two.
• type_apply (aka instantiate perhaps?) takes as input a PolyGraph<...>, has some list of static typeargs, and returns either a GraphType (if a TypeArg provided for every TypeParam) or a PolyGraph (i.e., partial application). Note I think type_apply here is probably NOT definable as an OpDef, only the core has enough flexibility to compute its Signature, because the type params + type args of the type_apply depend upon the type of its value input - type_apply really is a "method" of PolyGraph with a signature depending upon the PolyGraph in question. That is, you compute the Signature of a type_apply node from a PolyGraph and a list of TypeArgs that depend upon the PolyGraph.
• OpDef changes significantly. At present the list of TypeParams is stored outside the SignatureFunc. Instead the SignatureFunc can be either a PolyGraph (==> the typeparams are taken from that), or a custom binary function (with a list of typeparams). When we parse a YAML resourceextension definition, there are two (three?) cases
  • List of type params, no type scheme, but CustomSignatureFunc provided by extension (binary code)
  • List of type params, type scheme ==> YAML interpreter produces a PolyGraph, and then plays no further role; "type scheme interpretation" is done by type_apply with all arguments provided
  • (?) List of type params, "extended" type scheme ==> YAML interpreter implements CustomSignatureFunc - this is only if we want to allow additional flexibility in YAML type schemes beyond simple substitution. For example, substitution allows a type like foo<N: USize>(x: Array<Bar, N>) -> (y: Array<Bar, N>) but does not allow varargs qux<N: USize>(args: Bar^N) -> ...

[acl-cqc]

I think the uncertainties here mostly relate to "how to specify/enforce the types that are monomorphic"...

[acl-cqc]

Ok, so there is a bigger issue, still, relating to the difference between graphs ("type application" by substitution into a schema) and ops ("type application" by custom binary code).

Say we have a graph polymorphic over a type or indeed over a USize. How do we typecheck the graph (or indeed, do we not typecheck it at all)? There are two main options:

1. We avoid calling compute_signature on any custom ops until concrete types/sizes are substituted in for the type variables. This allows maximum flexibility in many places, but has one big drawback: type_apply (aka instantiation) can fail, as the custom compute_signatures can reject the concrete type arg, and/or compute types that do not "check".
2. We call compute_signature passing the type variable, and compute_signature is allowed to return a signature containing that type variable. That type variable will then be processed via substitution later. Whilst this works very "smoothly", it effectively means binary compute_signature cannot do anything more than substitution (as the result of calling compute_signature with a tyvar and then substituting something else for the tyvar, must surely be the same as calling compute_signature with that something else in the first place...?)
   • Perhaps this might work if type variables in higher-order graphs can only be types, not usizes or other TypeParams. So an OpDef is no longer equal to a PolyGraph. This might be a reasonable compromise. However, note that this does not allow a Graph polymorphic over Arrays of different length, say.

Another concern is if we wanted a Graph polymorphic over different widths of integer from the arithmetic extension. This requires checking that the width (usize) argument to the graph is valid for the individual arithmetic operations, which (according to compute_signatures thereof) tests that the width is in a specific set of legal widths. We can't do that for a variable.

This suggests to me that type_apply is fallible (exactly as compute_signature is fallible) might be the only way to go...?

• In which case we might want to either allow FuncDefn and const nodes to return statically-monomorphic graphs, or set GraphType==PolyGraph (with no typeargs), such that we can call without invoking type_apply

[acl-cqc]

Or, ok, another compromise. Split OpDef into two stages: Static parameters to OpDef, which must be instantiated by static TypeArgs (no type variables, even in a polygraph). This performs custom binary compute_signature, then returns a polymorphic graph. Arguments to polymorphic graph can be types or values, but are only substituted in.

Roughly, this translates as - rather than an OpDef being either a custom binary compute_signature or a PolyGraph - instead it is both. (If no.custom binary is provided, then we have a fixed/serialized/constant PolyGraph instead.)

Still a compromise: we can substitute into types (as we have no custom binary validity check there), and we could be polymorphic over array sizes or even tensor rank (no, e.g., sum over the first dimension), but we cannot be polymorphic over e.g. arithmetic-extension integer width (as that requires computation).

[acl-cqc]

And the "type_apply may fail" approach is, roughly, monomorphization - we can do type application at Tierkreis runtime, but for anything compiled down to binary code, we'd have to do all type_apply in the compiler first. Indeed, we have to do all custom-binary compute_signature in the compiler first under all approaches...

[ss2165]

I'm leaning towards:

Polymorphic functions in core HUGR is too much for an IR. They will be very useful in Guppy, but for HUGR purposes some level of templating over types in the tooling (with something like PolyGraphType as an internal struct that can be type-applied) is enough.

If we need it, we can take your polymorphic-extension-type function later and use binary type computation.

If there are use cases for which we definitely need polymorphic functions in core that I'm not recalling, please let me know.

[acl-cqc]

More discussion today. There are a few arguments for supporting something like this in core hugr.

• Parametric polymorphism (by infallible substitution of values for type arguments) is a core notion in functional programming (much like "size" is a core notion in low-level compilation), and Tierkreis is as much a client of Hugr as TKET is.
• It enables functions (Hugrs) to be almost as expressive as OpDefs (no custom binary compute_signature, but the same parametric polymorphism for which we have proposed YAML syntax in extensions). We can only really do this in core Hugr because there is an extra step of dependence: each polymorphic graph type requires its own OpDef, one cannot express a single OpDef that is (infallibly) correct for all polymorphic graph types and arguments to them (because the legal arguments depend upon the type parameters to the graph).
• Concretely, there are two kinds of errors that would be easier to detect if we supported polymorphism in core Hugr:

1. Applying binary compute_signature is fallible, and we would like to rule out failures at runtime. This is perhaps not so great a reason if we consider that many compute_signature impls are in fact infallible substitution, so we can perhaps lean harder on extension writers not to fail.
2. Passing a TypeArg that's the wrong kind for the declared TypeParam is a user programmer (not extension-writer) error, that we could catch statically (without doing anything as expensive as invoking compute_signature for every possible combination of TypeArgs that could ever result).

[acl-cqc]

Proposal 1

• FunctionType has a list of binders, over which it is polymorphic, each a TypeParam; type variables referring to these binders appear within the FunctionType. (They could also appear within a Hugr claiming to have that type.) Nomenclature is up for grabs but the case of >0 binders might be called a PolyGraph (and FunctionType might specifically mean "no binders").
  • It is easy to check that each variable appears only in a place where it has the correct kind (e.g. a variable bound by a TypeParam::USize can be used as the size of an array but not the element type; a variable bound as a TypeParam::Type(TypeBound::Copyable) can be used where an Any or Copyable type is expected but not where an EqType is expected)
  • We also have an function that applies a substitution to produce an actual type/signature. This can fail only when the wrong number of TypeArgs are supplied, or a "bad" TypeArg is passed (as per check_type_arg - e.g. passing a USize for a variable declared as requiring a type); both of these failures can be statically ruled before the actual TypeArgs are available (which happens only at Tierkreis runtime).
  • Finally, we'll have a similar thing that applies such substitutitions to actual Hugrs (this involves substituting TypeArgs into Ops and thus calling compute_signature and so is fallible)
• There is an operation of "type application" parameterized by (TypeArgs/TypeParams): (1) a PolyGraph type, or some expression thereof, and (2) some number of TypeArgs (dependent upon the binders of the particular PolyGraph given as first argument, hence this cannot be an extension OpDef) - perhaps always exactly one such. These are used to compute a runtime signature: the input is a PolyGraph (a Hugr) whose type is the first static parameter, the output is either a PolyGraph or a FunctionType: computed by applying infallible type substitution of the TypeArg (2) for the first binder of the polymorphic type (1). Instances where the output has no remaining binders (i.e. a FunctionType) might be called concretize to distinguish from partial type application producing a PolyGraph with fewer binders.

Note (limitation): does not rule out compute_signature failures at Tierkreis-runtime

[acl-cqc]

Simpler Non-proposal 1a

• Allow parameterization only by types of a single tag, e.g. Any.
• The parameters to "type application" no longer have dependence: there is always a representation of a PolyGraph, and a type. Thus, the TypeParams to type-application are fixed, and this can be defined as an extension OpDef. (The output can still be a PolyGraph or a FunctionType, but this is computed given the TypeParams by applying substitution, so that works ok)
• However, we cannot parameterize over, say, array lengths ==> I argue this is not expressive enough

Simpler Non-proposal 1b

• Type variables do not declare a kind of TypeParam; you can pass a USize when a Type is expected, or vice versa, etc. etc. (That is, substitution could produce malformed non-types like "An Array of length whose elements are 5").
• Again this allows type application to be an extension OpDef: its TypeParams are (1) the PolyGraph type, and (2) an opaque value representing the argument (that could be a type, a USize, etc. etc.)
• However, type application can fail at runtime with "wrong kind of type argument" - a user programmer error that we would like to rule out statically ==> I argue this does not provide desired type-safety guarantees

[acl-cqc]

Proposal 2

This strengthens Proposal 1 above to rule out runtime failure of custom binary compute_signature.

Beyond Proposal 1, we extend OpDef's compute_signature to allow returning a PolyGraph - that is, OpDef's that provide a binary compute_signature can first perform arbitrary computation on some TypeParams statically declared by the OpDef; then the returned PolyGraph can parametrize further over type variables bound therein (by infallible substitution). OpDef's that don't provide a binary compute_signature just have a fixed PolyGraph.

We then statically enforce that all arguments passed to compute_signature are closed (no free type variables). All compute_signature can then be done in advance (once only), leaving only infallible substitution to happen at Tierkreis-runtime. It is perhaps worth exploring why this restriction is necessary - it is so that we do not have to rerun compute_signature at runtime when a new type/value in substituted in for the type variable. For example, compute_signature(Array<tv_1, tv_2>) might perform some structural inspection of Array and output some signature dependent upon that (perhaps containing tv_1 and/or tv_2 for later substitution). However, we would expect compute_signature(tv_3) followed by simple substitution tv_3 -> Array<tv_1, tv_2> to produce the same result, and it cannot, as the simple substitution does not invoke the binary code of compute_signature for that to ever see the Array.

(That is, if a type variable could be passed in as a TypeArg to a particular TypeParam, simple substitution for that typevar is all that can happen at runtime, so it is all that compute_signature can be allowed to do statically. Thus, compute_signature should just return a PolyGraph with that TypeParam declared there instead.)

[croyzor]

we extend OpDef's compute_signature to allow returning a PolyGraph - that is, OpDef's that provide a binary compute_signature can first perform arbitrary computation on some TypeParams statically declared by the OpDef; then the returned PolyGraph can parametrize further over type variables bound therein (by infallible substitution). OpDef's that don't provide a binary compute_signature just have a fixed PolyGraph

This doesn't make sense to me. Substituting type arguments into the PolyGraph should be part of the "arbitrary computation on some TypeParams". At which point we either:

• return a graph type which has extra parameters, not listed in the op's type params
• return a closed graph (the same behaviour as we'd expect now?)

[acl-cqc]

The point is that while "arbitrary computation" could indeed include substitution, it's useful to separate out the substitution from the more general case because we know the former is infallible but the general case is not?

[acl-cqc]

i.e. to get the OpDef "superpower" (afforded only to OpDef's not Hugrs) of doing type computation that isn't just substitution, done and out of the way at compile-time

[cqc-alec]

When I think of examples where function polymorphism is useful, there is almost always some further parametrization beyond merely the free type, usually an associated operation with certain properties. For example, a "sort" function requires a type with a (suitably constrained) order relation. Have we thought about how such "parameters" would be passed around?

[croyzor]

The other week there was some allusion to achieving interfacey things by using higher order functions - i.e. sort takes an Array<T> and a graph [T, T] -> [Sum((), (), ())] which is the sorting function (or, say, [T, T] -> [bool] for an equality function), but I don't think we've formally settled on an answer to this

[acl-cqc]

That's the sort of thing I was thinking of, yes - we are already thinking of doing this for Map, right?

[acl-cqc]

Besides runtime failure of compute_signature, there is another problem that the two-stage method in Proposal 2 solves: what if compute_signature computes a signature with an unexpected number of ports? We could do the fallible version of substitution on a Hugr and end up with signatures for every node but missing (or meaningless unconnected) wires...

[acl-cqc]

(Or other typechecking errors, e.g. just mismatched ports connected by a wire; whereas we know that applying substitution uniformly across a Hugr preserves type-correctness)

[mark-koch]

Proposal 3

No polymorphism in Hugr.

There are certain type system features from frontends that we don't want to support in the IR (e.g. dependent types from Brat). We could treat polymorphism as one of those non-supported features and make it entirely the frontend's job to do type checking and rule out runtime errors. To this end, we could use an Any type to circumvent the Hugr type system. Similarly, Tierkreis wouldn't know about polymorphism either and produce a runtime failure when something goes wrong (which hopefully doesn't happen if the frontend is doing its job...)

I think one of the questions to consider is whether supporting polymorphic types in Hugr would enable optimisations that we want to do that would be harder otherwise?

[cqc-alec]

We should also consider adopting Proposal 3 (HUGR is monomorphic), and leave open the possibility of a future polymorphic HUGR 2.0. It's not clear to me how much we gain from having this feature in the IR, and how much extra complexity it would add.

I think one of the questions to consider is whether supporting polymorphic types in Hugr would enable optimisations that we want to do that would be harder otherwise?

I actually can't see that it would. Any optimization pass that you can do on a polymorphic function you can do on its monomorphization, and you'd probably want to anyway to take advantage of the specialization.

[ss2165]

Any optimization pass that you can do on a polymorphic function you can do on its monomorphization, and you'd probably want to anyway to take advantage of the specialization.

I think the issue with using Any types to circumvent the HUGR type system is exactly that you can't do this monomorphization + optimization. (i.e. if I just know that I've popped "Any" from a list I can't do as much as if I'd popped "Qubit"). There are arguments here about the front end also adding diligent coercions to aid the optimizer.

[acl-cqc]

Not a full response but a few thoughts. Firstly, monomorphization. There are two possible routes.

1. Statically - compute every possible concrete instantiation in advance. There are two downsides: space (code bloat) and time (if you optimize all of them) - noting that many of these may never be used at runtime. (Indeed, you can write programs where the set of possible instantiations is unbounded, but of course only a finite subset of these will ever be realized in a program that runs in finite time.) One upside is all compute_signatures are then done statically so there is no possibility of runtime failure (downside, if any of those fail statically - that instantiation might never have occurred at runtime!)
2. At runtime, as you go - so we monomorphize when the program creates an instantiation, and then JIT-compile. Upside, space. Downside, you are doing expensive compilation at runtime.

Both of these we need to think a bit about when compile-time / runtime happens - do people connect to Tierkreis and submit a polymorphic graph to run (which the server then compiles), or can we compile in some way in advance. We might also note the experience of e.g. Java, where runtime profiling has been very effective in optimizing higher-order programs with indirect jumps/calls.

I think there will also be "wins" from optimizing polymorphic graphs - before monomorphization - of course those wins could likely be repeated on each instantiation, but you'd have to find them many times over. Here "Any" is likely to be all but useless!

If we are statically monomorphizing, and all optimizations on polymorphic graphs are done by the frontend before passing monomorphized version to the backend, then we're ok (and don't need "Any"!). But in any other situation (e.g. JIT) the backend optimizer/runtime is likely to want all the type information the frontend had. So the "true" types (not erased) will be passed from the frontend alongside the Hugr in a separate structure (a Map<Port,PolyType>, say) to be read in by the backend - metadata perhaps. That's a bit ugly (and raises questions why our current types aren't in metadata too). Moreover, the frontend's type system is likely to have to include/duplicate the Hugr type system as a subset (+ add the additional checks that don't show up in the erased version).

[acl-cqc]

Proposal 2 above was implemented by #630. However maybe there was a less-polymorphic intermediate that we didn't consider.

• FuncDefn's can bind TypeParams used in their own bodies, and their own "type signatures". (Presumably FuncDecl's too, and maybe AliasDefn/Decl's).
• Thus, the "static output" of FuncDefn has a polymorphic type(-scheme)
• But, the Type hierarchy has only monomorphic function types.
• So, we have to make EdgeKind::Static and EdgeKind::Value significantly more different than they are at present
• The TypeApply operation introduced in feat: polymorphic function types (inc OpDefs) using dyn trait #630 is now combined into the Call operation - which takes a static input from a FuncDefn, and a list of type arguments, and then (using the TypeApply code i.e. substitute) computes its runtime Signature. This is as shown in PR feat: make FuncDecl/FuncDefn polymorphic #692, so building on top of that PR we could drop the TypeApply op altogether.

This is a lot like ML, etc. - "TLDs can be polymorphic but nothing else". No polymorphic lambdas. (If you want to make a lambda, i.e. a Graph, that calls a polymorphic function, the lambda has to instantiate that by supplying a list of TypeArgs - I'd say "fixed list of TypeArgs", they could contain type variables but only in that a call inside the body of a FuncDefn can use type variables declared by it's ancestor FuncDefn). So, not as expressive. But expressive enough to capture the primary use case, higher-order "standard library" graphs for Tierkreis.

In terms of code complexity, we get to drop the funky cases of substitute (InsideBinders, Renumber), which is definitely good news. We still have to keep the concept of TypeApply (but inside call), we still have to declare a list of binders (in FuncDefn and perhaps elsewhere). I think there may well be more code, in order to treat Static and Value edges differently.

Why didn't we think of this? Well, we were thinking about the Tierkreis standard library use case, but I don't think we really talked(/thought) about the other big change that Hugr brings from TierkreisGraph, i.e. the ability to have a load of FuncDefns/TLDs....

[acl-cqc]

(I'm not sure I understand the current situation with other_input and static_input but that might want to change too.)

[acl-cqc]

So if the goal here is to make this simpler for end users, by changing the Type hierarchy to include only FunctionType not PolyFuncType, then that's one thing. There is a corresponding loss of expressivity but I admit the utility of higher-order closures may be small.

If the goal is to simplify substitute and replace the Substitution trait with a simple &[TypeArg] (say), however, we may need to be more careful. #692 adds binders to FuncDefn's, allowing nested FuncDefn/cl's to refer to type variables declared by their enclosing FuncDefn, or indeed anywhere else outside (e.g. we may want "free" variables for ExtensionSets to replace the current notion of "variables" in extension inference). Applying substitution across the outer FuncDefn (e.g. to "run" the outer function in Tierkreis) would thus require some InsideBinders fun to correctly handle the inner FuncDefn. So if the goal is to remove the Substitution trait, we should probably insist that nested FuncDefn/cl's are not able to see any enclosing TypeParams.

[mark-koch]

While discussing the collections extension (see #725), we found a situation where TypeApplys might be necessary:

Let's say we want to define a polymorphic sorting function for lists that takes an ordering predicate as an extra argument. If we want to use this function to sort a list of lists, we might want to use an instance of a polymorphic list ordering predicate(e.g. lexicographical). However, without TypeApply, we couldn't feed this predicate into the sorting function.

The same holds true for polymorphic functions that need hashing, or any other interface on its type arguments (except for equality, which is built into the hugr).

[acl-cqc]

So sort here is a top-level function, and is polymorphic over the element type of the list. When you call it, you specialize it to an element type, e.g. list[inner], and provide a monomorphic comparison function (list[inner], list[inner]) -> bool (or whatever). If sorting over nested lists, the monomorphic comparator must be the result of calling (and type-applying) a polymorphic top-level lexicographic: forall e. ((e,e)->bool) -> ((list[e], list[e]) -> bool). To convert lexicographic into an actual comparison function, you not only need to "type-apply" but also provide a value for the underlying-element comparator, which is to say, you need to partially-evaluate it with both type and value arguments.

We don't have a construct for actually doing partial-evaluation at the moment (that'd be a Tierkreis thing), but again partial is a polymorphic TLD** with lots of monomorphic args:

// User-provided TLD's
sort: forall e. ((e,e) -> bool), list[e] -> list[e]
lexicographic: forall e'. ((e',e') -> bool) -> ((list[e'], list[e']) -> bool)

// Need to generate code for:
sort_nested: forall s. ((s, s) -> bool), list[list[s]] -> list[list[s]]
   // roughly: (f,lst) => let comparator = lexicographic[s](f) in sort(comparator, lst)
   // thus, define monomorphic constant graph (monomorphic because within "sort_nested", *s* is a valid type)
   let comp :: (s->s) -> (list[s] -> list[s]) = Constant(Graph( f => lexicographic[s](f) ))
   // now we can:
   sort[list[s]](partial(comp, f), lst)

** I think the bigger issue here may be that I'm not sure we have enough flexibility in the Hugr type system to define partial as an extension op. I think we may need some new things like concatenating rows/lists of types within TypeParam/TypeArg etc. to define that. But perhaps if everything is curried and partial only supports specifying the first parameter, we're ok.

[acl-cqc]

I think the general principle to stress here is that if you want to "type-apply" then you are necessarily type-applying types to a TLD (because nothing else takes type arguments), and even if you have no value arguments at the same time, you can do this via a monomorphic constant graph (not Func) that takes the value-arguments and then calls the TLD with the type-arguments (fixed in the constant-graph) and those value arguments.

The key to that being that within a polymorphic TLD, monomorphic constant graphs (but not nested Funcs) can refer to type arguments of said containing TLD

[acl-cqc]

Conclusion will be enacted by #904