In many situations, programming languages with varying levels of expressiveness need to interact to achieve a final result. This paper is about HC, a framework derived from a categorical model that formalizes how two typed paradigmatic programming languages H and C can interact in a hierarchical manner: the host language H can operate on the core terms of C, but not the other way around. We recall the essential structure of the categorical model, and present a specific example of HCwhere H is capable of composing circuits that can be modeled using C. Finally, we discuss potential straightforward and natural generalizations of this instance of HC.
are endowed with suitable simulation tools (e.g. Vilinx Vivado and Quartus Prime) for the
development of digital circuits. Often, HDLs programs are interfaced with software written
in C/C++. Reversible circuits are a special class of digital circuits where every operation is
physically reversible, so that the energy dissipation can be tamed in a precise way. Specialized
languages and extensions of existing HDLs to describe reversible circuits are considered in
RevKit and, sometimes, interoperates with quantum programming. The quantum programming
is essentially done in terms of quantum circuits (see Quantum Azure, IBM Quantum Platform,
...) in a context controlled by a high-level language (typically Python) which sets up the desired
orchestration of quantum operations. Last, a situation not dissimilar to the digital case occurs
in the case of analog circuits, which typically must be interfaced with digital systems by using
Verilog-AMS and VHDL-AMS (extensions of Verilog and VHDL for analog/mixed signal).
Languages distinctive traits. This paper aims to model the interaction between two
languages: a core one, describing circuits and a host language that manipulates them. This
interoperation is typical of any quantum development kit (e.g., see QiSKIT and QDK) that
grasps an usual facet of quantum programming languages (see, for instance, [
We notice that this work is meant to be explorative, so we will keep it as simple and intuitive as possible. We begin by identifying the distinguishing features that characterize the host-core scenario that we want to explore.
• The language for circuits we will formalize is iteration-free. It provides primitives to
compose sub-circuits. The host language will allow us to manipulate sub-circuits, for
example replicating them as required, possibly depending on some parameter. For example,
an adder could be parameterized on the number of its input/output bits.
• The host language operating on the terms of a core language fits in the area of
metaprogramming, where programs manipulate other programs. We address to [
Metodology. Our starting point is a categorical analysis as proposed in [
On the categorical ground we define a typed calculus HC embodying two communicating languages H (host) and C (core), our calculus being the sound and complete internal language of the mentioned interacting categories. The language C is a linearly typed calculus suficient to model the composition of circuits. The language H is essentially a simply typed lambda calculus characterized by the type Proof(, ), where and are types for the terms in C. The presence of types with form Proof(, ) in H place H in a higher position than that of C in a straightforward hierarchy which establishes which language manipulates the terms of the other language. Specifically, host terms in H can manipulate core terms in C, namely circuits, but not vice versa.
It is worth noting that HC has some significant limitations. Firstly, for example, C will not
include the fan-out wiring (see [
We here do not see the mentioned limitations as an obstacle to start the investigation that we summarize in this work. We will briefly discuss how to overcome limitations in a simple way in the conclusions.
In this section we present the typed calculus HC. It builds upon the two components host language H, designed as a simply typed lambda calculus, and embedded core language C which we assume can be typed by a linear type discipline. By design, the host language is privileged, as compared to the core. Seen in the other way round, we do not allow that every of the terms we can build as part of the host language can be seen as terms at the core level. Roughly, the core language is hierarchically dependent on the host language.
HC difers from the language that Benton introduces in [
• Regarding the host language H, H-types are ranged over , , . . . , H-type contexts by Γ, Γ′, H-variables by , , . . . , and H-terms by , , . . . . • Regarding the core language C, C-types are ranged over by , , . . . , C-type contexts by Ω, Ω′, C-variables by , , . . . , and C-terms by ℎ, , . . . .
We write Γ | Ω to identify a mixed context that includes both host (in Γ) and core (in Ω) type information. For every host context Γ, we denote the product of its elements by × Γ. Same for every core context Ω. We consider two fixed sets of base types: a set ΣC of base C-types, ranged over by (possibly indexed) and a set ΣH of base H-types, ranged over by (possibly indexed).
The language T of types for the core language is generated by the grammar: , , ::= | , 0, 1, . . . | ⊗ (1) with the unit type, and , 0, 1, . . . elements of ΣC, set of base types for C. An example of an element in ΣC is Bit (see Section 3 ). The type is the unit for the tensor ⊗ , meaning that we can always think of 1 ⊗ . . . ⊗ and ⊗ 1 ⊗ . . . ⊗ as simply whenever = 0.
The language T of types for the host language is generated by the grammar: , , ::= 1 | , 0, 1, . . . | × | → | Proof(, ) (2) with 1 the unit type, , 0, 1, . . . elements of ΣH, set of base types for H, and both , being C-types. Examples of elements in ΣH are {Nat, Bool}.
Similarly to [
The grammars that generate the core language C and the host language H have the following mutually recursive definitions: , ::= ∙ | | ⊗ | let be ⊗ in ℎ | let be ∙ in ℎ | derelict(, ) , ::= * | | ⟨, ⟩ | 1() | 2() | : . | | promote(1, . . . , . ) (3) (4) respectively, where in (4) is a core term generated by (3), and in (3) is a host term generated by (4).
Core terms belong to a linear language1 with let constructor and unit ∙ with type . Host terms are simply-typed lambda calculus with unit term * with type 1. Finally, the functions derelict(· , · ) and promote(· .· ) model the communication between host H and core C.
The typing rules for HC are in Figure 1. The dereliction rule (der) “derelicts” a host term to
the core language by applying it to a correctly typed (linear) core term; this choice is consistent
with the standard presentation of this kind of rules (e.g., see [
The following lemma can be proved by structural induction on the derivations that we can build by means of the rules in Figure 1.
Lemma 1. [Substitution]
(sub1) If Γ ⊢H : and Γ, : | Ω ⊢C : then Γ | Ω ⊢C [/] : .
(sub2) If Γ | Ω1 ⊢C : and Γ | Ω2, : ⊢C : then Γ | Ω1, Ω2 ⊢C [/] : .
(sub3) If Γ ⊢H : and Γ, : ⊢H : then Γ ⊢H [/] : .
1We use “linearity” to identify the linear use of variables (alternative linearity notions are discussed in [
Γ1, : , Γ2 ⊢H : (pv) Γ ⊢H : Γ ⊢H :
Γ ⊢H ⟨, ⟩ : × ( 2) Γ ⊢H : ×
Γ ⊢H 2() : (aev) Γ ⊢H : → Γ ⊢H :
Γ ⊢H () : (ac) Notice that (sub1) allows us to substitute a host term for a variable in a core term. In designing (sub2), we follow the line adopted in languages like QWire and EWire, which have some primitive notions of substitution for composing functions of Proof(· , · ) type. Finally, (sub3) models the replacement of a term for a variable in the host language as well as in simply typed lambda calculus. These substitution lemmas are quite similar to that presented in the enriched efect calculus EEC, see [15, Prop. 2.3]
The equational theory among the terms in H is the standard one induced by / -rules which equates simply typed lambda terms. Figure 2 introduces the equational theory of HC.
The equations in the rules of Figure 3 model how promotion and dereliction are each other dual, where in (der-prom) we use Ω to denote [1 : 1, . . . , : ].
(el1) Γ | Ω1, : , : ⊢C : Γ | Ω2 ⊢C : Γ | Ω3 ⊢C ℎ :
Γ | Ω1, Ω2, Ω3 ⊢C let ⊗ ℎ be ⊗ in = [/, ℎ/] : (el2)
Γ | Ω1, : ⊗ ⊢C : Γ | Ω2 ⊢C : ⊗ Γ | Ω1, Ω2 ⊢C let be ⊗ in [ ⊗ /] = [/] : (el3)
Γ | Ω ⊢C : Γ | Ω ⊢C let ∙ be ∙ in = : (el4) identify terms that we can interpret as purely linear structures that we can build by means of tensor products.
Remark. As compared to Benton LNL system, here we add the rules to the calculus following
the presentation of [
Specifically, the crucial diference between LNL original presentation and HC is that the interaction between H and C is not symmetric. Since we are programmatically defining HC as a minimal system, having a linear core is a natural starting choice. This could appear very limiting and dificult to overcome when writing a program. However, it is not the case.
On a first hand, to extend C with non-linear behavior, it would be enough to endow the rules
for the tensor product with additive contexts and transform it into a Cartesian product. This
can be easily reflected at the semantic level, restoring all the results about the correspondence
between syntax and semantics [
On the other hand, the design of the system HC is motivated by the need to incorporate linearity into languages for quantum computing and multi-language frameworks, the goal being to demonstrate how a minimal linear system like HC can be efectively integrated into a host language and extended for future applications. □ Example 1. [Composition in H of C terms] Let the following judgments: Γ ⊢H : Proof(, ) Γ ⊢H : Proof(, ) be given. We can construct the term: Γ ⊢H promote(.derelict(, derelict(, ))) : Proof(, ) (6) in H, denoted as comp(., ), which becomes the associative composition in H of terms in C which we can think of as functions from to , and to . □
We here introduce examples to show how we concretely think of using a formal framework like HC. The examples assume to equip HC with constants and functions to support basic circuit definition and manipulation, specializing HC to a system hosting a (toy) hardware definition language.
Since languages for circuit manipulation are particularly relevant for classical,
probabilistic[
The extensions of C and H with new terms and the specification of their operational semantics are kept at an intuitive level, in an illustrative perspective. This work is meant to show that modelling the interaction between two languages as we do is viable, leaving a full technical development to future work.
Example 2. [Reversible Boolean Circuits at the core level] We recall that any boolean reversible gate with arity is interpreted as a self-dual boolean injective function with input and output.
We start by extending C to C* to include boolean reversible gates. We need to fix a new type Bit and its two inhabitants 0, 1 such that: Γ | − ⊢ C 0 : Bit Γ | − ⊢ C 1 : Bit which we interpret obviously by the corresponding natural numbers.
The further extension of C* , as compared to C, is by the set of boolean reversible gates “Swap” sw, “Negation” not, also known as “Tofoli-one ”, “Tofoli-two ” cnot, and “Tofoli-three ” ccnot whose typing rules are:
Γ | Ω ⊢C : Bit Γ | Ω ⊢C not( ) : Bit Γ | Ω ⊢C : Bit
Γ | Ω ⊢C : Bit Γ | Ω , Ω ⊢C sw(, ) : Bit ⊗ Bit Γ | Ω ⊢C : Bit
Γ | Ω ⊢C : Bit Γ | Ω , Ω ⊢C cnot(, ) : Bit ⊗ Bit Γ | Ω ⊢C : Bit
Γ | Ω ⊢C : Bit Γ | Ωℎ ⊢C ℎ : Bit .
Γ | Ω , Ω, Ωℎ ⊢C ccnot(, , ℎ) : Bit ⊗ Bit ⊗ Bit The reversible gates can be interpreted as boolean functions with inpu/output values in {0, 1}: sw(, ) ::= ⊗ cnot(, ) ::= ⊕
not() ::= 1 − ccnot(, , ) ::= ⊕ , where ⊕ is the exclusive or and the multiplication between and .
For cnot, modelling it as a self-dual operator, would mean to add the axiom: let cnot(, ) be ⊗ ′ in cnot(, ′) = ⊗ to C* . The equation models that a series composition of cnot(, ), and cnot(, ′) yields the identity on the tensor product ⊗ between the two “wires” , and . Analogous axioms would be required for sw, not, and ccnot.
For example, we can derive Γ | Ω ⊢C not(not( ) : Bit by means of the substitution rule (2), as follows:
Γ | Ω ⊢C : Bit Γ | Ω ⊢C not( ) : Bit Γ | Ω ⊢C not(not( )) : Bit .
Linear constraints on Bit forbid the duplication of variables with type Bit. This aspect is crucial in contexts like reversible and quantum computing where the no-cloning property on values must hold. □ Examples 3 and 4 below suggest how to accommodate the syntax of the host language to the extension in Example 2. In particular, we focus on the circuits manipulation at host level. Example 3. [Promoting Reversible Boolean Circuits to the host level] Let our core language be C* as in Example 2. The core constants 0 and 1 can be lifted the host level, so belonging to what we can call H* , by means of ():
Γ ⊢H promote(− .0) : Proof(, Bit) Likewise, lifting exists for gates and complex circuits built on gates. For example: Γ ⊢H promote(1 . . . .not ( )) : Proof(⊗ Ω, Bit) Γ ⊢H promote(1 . . . , 1 . . . .cnot (, )) : Proof(⊗ Ω ,Ω , Bit) , where ⊗ Ω ,Ω denote 1 ⊗ . . . ⊗ ⊗ 1 ⊗ . . . ⊗ , assuming that: 1 : 1 . . . : ⊢C : Bit 1 : 1 . . . : ⊢C : Bit .
In fact, we can apply the lifting to H* to more complex circuits in C* to obtain further complex structures, like parallel composition. Let: Γ ⊢H : Proof(, ) Γ | : ⊢C : Γ ⊢H : Proof(, ) Γ | : ⊢C : be given, where, the terms , , and ℎ have already be lifted to H* from C* . The parallel composition of and , which depend on , and , respectively, is:
parallel(., .) ::= promote(, .(derelict(, ) ⊗ derelict(, ))) whose type is Proof( ⊗ , ⊗ ). Fig. 4 derives it.
: Proof(, ). : Proof(, ). parallel(., .) (7) with : and : open variables from C* , not in H* , and type
Proof(, ) → Proof(, ) → Proof( ⊗ , ⊗ ) .
A term analogous to (7), which, however, model the series composition, is:
ℎ : Proof(, ). : Proof(, ).comp(.ℎ, ) with type Proof(, ) → Proof(, ) → Proof(, ) which applies ℎ after , where comp(.ℎ, ) is defined in Example 1. □ Example 4. [A circuit core language, III: Controlling Circuits, some reflections] Let us assume to call H++ the extension of H* in Example 3 with boolean constants true, false, typed by the obvious rules, with: Γ ⊢H : bool Γ ⊢H : Γ ⊢H :
Γ ⊢H if then else : Depending on the value of , we can decide to operate either on , or which may well have been lifted from C* . So, inside H++ it is possible control how to operate on circuits that come from C* .
For example, let us assume that : , : , : Bit ⊗ Bit, and Γ be:
: bool, : Proof(Bit ⊗ Bit, Bit ⊗ Bit), : Proof(Bit ⊗ Bit, Bit ⊗ Bit) . We can start to observe that the terms: promote(− .0 ⊗ 0) promote(− .1 ⊗ 1) represent input values 0 ⊗ 0, and 1 ⊗ 1 lifted from the core level to the host one. Then, we can derive the two following judgments:
[] Γ ⊢H ⏞comp(.promo⏟te(− .0 ⊗ 0), ) : Proof(, Bit ⊗ Bit) Γ ⊢H comp(.promote(− .1 ⊗ 1), ) : Proof(, Bit ⊗ Bit) ,
⏟ [⏞] where [ ] (with free variable ) stands for the application of to the input promote(− .0⊗ 0), and [] (with free variable ) has analogous meaning, or the slightly more complex judgment: [,] Γ ⊢H ⏞comp(.promote(− .1 ⊗ 1), comp(., )) : Proof(, Bit ⊗ Bit) ⏟ in which [, ] (with free variables , ) represents tha application of the promoted to the application of the promoted to the promoted input 1 ⊗ 1.
Building on the previous terms, we can give the type: bool → Proof(Bit ⊗ Bit, Bit ⊗ Bit)
→ Proof(Bit ⊗ Bit, Bit ⊗ Bit) → Proof(, Bit ⊗ Bit) to the term: [] ...
if then ⏞comp(.promo⏟te(− .0 ⊗ 0), ) (8) else comp(.promote(− .1 ⊗ 1), comp(., ))
⏟ [⏞,] where we omit the types of lambda-abstracted variables for the sake of readability. Obviously, (8) evaluates only one of the two branches depending on the eventual value of . □
Example 4 shows a very basic form of control by the host on the core. According to further
extensions of the core C, one can define more significant control operations. For example, if we
move to a Turing complete host, or at least to a typed system as expressive as Gödel System ,
we can think of defining series or parallel compositions of circuits whose length or dimension
depends on a numeric parameter , used to drive some iteration. These would be quite handy
to define terms at the host level ready to build well-known quantum algorithms [
In this section we recall the main ideas and some results we inherit from the technical report
[
One can define a model for HC in terms of an instance of an enriched category, by interpreting the host part into a category H and the core part into a suitable category C enriched in H [20]. Definition 1. A model for HC is given by a pair (ℋ, ), where ℋ is a cartesian closed category, and is a ℋ-enriched symmetric monoidal category.
Structure and interpretation are defined in a standard way. A structure for the language
HC in (ℋ, ) is specified by giving an object [||] ∈ ob(ℋ) for every base H-type , and
an object [||] ∈ ob() for every base C-type . Given these assignments, the other types
are interpreted recursively. We address to [
Theorem 1. [Soundness and Completeness] Enriched symmetric, monoidal categories on a cartesian closed category are sound and complete with respect to the calculus HC.
In the proof of the previous theorem and in the following results, some notions play a crucial role. The first one is the category Th(HC) of HC-theories, whose objects are HC-theories, i.e., type systems that properly extend HC with new base types, term symbols, and equality rules. The morphisms are translations between theories, mapping types and terms to types and terms, preserving type and term judgments.
Notice that concrete instances of HC introduced in the previous section are examples of HC-theories.
The other key notion to achieve the Internal Language theorem is the category of models
Model(HC). This step is the more interesting and challenging part of the proof. The objects
of Model(HC) are models of HC (see Definition 1). Morphisms of Model(HC) require to
introduce the formal notion of change of base, that explains formally how by changing the host
language one can induce a change of the embedded language. Given a cartesian closed functor
: ℋ1 → ℋ2 (a morphism between two models for H1 and H2 resp.), the induced change
of base functor * : ℋ1- Cat → ℋ2- Cat sends a ℋ1-category (a category for a core C1
embedded in H1) to the ℋ2-category * () (a category for a core C2 embedded in H2). * ()
has the same objects as and for every and of , one defines * ()(, ) = ((, ));
the composition, unit, associator and unitor morphisms in * () are the images of those of
composed with the structure morphisms of the cartesian closed structure on (see [21,
Proposition 3.5.10] or [20] and [
Notice that the notion of change of basis suggests how efectively the embedding of a core in
a host works and how two obtain new embeddings: if one provides a translation between two
host languages H1 and H2 and C is a core language for H1, then one can use this translation of
host languages to change the host language for C, obtaining an embedding in H2. See [
We know from [
We state now the theorem showing the equivalence between the categories of models and that of theories for HC.
Theorem 2. [Internal Language Theorem] The typed calculus HC provides an internal language for Model(HC), i.e. Th(HC) is equivalent to Model(HC).
The proof relies on the construction of a pair of functors: the first functor
: Th(HC) → Model(HC) assigns to a theory its syntactic category, and the second
functor : Model(HC) → Th(HC) assigns to a pair (ℋ, ) (a model of HC, see Definition 1) its
internal language, as a HC-theory (see [
We conclude this work by recalling some observations we left at the end of our introduction, which are related to the expressiveness of the components H, and C of HC.
A possible way to add a fan-out to C in order to duplicate values is to adopt Tofoli’s proposal
in [
Similarly, we can enhance the expressiveness of H by incorporating constants with types that align with the categorical semantics, and which can be interpreted as recursion or while iterators. For instance, a recursion iterator could have the type Nat → (Nat → Nat) → Nat → Nat, where Nat denotes the type of natural numbers. This type can be easily interpreted in a straightforward generalization of the categorical model from the previous section, where the tensor product ⊗ can be replaced by the Cartesian product × .
According to a wider perspective, we see how HC can be extended to model the interaction
between a classical and a reversible, or quantum language. Specifically, we plan to explore how
to add the constant “projection” to HC, “projection” being present in the languages explored in
[
Press, 1986. [24] A. M. Pitts, Categorical logic, in: S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (Eds.),
Handbook of Logic in Computer Science, volume 6, Oxford Univ. Press, 1995, pp. 39–.129. [25] P. Johnstone, Sketches of an elephant: a topos theory compendium, volume 2 of Studies in
Logic and the foundations of mathematics, Oxford Univ. Press, 2002. [26] L. Paolini, M. Piccolo, L. Roversi, On a class of reversible primitive recursive functions and its turing-complete extensions, New Generation Computing 36 (2018) 233–256. doi:10. 1007/s00354-018-0039-1. [27] L. Paolini, M. Piccolo, L. Roversi, A certified study of a reversible programming language, in: T. Uustalu (Ed.), 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, volume 69 of LIPIcs, Schloss Dagstuhl - LeibnizZentrum für Informatik, 2015, pp. 7:1–7:21. doi:10.4230/LIPICS.TYPES.2015.7. [28] A. B. Matos, L. Paolini, L. Roversi, On the expressivity of total reversible programming languages, in: Reversible Computation: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings, Springer-Verlag, Berlin, Heidelberg, 2020, p. 128–143. doi:10.1007/978-3-030-52482-1_7. [29] L. Paolini, M. Piccolo, L. Roversi, A class of recursive permutations which is primitive recursive complete, Theor. Comput. Sci. 813 (2020) 218–233. doi:10.1016/j.tcs.2019. 11.029.