Static compilation and typing¶
Introduction¶
While Guppy functions mostly look like regular Python functions (just annotated with the @guppy decorator), the code they contain is processed differently compared to Python code. You can normally run Python programs directly on your machine, whereas we want to be able to run Guppy programs with a variety of simulators and quantum hardware.
In order to achieve this, programs are statically compiled into an intermediate representation called HUGR. An intermediate representation allows us to optimise programs before further converting them to code that can actually be executed on the desired target.
A big advantage of compilation is that it helps us catch errors earlier than runtime. For example, the compiler ensures that variables are definitely defined before they are used.
from guppylang import guppy
@guppy
def bad_function(b: bool) -> int:
if b:
x = 2 # x not defined if b is False
return x
bad_function.check() # Check fails!
Error: Variable not defined (at <In[1]>:7:11)
|
5 | if b:
6 | x = 2 # x not defined if b is False
7 | return x
| ^ `x` might be undefined ...
Note:
|
4 | def bad_function(b: bool) -> int:
5 | if b:
| - ... if this expression is `False`
Guppy compilation failed due to 1 previous error
However, it also has implications on the information we have to provide in the program, in particular about types.
Type checking¶
You may be familiar with type hints in Python.
def python_function(x: float) -> str: # float and str are type annotations
return f"The value of x is {x}"
Python type hints are an optional feature and not enforced at runtime; they are for static analysis only. Guppy however is strongly typed - code must type-check at compile-time, and ill-typed programs will be rejected by the compiler. For example, observe the error when trying to compile the program below.
@guppy
def bad_function(x: int) -> int:
# Return incorrect type
return (x, x)
bad_function.check() # Check fails!
Error: Type mismatch (at <In[3]>:4:11)
|
2 | def bad_function(x: int) -> int:
3 | # Return incorrect type
4 | return (x, x)
| ^^^^^^ Expected expression of type `int`, got `(int, int)`
Guppy compilation failed due to 1 previous error
It also means variables must have a unique type when they are used:
@guppy
def bad_function(b: bool) -> int:
if b:
x = 4
else:
x = True
return int(x) # x has different types depending on b
bad_function.check() # Check fails!
Error: Different types (at <In[4]>:7:15)
|
5 | else:
6 | x = True
7 | return int(x) # x has different types depending on b
| ^ Variable `x` may refer to different types
Notes:
|
3 | if b:
4 | x = 4
| - This is of type `int`
5 | else:
6 | x = True
| - This is of type `bool`
Guppy compilation failed due to 1 previous error
The Guppy compiler can infer types most of the time, meaning that type annotations are usually only required for function definitions. However, it can be necessary to provide type annotations where the type cannot be determined. An example of this is when initialising nothing in the following program:
from guppylang.std.option import nothing
@guppy
def foo() -> None:
q = nothing()
q.unwrap_nothing()
foo.check()
Error: Cannot infer type (at <In[5]>:5:8)
|
3 | @guppy
4 | def foo() -> None:
5 | q = nothing()
| ^^^^^^^^^ Cannot infer type variables in expression of type
| `Option[?T]`
Guppy compilation failed due to 1 previous error
In this example, the Guppy compiler cannot infer what the type of q should be. To fix this, we can provide a type hint Option[qubit] for the compiler.
@guppy
def foo() -> None:
q: Option[qubit] = nothing()
q.unwrap_nothing()
foo.check()
In the next section, we will introduce generic functions where input and output arguments depend on parameters. This is another example of where type annotations can be necessary to provide the Guppy compiler enough information to determine variable types.
A particularly useful feature of the Guppy type system when it comes to qubits are linear types, which you can read more about in the section on linearity.
Generics¶
Another interesting aspect of the type system is polymorphism. In our case, polymorphism means we can have generic function definitions - functions that depend on parameters, either types or natural numbers.
Unlike normal function parameters which are passed at runtime, type-level parameters are resolved at compile-time. They are placeholders for types, as opposed to data - this distinction is particularly important to keep in mind with natural numbers as not everything that can be done with a function parameter can be done with a type parameter.
Consider for example the identity function which works for inputs of any type. In Python this would work implicitly, as the type would only be determined at runtime:
def identity(x):
return x
In Guppy however, we need to explicitly state that the type is a generic parameter to make the function polymorphic:
T = guppy.type_var("T")
@guppy
def identity(x: T) -> T:
return x
An example of parameters representing natural numbers are functions that are generic over the length of arrays:
from guppylang.std.builtins import array
T = guppy.type_var("T")
n = guppy.nat_var("n")
@guppy
def apply_identity(a: array[T, n]) -> None:
for i in range(n):
identity(a[i])
This function now works for arrays of any length and type! This is possible because the compiler turns each instantiation of a generic function into a concrete instance with specific types in a process called monomorphisation.
@guppy
def main() -> None:
arr1 = array(1, 2)
apply_identity(arr1)
arr2 = array(1.5, 2.5, 3.5, 4.5)
apply_identity(arr2)
main.check() # Check succeeds :)
Normally determining the specific type is done automatically through type inference, but it is also possible to explicitly apply type arguments if needed.
n = guppy.nat_var("n")
@guppy
def foo(x: array[int, n]) -> int:
return n
@guppy
def main() -> int:
return foo[0](array()) + foo[2](array(1, 2))
main.check()
Generics can be particularly useful for parameterising quantum programs by an arbitrary number of qubits:
from guppylang.std.quantum import qubit, cx, measure_array
@guppy
def rep_code(q: array[qubit, n]) -> array[bool, n]:
a = array(qubit() for _ in range(n))
for i in range(n - 1):
cx(q[i], a[i])
cx(q[i + 1], a[i])
return measure_array(a)
rep_code.check()
As we saw in the previous section, it is sometimes not possible for the Guppy compiler to infer types and it is necessary to include additional information through type annotations. This can be the case with functions that have generic return values. Consider the following append function which takes an array of qubits and appends a qubit to the end. In this example, the input array of qubits is of generic size n while the return is of size m.
from guppylang.std.builtins import owned
from guppylang.std.option import some
m = guppy.nat_var("m")
@guppy
def append(q_arr: array[qubit, n] @owned, qb: qubit @owned) -> array[qubit, m]:
q_arr_opt = array(nothing[qubit]() for _ in range(m))
idx = 0
for q in q_arr:
q_arr_opt[idx].swap(some(q)).unwrap_nothing()
idx += 1
q_arr_opt[m].swap(some(qb)).unwrap_nothing()
qs = array(q.unwrap() for q in q_arr_opt)
return qs
When we then call append in from our main program, the compiler will throw an error as it is unable to infer the return size m of the array.
@guppy
def main() -> None:
qb = array(qubit() for _ in range(2))
qb_new = append(qb, qubit())
measure_array(qb_new)
main.check()
Error: Cannot infer type (at <In[14]>:4:13)
|
2 | def main() -> None:
3 | qb = array(qubit() for _ in range(2))
4 | qb_new = append(qb, qubit())
| ^^^^^^^^^^^^^^^^^^^ Cannot infer type variables in expression of type
| `array[qubit, ?m]`
Guppy compilation failed due to 1 previous error
However, as we know the size of the array that should be returned, we can provide this information with a type hint for the compiler:
@guppy
def main() -> None:
qb = array(qubit() for _ in range(2))
qb_new: array[qubit, 2] = append(qb, qubit()) # Type hint added
measure_array(qb_new)
main.check()