Annotations

Silq supports annotations !, qfree, mfree, const, and lifted.

Classical types: !

To indicate that a type τ may only hold classical values (and not superpositions), we annotate it as $!\tau$. This ensures we can freely duplicate and drop values of that type. For example, $1+2$ has type !int[n]. In contrast, H(0) holds $\facs \big(\ket{0}+\ket{1} \big)$ and is thus not classical: It has type 𝔹 and not !𝔹.

Example: The function classicalExample (below) takes two arguments x (a classical Boolean) and f. The latter takes a classical Boolean and returns a classical Boolean. Moreover, f itself is classical, meaning that it is classically known.

def classicalExample(x:!𝔹,f:!𝔹!→!𝔹){
  return f(x);             //  ^ f is classical
}

Example (not classical): The function captureQuantum (below) illustrates a non-classical function. It returns a function captured which captures the quantum variable x. Thus, the state of captured is in superposition, meaning we cannot refer to captured as being classical.

def captureQuantum(x:𝔹){
  captured := λ(). { // function `captured` takes no arguments
    return H(x); // the body of function `captured` applies `H` to `x`
  };
  return captured:𝟙→𝔹;
                // ^ the returned function is not classical
}

In the following, we summarize some useful properties of classical types:

  • We can ignore duplicate classical annotations: !!τ ≡ !τ
  • Classical commutes with tuples: !(τ × τ) ≡ !τ × !τ (analogously for n-tuples with n>2). As a consequence, we also have !(τ × τ) ≡ !(τ × !τ) ≡ !(!τ × τ) ≡ !(!τ × !τ)
  • Classical commutes with arrays: !τ[] ≡ (!τ)[] ≡ !(τ[])
  • Classical commutes with fixed-length arrays: !τ^n ≡ (!τ)^n ≡ !(τ^n)
  • Classical values can be re-interpreted as quantum values: !τ <: τ

qfree

We use the annotation qfree to indicate that evaluating functions or expressions neither introduces nor destroys superpositions. Annotation qfree (i) ensures that evaluating qfree functions on classical arguments yields classical results and (ii) enables automatic uncomputation.

Example 1 (not qfree): H is not qfree as it introduces superpositions: It maps $\ket{0}$ to $\facs \Big(\ket{0}+\ket{1}\Big)$.

Example 2: X is qfreeas it neither introduces nor destroys superpositions: It maps $\sum_{b=0}^1 \gamma_b \ket{b}$ to $\sum_{b=0}^1 \gamma_b \ket{1-b}$.

Example 3: Logical disjunction (as in x||y) is of type const 𝔹×const 𝔹→qfree 𝔹, since ORing two values neither introduces nor destroys superpositions.

Example 4: Function myEval (below) takes a qfree function f and evaluates it on false. Thus, myEval itself is also qfree.

def myEval(f:𝔹→qfree 𝔹)qfree{
  return f(false); //   ^ myEval is qfree
}

mfree

Annotation mfree indicates that a function can be evaluated without applying any measurements.

Example: Function myEval (below) takes a mfree function as argument and evaluates it on false. Thus, evaluate itself is also mfree.

def myEval(f:𝔹→mfree 𝔹)mfree{
  return f(false); //   ^ myEval is mfree
}

const

Annotation const indicates that a variable will not be changed in the given context. Concretely, each parameter of a function and each variable in the context may be annotated as const. We can use constant parameters and variables more liberally, since they are guaranteed to persist in the given context.

Example: Function myEval (below) takes a constant x and a function f that leaves its first argument const:

def myEval(const x:𝔹,f:const 𝔹!→𝔹){
  return f(x);
}

lifted

Annotation lifted is a shorthand to indicate qfree functions with only constant arguments (classical arguments are implicitly treated as constants).

Example: Function MyOr is lifted:

def MyOr(x:𝔹, y:!𝔹)lifted{ // x and y are implicitly const
  return x||y;  //  ^ MyOr is lifted 
}

Types

Silq supports the following types. In this list, n stands for an arbitrary expression of type !ℕ.

  • 𝟙 (or 1): The singleton type that only contains element ()
  • 𝔹 (or B): Booleans
  • ℕ (or N): Natural numbers 0, 1, … (must be classical)
  • ℤ (or Z): Integers …, -1, 0, 1, … (must be classical)
  • ℚ (or Q): Rational numbers (must be classical)
  • ℝ (or R): Reals (must be classical). Simulation semantics are implementation-defined (typically floating-point)
  • int[n]: n-bit integers
  • uint[n]: n-bit unsigned integers encoded in two’s complement
  • τ×...×τ (or τ x ... x τ): tuples of types, e.g., 𝔹×int[n]
  • τ[]: dynamic-length arrays
  • τ^n: vectors of length n
  • !τ: type τ, but restricted to classical values
  • [const] τ×...× [const] τ → [mfree|qfree] τ: functions, optionally annotated as mfree or qfree, whose input types are optionally annotated as const

Type Conversion

Silq allows converting types by type annotation or type conversion.

Type Annotation

Type annotations allow re-interpreting the type of an expression if no runtime conversion is needed.

Examples: Function zeroes (below) creates representations of 0 of different types:

def zeroes(){
  a:=0:!𝔹; // classical bit in zero state
  b:=a:𝔹; // quantum bit in zero state
  c:=0:uint[3]; // quantum 3-bit unsigned integer
  d:=vector(4,false):𝔹[]; // quantum 4-bit vector
  return (a,b,c,d);
}

Example: By default, constant values (e.g., 0, true, …) are considered classical. To create a quantum constant, Silq requires an explicit type annotation:

def plusState():𝔹{
  x := false:𝔹;
  x := H(x);
  return x;
}

Writing x := false instead of x := false:𝔹 in plusState results in x being classical, meaning that it is not consumed by H(x). This results in the following error:

def plusStateInvalid():𝔹{
  x := false;
  x := H(x);
  return x;
} // error: redefinition of "x"

Safe Type Conversion

Safe type conversions (as) allow changing the type of an expression by converting runtime values from one type to another. They are only allowed if the conversion is safe, i.e., cannot result in a runtime exception.

Examples: Function casts shows examples of safe type conversions.

def safe_conversions(){
  // !int[32] to !ℤ
  a:=0:!int[32];
  b:=a as !ℤ;

  // !ℤ to !int[32] (wraparound in case of overflow)
  c:=0:!ℤ;
  d:=c as !int[32];

  // 𝔹^10 to int[10]
  e:=vector(10,0:𝔹);
  f:=e as int[10];

  // int[10] to 𝔹^10
  g:=0:int[10];
  h:=g as 𝔹^10;

  // convert element-wise
  i:=(0,1,2):!ℕ^3;
  j:=i as !ℕ×!ℤ×!int[3];
}

Unsafe Type Coercion

Type coercion is the unsafe alternative to type casts, which is needed whenever the type transformation may throw a runtime exception.

Examples: Function coerces shows to applications of coerce.

def unsafe_conversions(){
	// coerce array to vector
	a:=array(4,true):𝔹[];
	b:=a coerce 𝔹^4;
}

Statements and Expressions

In the following, we discuss statements and expressions in Silq.

Control Flow

  • Syntax: if e {...} else {...}

Silq supports both classical and quantum control flow. Classical control flow poses no restrictions on the two branches:

def measureInBasis(b:!𝔹,x:𝔹):!𝔹{
  // measure in |±>-basis (if b=1) or in computational basis (if b=0)
  if b{
    x := H(x);
    return measure(x);
  }else{
    return measure(x);
  }
}

Silq also supports quantum control flow. For example, the procedure cnot (below) modifies y conditioned on x:

def cnot(const x:𝔹,y:𝔹):𝔹{
  if x{
    y := X(y);
  }
  return y;
}

For quantum control flow, Silq enforces some restrictions. For example, it would disallow conditionalMeasure (below). This procedure attempts to measure x in a quantum conditional. Because this is not physically realizable, Silq rejects conditionalMeasure.

def conditionalMeasure[n:!ℕ](const b:𝔹, x:uint[n]):𝟙{
  if b{
    x := measure(x);
  }
} // error: cannot call function 'measure[uint[n]]' in 'mfree' context

Overall, Silq enforces the following properties for quantum control flow:

  • Both branches are mfree.
  • The condition can be implicitly uncomputed at the end of the two branches: the condition is lifted and all variables occurring in it are left const by both branches.
  • Both branches cannot (i) write to variables of classical type, or (ii) create arrays or (iii) create functions. The reason for this restriction is that allowing these writes would induce unexpected superpositions of (i) classical values, (ii) arrays of different lengths, or (iii) functions.

Loops

  • while e {...}: While loops; e must be classical.
  • for i in [e1..e2) {...}: For-loop from e1 (inclusive) to e2 (exclusive). Both e1 and e2 must be classical.
  • for i in [e1..e2] {...}: For-loop from e1 (inclusive) to e2 (inclusive). Both e1 and e2 must be classical.

For example, geometric samples from the geometric(0.5) distribution by counting the number of trials until measuring H(false) returns 0:

def geometric():!ℕ{
    count := 0;
    ok := true;
    while ok{
        count += 1;
        ok = measure(H(false));
    }
    return count;
}

As an example of an invalid program, the procedure quantumWhile (below) attempts to control a while-loop by a quantum condition. Silq disallows this, since the number of loop iterations is unbounded, meaning we cannot build a quantum gate that implements this loop.

def quantumWhile(const x:𝔹)mfree:𝟙{
  while x==0{
    // do work
  }
} // error: type of condition should be !𝔹, not 𝔹

Assignments

For assignments, Silq also supports modifying individual vector/array elements, as in the following code snippet:

def uniformSuperposition[n:!ℕ]():𝔹^n{
  vec := vector(n,0:𝔹); // vector of length n filled with zeros
  for i in [0..n){
    vec[i] := H(vec[i]);
  }
  return vec;
}

In general, vector/array elements can be modified according to this pattern:

Inplace modification of vector/array

Of course, Silq prevents implicitly overwriting vector entries:

def overwrite[n:!ℕ]():𝔹^n{
  vec := uniformSuperposition[n]();
  vec[0] := H(vec[1]);
  return vec;
} // error: indices for component replacement must be identical

Expressions

  • Constants: π, -10, 0, 10, 10.5, …
  • Lambda abstraction (Option 1): λ([const] x1:τ1,...,[const] xn:τn). {...}
  • Lambda abstraction (Option 2): lambda([const] x1:τ1,...,[const] xn:τn). {...}

Indexing

Indexing arrays works as usual:

def main(){
  x := [0,1,2,3];
  return x[3]; // returns 3
}

Analogously, Silq also supports indexing into the bit representation of (unsigned) integers.

def main(){
  x := 5: uint[4];
  return (x[3], x[2], x[1], x[0]); // returns the bit representation of 5: 0101
}

Silq also supports quantum indexing e1[e2] for non-classical e2, if e1 does not contain any classical components (i.e., no classical types, function types, or array types).

Functions

In the following, we discuss functions in Silq.

Lifted Operations

Silq supports various standard operations lifted to the quantum setting, including:

  • +, -, *, /
  • xorb or ⊕ (bitwise-xor)
  • div (integer division, rounded down)
  • ^ (exponentiation)
  • sin, asin (arcsin), cos, acos (arccos), tan, atan (arctan)
  • ceil (round up), floor (round down), round (round to closest)
  • comparators: <, <= or ≤, != or ≠, == or =, >, >= or ≥
  • Boolean operators: &&, ||
  • sqrt, exp, log (for $\log_b(x)$, write log(x)/log(b))
  • abs
  • min, max

Reverse

The primitive reverse allows to reverse a procedure, assuming this procedure is mfree. For example, the following line is a crucial ingredient to quantum phase estimation. It reverses QFT (the Quantum Fourier transform with the specified precision) and applies the resulting procedure to ancilla.

ancilla := reverse(QFT[precision])(ancilla);

Other Functions

The following table lists other functions supported by Silq.

Function: Type Explanation  
measure: τ→!τ measure(e) returns measured e  
H:𝔹→mfree 𝔹 H(x) returns Hadamard transformed x  
phase:!ℝ→mfree 𝟙 phase(r) multiplies the phase of the current state by $e^{i r}=\cos(r)+i\sin(r)$. phase only has an observable effect if it is executed in a quantum conditional.  
rotX:!ℝ×𝔹→mfree 𝔹 rotX(r,b) returns b:𝔹 rotated around X-axis by r:!ℝ: $\ket{r}\ket{b} \mapsto \cos\frac{r}{2}\ket{b}-i \sin \frac{r}{2} \ket{1-b}$  
rotY:!ℝ×𝔹→mfree 𝔹 rotY(r,b) returns b:𝔹 rotated around Y-axis by r:!ℝ: $\ket{r}\ket{b} \mapsto \cos\frac{r}{2}\ket{b}+ \sin \frac{r}{2} (-1)^b \ket{1-b}$  
rotZ:!ℝ×𝔹→mfree 𝔹 rotZ(r,b) returns b:𝔹 rotated around Z-axis by r:!ℝ: $\ket{r}\ket{b} \mapsto \cos\frac{r}{2}\ket{b}-i \sin \frac{r}{2} (-1)^b \ket{b}$  
X:𝔹→qfree 𝔹 X(b) returns bit-flipped b : $\ket{b} \mapsto \ket{1-b}$  
Y:𝔹→mfree 𝔹 Y(b) returns b after applying Y-gate: $\ket{b} \mapsto i (-1)^b \ket{1-b}$  
Z:𝔹→mfree 𝔹 Z(b) returns b after applying Z-gate: $\ket{b} \mapsto (-1)^b \ket{b}$  
dup:const τ→qfree τ dup(v) returns a duplicate of v: $\ket{v} \mapsto \ket{v}\ket{v}$. Note that dup does not violate the no cloning theorem.  
array:!ℕ×const τ×→qfree τ[] array(v,m) returns an array filled with m duplicates of v (analogous to dup)  
vector:!ℕ×const τ×→qfree τ^n vector(v,m) returns a vector filled with m duplicates of v (analogous to dup)  
forget(⋅=⋅):τ×const τ !qfree forget(x,y) forgets x if it equals y (and is undefined otherwise). This allows for (unsafe) uncomputation according to a specific function.  
⋅[⋅]:const τ×!uint !→qfree τ e1[e2] returns the e2-th element of e1  

Debugging

The following functions are useful for debugging:

  • dump(); dumps the current program state when running the program
  • exit(); aborts the program with an error, most useful directly after dump
  • __show(__query("dep", var)); prints the dependencies for variable var (these dependencies are used for uncomputation)
  • print(e) prints the value of the (classical) expression e

Further, in the vscode plugin, pressing F6 prints statements as they are executed as well as intermediate program states between consecutive statements.

Entry Point

The entry point for running programs is function main.

Unicode Input

Silq code often contains unicode symbols like → or 𝔹. In the following, we explain how to handle such unicode symbols.

Typing Unicode Symbols

For typing unicode input in vscode, we recommend (enter this command after hitting CTRL+P):

ext install freebroccolo.input-assist

Then in settings (CTRL+, and search for input-assist.languages) add:

"input-assist.languages": ["plaintext", "silq"]

Common Unicode Symbols

In the following, we provide a short list of commonly used unicode symbols, how the can be typed, and how to type them using ASCII symbols instead (if desired).

Symbol Shortcut ASCII alternative
→ \to ->
ℕ \bn N
ℝ \br R
π \pi pi
𝔹 \bb B
⋅ \cdot *
θ \theta (any other letter)
ψ \psi (any other letter)
λ \lambda lambda
¬ \neg !
× \times x
± \pm (none)
𝟙 \b1 1