Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Compositional theories for embedded
programming (I)Margherita Zorzi, Ph.D
A joint work with Davide Trotta, Ph.D
Department of Computer Science, University of Verona

IWC 2020 Paris Nord Summer of LoVe 2020

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

A minimalist incipit←−H −→ C

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

The programming perspective

Embedded programming style allows to split the syntax in two parts,representing a host language H and a core language C embedded in
H respectively. This formally models several situations in which auser writes a code in a main language and delegates some tasks toanother ad hoc (sometimes domain specific) language.
The interaction between H and C is controlled by “mixed” typing
rules that specify how to “promote” well-formed terms from thecore to the host and (possibly) viceversa.
Question: how to give a theoretical foundation of host-coreprogramming style?

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Back to the theory ( or Back to the Garden, “Woodstock”, 1969)
A theoretical foundation of a crucial particular case of embedded
languages is rooted in the Linear/Non Linear (L/NL) system
introduced by Benton (here we mainly follow “Relating Categorical
Semantics for Intuitionistic Linear Logic” by Maietti et al.).
The dichotomy L/NL is interesting but it can not represent “as itis” the basis for a theory for embedded programming.
One need to define a more flexible system, in which the embeddingof an arbitrary (possibly non linear) core into an arbitrary hostlanguage is allowed, and where L/NL follows as a particular case.
Goals: the definition of a systematised type theory able to captureand standardize common properties of embedded languages; tostudy the relationship between embedded languages and theirmodels.
Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

OutlineHC0 : syntax
HC0 : semantics
Relating syntax and semantics
On the compositionality of HC0
WIP: the insight into the PL perspective

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

HC0 : main ideas
We start from a simply typed H and a linear C to define a “kernel”
type theory, that can be easily extended both in the host and in thecore parts.
We intentionally start from a linear core, since, as we will show, wecan easily obtain a non linear core as a particular case.
HC0 is a minimal language able to capture the good properties
common to an ideal class of embedded languages {HCi }i , built out
from HC0 , in order to derive any more expressive type theory as anextension of the kernel rules, both for the core C and the host H.
The design of the HC0 type system “privileges” the host language Hi.e., mirroring concrete programming, we establish an hierarchicaldependency of the core part on the control part: the embedded
language C is fully described in the host H.
Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Judgements and Type constructors`H X : type

`H X = Y : type

Γ `H t : XΓ `H t = s : X .

`C A : type

`C A = B : type

Γ | Ω `C f : A

Γ | Ω `C f = h : A`C A : type

(t0c)
(t1c)
(t2c)

`C A : type
`C B : type
`C A ⊗ B : type
`C A : type
`C B : type
`H Proof(A, B) : type
`H X : type(t0v )(t2c)(t2v )`H X : type
`H Y : type
`H X × Y : type
`H X : type
`H Y : type
`H X → Y : type

Table: Types constructors

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Well-typing rules (fragment)Γ 1 , x : X , Γ 2 `H x : X(av)(π1v )

Γ `H s : XΓ `H s : XΓ `H t : YΓ `H hs, ti : X × Y(π2v )Γ `H inl(v ) : X(aiv)Γ `H t(s) : YΓ `H v : X × YΓ `H inr(v ) : Y
Γ, x : X `H t : YΓ `H λx : X .t : X → Y

Γ | a : A `C a : A(ac)(tc)Γ `H v : X × YΓ `H t : X → Y(aev)(pv)

Γ | Ω1 `C f : A(let1c)(prom)Γ | Ω2 `C g : B

Γ | Ω1 , Ω2 `C f ⊗ g : A ⊗ B
Γ | Ω1 `C f : A ⊗ BΓ | Ω2 , a : A, b : B `C h : C

Γ | Ω1 , Ω2 `C let f be a ⊗ b in h : C
Γ | Ω `C f : AΓ `H promote(f ) : Proof(×Ω , A)
Margherita Zorzi, Ph.DΓ `H f : Proof(A, B)(der)| a :embedded
A `C derelict(f) : B (I)
Compositional theoriesΓ forprogramming

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Evaluations

The β and η rules for the H-terms are those of simply typed lambda
calculus;
The β rules for the C-terms are those of the modality-free fragmentof linear logic (without exponents).

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

The category Th(HC0 ): objects and morphisms

Definition (HC0 -theory)
A typed system T is a HC0 -theory if it is an extension of HC0 withproper-T-axioms, namely with new ground type symbols, new typeequality judgments, new terms symbols and new equality judgments ofterms.
Definition (HC0 -translation )Given two HC0 -theory T1 and T2 , an HC0 -translation L is a function
from types and terms of T1 to types and terms of T2 preserving types
and terms judgments

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Breaking the dichotomy Linear-Non Linear, Part I

If we want to extend the language C to a non-linear core, we haveto force the tensor product to be a cartesian product. This can doneby adding to the core type system the rules for product plus
projections (with mixed contexts). Notice that old rules for tensor
are easily derivable from the new ones.

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Categorical semantics

We state a correspondence between the typed calculus HC0 and its
categorical model via the notion of internal language.
HC0 provides an internal language of the category Model(HC0 ) of its
models if Model(HC0 ) ≡ Th(HC0 ).
Intermediate goal: to define a category of models Model(HC0 )such that HC0 provides an internal language for these models.
Objects of Model(HC0 ): models of HC0
Morphisms: interesting part of the construction.

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Models of HC0

We define a model for HC0 in terms of an instance of an enrichedcategory, by interpreting the host part into a category V and the core
part into a suitable category C enriched in V.
Definition (Models of HC0 )A model of HC0 is a pair (V, C) where V is a cartesian closed category
and C is a V-monoidal symmetric category.

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Defining the category Model(HC0 )Structures and interpretation are defined in the usual way, some cases:[|Proof(A, B)|] = C([|A|], [|B|])[|Γ `H promote(f ) : Proof(×Ω , A)|] := [|Γ | Ω `C f : A|][|Γ | a : A `C derelict(g ) : B|] = [|Γ `H g : Proof(A, B)|].
Theorem (Soundess and Completeness)
Symmetric, monoidal categories enriched on cartesian closed categories
are sound and complete with respect to the calculus HC0 .

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Defining the category Model(HC0 )A key notion:
Definition (Change of base)/ V2 , the induced functor
Given a cartesian closed functor F : V1
/ V2 - Cat is called change of base.
F∗ : V1 - Cat
TT-programming “reading key”: if we have a translation between
two host language H1 and H2 and C is an embedded language in
H1 , then we can use the translation to change the host language forC, obtaining an embedding in H2 .

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

The category Model(HC0 )Definition (Category of HC0 models)
Objects of Model(HC0 ): models (V, C);
An arrow in Model(HC0 ) between two models (V1 , C1 ) and (V2 , C2 ) is given by a/ V2 if a strict cartesian closed functor, andpair (F , f ) where F : V1f : F∗ (C1 )/ C2 is a V2 -functor, preserving strictly all the structures.

Given two arrows (F , f ) : (V1 , C1 )(G , g ) : (V2 , C2 )/ (V2 , C2 ) and/ (V3 , C3 ) the composition of these is given by the pair

(G , g )(F , f ) := (GF , gf ) wheregf := gG∗ (f ).

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.DIntroduction
The “kernel” embedded calculus HC0Categorical semantics
Discussions

Th(HC0 ) ≡ Model(HC0 )Theorem
The typed calculus HC0 provides an internal language for Model(HC0 ),i.e. Th(HC0 ) is equivalent to Model(HC0 ).
Proof (sketch)/ Model(HC0 ) by mapping a HC0 -theory to its syntactic
C : Th(HC0 )category defined as in Theorem Soundness and Completeness.
/ Th(HC0 ) is defined by mapping an object (V, C) ofL : Model(HC0 )Model(HC0 ) to the HC0 -theory obtained by extending HC0 . For example:- we add new C-types A with the corresponding axiom `C A : type for eachelement of ob(C) (we are naming the objects of C in the calculus and we extend
the interpretation of the C-types of HC0 by interpreting the new names with thecorresponding objects);- we add new C-terms f and Γ | ×Ω `C f : A for each morphism/ Proof(×Ω , A) of V having the interpretation of Γ as domain andf:Γ
of Proof(×Ω , A) has codomain.
Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
DiscussionsBreaking the linearity of the core, Part II- Semantics

If we want to extend C to a non-linear core, we have to force thetensor product of the enriched category C to be a V-cartesian
product. Notice that the new product is a particular case of theV-tensor product.

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

On the compositionality of HC0 -I

The kernel calculus HC0 has been designed to be “compositional”(both from the syntactical and the semantics viewpoints).
In our host-core type theory we establish a hierarchical dependencyof the core on the host. Notwithstanding, H and C are independentcalculi, with their own syntax and denotation. They both can work
as standalone languages, with independent operational semantics
and categorical interpretation. In the moment one decide to embed
C in H, the promotion mechanism allows to import syntax from C
into H (to have a“mixed” syntax is mandatory).
Both H and C can be extended to include more complex features
easily mirroring the extension at the semantical level.

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

On the compositionality of HC0 - II:“tuning” the computational paradigm

The core C can be “specialized” to a computational paradigm.
As a particular case, we can set the C to a circuit description
languages and we can “tune” it to quantum, probabilistic orreversible computation.
Relation with Staton’s EWire and the embedded language QWire(Zdancewic et al.).

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

In progress: the PL perspective, informally...

We are now able to provide a formal definition of host-core languages: Given L1and L2 standalone languages with their respective syntactic denotations D1 andD2 , we say that L2 is embedded in L1 if the pair (D1 , D2 ) belongs toModel(HC0 ). This means that there exists an host-core language L3 such thatL1 hosts L2 .
From the constructive proof of the correspondence between syntax andsemantics we extract an algorithm that, given two models D1 and D2 builds a“candidate” type theory L3 .
Working on concrete instances of the family HCi and specializations to nonclassical computational paradigm: we are studying instances of (versions of) HC0
as higher-order quantum/reversible/probabilistic circuit description languages.

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussions

Mini Biblio
D. Trotta, M. Zorzi. Compositional theories for embedded languages, journal
paper, submitted, 2020. https://arxiv.org/abs/2006.10604
P. N. Benton. 1995. A mixed linear and non-linear logic: Proofs, terms andmodels. In Computer Science Logic, Leszek Pacholski and Jerzy Tiuryn (Eds.).
Springer Berlin Heidelberg, Berlin, Heidelberg, 121-135
M. E. Maietti, P. Maneggia, V. de Paiva, and E. Ritter. 2005. Relating
Categorical Semantics for Intuitionistic Linear Logic. Appl. Categ. Structures
13, 1 (2005), 1-36.
Mathys Rennela and Sam Staton. 2018. Classical Control and Quantum
Circuits in Enriched Category Theory. Electronic Notes in Theoretical Computer
Science 336 (2018), 257-279. https://doi.org/10.1016/j.entcs.2018.03.027.
MFPS XXXIII.
Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: A Core
Language for Quantum Circuits. In Proceedings of the 44th ACM SIGPLAN
Symposium on Principles of Programming Languages (Paris, France) (POPL2017). ACM, New York, NY, USA, 846-858.
https://doi.org/10.1145/3009837.3009894
Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D

Introduction
The “kernel” embedded calculus HC0
Categorical semantics
Discussionsthanks, merci, gracias, grazie, vic-tour e smursma, peace&love

Compositional theories for embedded programming (I)Margherita Zorzi, Ph.D