The QCurry type class is similar to the Curry type class, except that the result type is guarded by the Circ monad. It provides a family of type isomorphisms

fun  ≅  args -> Circ res,

where

fun = a1 -> a2 -> ... -> an -> Circ res,
args = (a1, (a2, (..., (an, ())))).

The benefit of having Circ in the result type is that it ensures that the result type is not itself a function type, and therefore fun has a unique arity n. Then args and res are uniquely determined by fun, which can be used to write higher-order operators that consume fun of any arity and "do the right thing".

Often a low-level function, such as qcdata_zip or qcdata_promote, throws an error because of a failure of some low-level condition, such as "list too short". To produce error messages that are meaningful to user-level code, these functions do not have a hard-coded error message. Instead, they input a stub error message.

A meaningful error message typically consists of at least three parts:

• the name of the user-level function where the error occurred, for example: "reverse_generic";
• what the function was doing when the error occurred, for example: "operation not permitted in reversible circuit";
• a specific low-level reason for the error, for example: "dynamic lifting".

Thus, a meaningful error message may be: "reverse_generic: operation not permitted in reversible circuit: dynamic lifting".

The problem is that the three pieces of information are not usually present in the same place. The user-level function is often a wrapper function that performs several different mid-level operations (e.g., transforming, reversing). The mid-level function knows what operation was being performed when the error occurred, but often calls a lower-level function to do the actual work (e.g., encapsulating).

Therefore, a stub error message is a function that inputs some lower-level reason for a failure (example: "list too short") and translates this into a higher-level error message (example: "qterm: shape of parameter does not data: list too short").

Sometimes, the stub error message may also ignore the low-level message and completely replace it by a higher-level one. For example, a function that implements integers as bit lists may wish to report a problem with integers, rather than a problem with the underlying lists.

Labelable a s means that a is a data structure that can be labelled with the format s. A "format" is a string, or a data structure with strings at the leaves.

Run a subcomputation with a subscript index appended to the current index list. Sample usage:

with_index "0" $ do
  <<<labelings>>>

Run a subcomputation with a dotted index appended to the current index list. Sample usage:

with_dotted_index "left" $ do
  <<<labelings>>>

Like with_index, except the order of the arguments is reversed. This is intended to be used as an infix operator:

<<<labeling>>> `indexed` "0"

Like with_dotted_index, except the order of the arguments is reversed. This is intended to be used as an infix operator:

<<<labeling>>> `dotted_indexed` "left"

Take two IntMaps with the same domain, and form a new IntMap whose values are pairs. It is an error if the two inputs don't have identical domains.

Like intmap_zip, but also takes an error message to use in case of domain mismatch.

Map a function over all values in an IntMap.

Monadic version of intmap_map. Map a function over all values in an IntMap.

The type Identity a b witnesses the fact that a and b are the same type. In other words, this type is non-empty if and only if a = b. This property is not guaranteed by the type system, but by the API, via the fact that the operators reflexivity, symmetry, and transitivity are the only exposed constructors for this type. The implementation of this type is deliberately hidden, as this is the only way to guarantee its defining property.

Identity types are useful in certain situations. For example, they can be used to define a data type which is polymorphic in some type variable x, and which has certain constructors that are only available when x is a particular type. For example, in the declaration

data ExampleType x = Constructor1 x | Constructor2 x (Identity x Bool),

Constructor1 is available for all x, but Constructor2 is only available when x = Bool.

Witness the fact that a=a.

Witness the fact that a=b implies b=a.

Witness the fact that a=b and b=c implies a=c.

The identity function id : a → b, provided that a and b are the same type.