Type level arithmetic

[mark-koch]

Users have asked for generic types like array[qubit, n + 1]. This are some thoughts on how we could achieve that.

Proposal

Allow arbitrary arithmetic expressions made up of +, -, *, //, ** as type args. Arithmetic expressions only unify if they are exactly the same (in the future, we could make this smarter by implementing some kind of normalisation strategy).

def foo(xs: array[qubit, 2 * n]) -> None: ...

def bar(xs: array[qubit, n + 1]) -> None:
    ys = array(*xs, *xs)  # Type: array[qubit, (n + 1) + (n + 1)]
    foo[n + 1](ys)  # Error: expected `array[qubit, 2 * (n + 1)]`, got `array[qubit, (n + 1) + (n + 1)]`

However, users may convince the type checker by adding explicit asserts:

def bar(xs: array[qubit, n + 1]) -> None:
    ys = array(*xs, *xs)
    assert comptime((n + 1) + (n + 1) == 2 * (n + 1))
    foo[n + 1](ys)

These asserts are checked during monomorphisation:

def bad(xs: array[array, 2 ** n]) -> None:
    assert comptime(2 * (2 ** (n - 1)) == 2 ** n)  # Not true for n == 0 since `0 - 1` underflows for nats
    foo[2 ** (n - 1)](xs)

def main() -> None:
    bad[1](array(qubit(), qubit()))
    bad[0](array(qubit()))

The second call to bad would fail during monomorphisation.

Pros

• Not too difficult to implement
• The assert escape hatch gives users the opportunity to express whatever they want.

Cons

• Programs that type check can fail during monomorphisation. E.g. a library could type check, but then fail to compile when invoked with arrays of some specific length
• Doesn't refine across control-flow:

  def bar(xs: array[qubit, n]) -> None:
      if n % 2 == 0:
          assert comptime(2 * (n // 2) == n)
          foo[n // 2](xs)

  Users might think that this is fine since the assert is guarded by the if, but this would still fail during monomorphisation since the if guard is not taken into account. To support this, we would need a length cast that is executed at run-time rather than compile-time. To explain this to users, we should probably frame this feature as "Zig/C++ templates" rather than "dependent types".

Questions

Should we monomorphise in Guppy or Hugr? Doing it in Hugr would require generalising array ops (e.g. pop_left: arrar<N, T> -> T, array<M, T>) and adding casts. Doing it in Guppy would slow down the compiler but allow for nicer error messages.

Alternatives

We could restrict to a decidable fragment of arithmetic (e.g. Presbuger arithmetic or Brat's arithmetic language). However, my feeling is that users would not be super happy with that.

[scercelescu-QNT]

This would also enable popping from arrays while maintaining static memory allocation pop : Array n a -> (a, Array (n-1) a).

[ss2165]

In many cases where one would use type level arithmetic you can just use python wrappers instead:

clunky but workable

from guppylang import guppy
from guppylang.std.builtins import array, py, result
from guppylang.defs import GuppyFunctionDefinition

T = guppy.type_var("T", copyable=True)
def n_double(n: int) -> GuppyFunctionDefinition:
        
    @guppy
    def foo(ar: array[T, py(n)]) -> array[T, py(2*n)]:
        out = array(ar[i%py(n)] for i in range(py(2*n)))
        return out
    return foo

double3 = n_double(3)
@guppy
def bar() -> None:
    a = array(0 for _ in range(3))
    a = double3(a)
    result("a", a)
bar.check()

[CQargi]

In guppy-algorithms, I have experimented with a templating decorator to carry out monomorphisation in python to allow:

• Usage of type information (like n) in comptime
• Type level arithmetic (this was not my main goal and I did not try covering this, but it could possibly be also used for this)

I decided not to merge or use it, so I wanted to write a record of it here.
It had the following syntax

@guppy_template(replacements={"n": range(2, 50)})

and this decorator is identical to guppy when there is no replacements.
It generated all the specialisations of the template for the given range of values for a given type symbol. Other symbols are left as generic.

[ss2165]

Many "template" like use cases outlined here should be addressed by #1299