Signature Metaprogramming & Monomorphisation

[mark-koch]

The Problem

Guppy offers powerful metaprogramming capabilities within function bodies via the comptime feature. However, the signature of those functions is static and cannot be set programmatically (except for basic things like array lengths that can be set using comptime expressions). This can be quite limiting: For example, we might want to write a library function that takes an generic number of qubit registers, each with a generic size. This cannot be expressed at the moment.

Proposal

Comptime types

Using the current syntax, we should allow type-level comptime expressions that evaluate to types (instead of just values). In particular, this will require a Python runtime representation of Guppy types:

def make_type(n: int) -> guppytype:
    """Python function that returns a Guppy type""" 
    if n % 2 == 0:
        return array[int, n]
    return float

@guppy
def foo(x: comptime(make_type(42)), x: comptime(make_type(43))) -> None: ...

Generic Programming & Monomorphisation

To allow generic programming, these type-level comptime expressions must have access to the generic parameters of the function as python values:

@guppy
def bar[n: nat](x: comptime(make_type(n)))

For this to work, we have to monomorphise these generic value parameters during type checking and each version needs to be type-checked separately.

To maintain a bit of parametricity, we should prohibit inspection of type parameters for now, so those will not need to be monomorphised:

# The following is not allowed: The value of `T` cannot be inspected
def not_allowed[T](x: comptime(float if T == int else T)) -> None: ...

Example

The example mentioned in the introduction involving a generic number of qubit registers, each with a generic size would look as follows:

@guppy.comptime
def example[N: nat, LENS: frozenarray[nat, N]](
    registers: comptime(tuple[*(array[qubit, LEN] for LEN in LENS)])
) -> None: ...

@guppy
def foo(qs1: array[qubit, 3], qs2: array[qubit, 10], qs2: array[qubit, 42]):
   example[1, [3]]((qs1,))
   example[1, [4]]((qs1,))  # Error: expected `tuple[array[qubit, 4]]`
   example[2, [3, 10]]((qs1, qs2))
   example[3, [3, 10, 42]]((qs1, qs2, qs3))

Note that example is a comptime function, otherwise registers would be barely usable since tuple indexing must be static. With inline comptime sections, this could be localised further.

Variadic functions

Using the syntax so far, the total number of parameters is still fixed (that's why we had to use tuples in the example above). This could be fixed using Python's *args syntax:

def example[N: nat, LENS: frozenarray[nat, N]](
    *args: *comptime(tuple[*(array[qubit, LEN] for LEN in LENS)])
) -> None: ...

The *type syntax was introduced in Python 3.11. The backwards-compatible version would use Unpack.

Follow-up: Types are comptime by default?

If we go with this propsal, a potential follow-up would be to make all type annotations comptime by default. This would declutter the syntax and make things more uniform: The static type-language of Guppy would just become Python!

Discussion

Benefits

Monomorphising value parameters in Guppy would also have additional benefits:

Type-level arithmetic

The monomorphisation approach discussed here would also immediately solve our previous problems with expressing type-level arithmetic (see #785). Previously, users had to rely on the workaround of wrapping Guppy functions into Python functions:

def make_concat(n, m):
    @guppy
    def concat[T](
        xs: array[T, comptime(n)], array[T, comptime(n)]
    ) -> array[T, comptime(n+m)]: ...
    
    return concat

With this proposal, the static n, m parameters can just be turned into generic parameters and the compiler will monomorphise it for us:

@guppy
def concat[T, n: nat, m: nat](
    xs: array[T, n], ys: array[T, m]
) -> array[T, comptime(n + m)]:
    return array(xs[i] if i < n else ys[i-n] for i in range(comptime(n+m)))

Generic comptime functions

A long outstanding feature are generic comptime functions. We haven't implement them yet since comptime requires knowledge of array sizes to turn them into Python lists. If all value params are monomorphised, this becomes very easy to support!

Accessing generic parameters in comptime expressions

Furthermore, monomorphisation allows us to access the values of generic parameters inside comptime expressions. This is a feature people have asked for in the past, but would be impossible without monomorphisation in Guppy:

@guppy
def foo[n: nat](...):
    x = comptime(n + 1)

Drawbacks

Performance

The main downside we need to consider is compiler performance. Monomorphising in Python will obviously slower than doing it in Rust. Moreover, this proposal requires that each monomorphisation is type-checked separately!

Type Inference

Finally, note that comptime types will block type inference:

@guppy
def baz[b: bool, T1, T2](x: comptime(T1 if b else T2))

@guppy
def main():
    baz(42)  # error: Cannot infer type parameters
    baz[True, int, float](42)

(That's why generic parameters in Zig are never inferred and always need to be specified.)

Especially if we go with the follow-up of making everything comptime by default, we'll need a way to distinguish cases where type inference is possible vs not. I think a good solution would be to test whether the comptime expression tries to inspect the value of any generic parameters, or if they are only used opaquely. The latter case subsumes all currently possible signatures where type inference is fine.

[GBoydQ]

Really like this proposal! Transformations on generic circuits which may act on varying numbers of registers will be very important

[GBoydQ]

Two important examples come to mind, although there are probably many more,

Amplitude amplification, probably the most important quantum "algorithm":
AA takes a unitary acting on an arbitrary number of registers, of arbitrary lengths, and repeats this along with some reflection operators acting on some set of those registers. In order to write a generic version of AA it seems like would need something that can pass around arbitrary signatures and apply them to arrays of differently sized registers.

Data loading via QROM, the most prevalent way of loading information:
QROM takes a mapping of index->bitstring, and then applies the relevant bitstring depending on the state of some index register.
This is the most basic version, but it is also common for QROM to both act on multiple input registers (a function of multiple variables) and multiple output registers (multiple data that depend on the same values). These can be (and often are) of different sizes.

I'm not familiar with Succ though, could you expand on that?

[GBoydQ]

And pretty much the entire framework of QSVT, where we need to be able to perform polynomial tranformations of block encodings that may act on arbitrary registers (especially as they may be nested, where one BE is constructed from multiple others, including their "main" and ancilla registers)

[NathanCQC]

Any abstract block encoding framework will need to agnostically handle block encodings of arbitrary register numbers of differing sizes. This is super important for us. I cannot see any alternative other than building the signature on the fly.

[acl-cqc]

Succ as in successor: append[N:Nat, T: Type](in: array[T,N] @ Owned, elem: T) -> array[T, Succ(N)]. A more interesting case is the reverse pop[N: Nat, T: Type](in: array[T, Succ(N)] @ Owned) -> tuple[array[T, N], T] where the type system then statically detects/prevents trying to pop from a zero-length array.

If you really need arbitrary number of registers with different registers having different sizes, but your algorithm is parametric (somehow) over that vector of lengths, then yeah, I don't think you'll get there with any decidable statically-checked type system. (You can go dependent types: undecidable statically-checked!) This "signature metaprogramming" says, no static checking; fine if you are willing to run the python and then hope the generated circuit passes checking, e.g. in advance of circuit submission; much less fine if your python circuit-generator falls over with an invalid generated circuit (i.e. guppy type error) on the nth iteration of a hybrid algorithm (e.g. VQE/QAOA, but that generates a circuit each iter, not just tweaks float params).

I will think more about AA (haven't grokked QROM yet), but I don't necessarily see a problem with nesting blocks. I mean, let's think carefully about what we lose if we just express your block as a tuple (parametrized over an inner block/qubit).

[acl-cqc]

Thanks @NathanCQC for the detailed discussion today, will be writing more in due course. Have you seen the proposal for slices? (@mark-koch not sure where this is?) But I think that would deal with some of your concerns, e.g. the block encoding framework, albeit not (I don't think) Amplitude Amplification.

[acl-cqc]

Dependent types!!

Like the idea that all guppy types could be python exprs. Less sure how happy the parser would be with this...would that work??

We already have many situations where guppy compilation could fail because of what the python did so I guess that's not new. This does make the language less modular: a bit like C++ template expansion, type-checking can fail somewhat-unexpectedly if you instantiate with an argument that doesn't quite behave the way that was expected, and it's hard to offer any static guarantees about this; you just have to run the python. (Contrast with say Rust parametric polymorphism, instantiation always succeeds, for any type argument satisfying the constraints/bound on the type parameter decl). So I think that's a drawback, that this proposal doubles down on, rather than trying to reduce/minimize/move away from.

[acl-cqc]

We should be very wary of python functions that access (mutable) global variables - whether they mutate, or just read variables mutated elsewhere. This is python....so we probably just have to strongly discourage this...and be very careful about when (and in what order) these functions are called - specifically, how many times (cache after first call?), and what about monomorphization? Or does polymorphism disappear and instead we write python functions that take a type and define a monomorphized guppy function?

[mark-koch]

Yeah I think there is no way reliably prevent the user from mutating state inside those Python functions

cache after first call?

We could cache for each combination of parameter instantiations, but e.g. in the first example above make_type will need to be called twice

and be very careful about when (and in what order) these functions are called

I think we should just say that those functions must be pure and we make no guarantees to the user how often or in what order they are called 😅

[acl-cqc]

We could cache for each combination of parameter instantiations, but e.g. in the first example above make_type will need to be called twice

If there are two textual calls, we should probably execute both. And of course we will memoize the whole function body produced for the typeargs, that might be the most important thing!.

Of course this relates to the flow of the compiler, which will change quite a bit - we can no longer do typechecking and then monomorphization - and I don't think we can do all monomorphization first either, as typechecking may be required to infer the type arguments with which to monomorphize...so we probably need to interleave both.

But it might be possible to give some guarantees like we'll execute all comptimes within one function body before resolving any of the calls (which might create new callees and repeat the process).

People will want print statements inside make_type for debugging, including seeing what args actually get passed in.

[acl-cqc]

To maintain a bit of parametricity, we should prohibit inspection of type parameters for now

So if you want to do that, can you can get round this deliberate limitation via a much more awkward route of defining a python function, taking type/etc. args, that inspects the type parameters as you suggest (my_computed_ty = float if T == int else T), then returns a monomorphic guppy function that uses comptime(my_computed_ty)?

I mean, if this is an artificial restriction and there is a workaround, then fine, we can see how often the workaround is used. (But it does seem like a two-level system: types are second class citizens alongside first-class nats).