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.