Multiversal Polymorphic Algebraic Theories— Syntax, Semantics, Translations, and Equational Logic —Marcelo Fiore

Makoto Hamana

Computer Laboratory, University of Cambridge

Dept. of Computer Science, Gunma University

Abstract—We formalise and study the notion of polymorphic
algebraic theory, as understood in the mathematical vernacular asa theory presented by equations between polymorphically-typed
terms with both type and term variable binding.
The prototypical example of a polymorphic algebraic theory
is System F, but our framework applies more widely. The extra
generality stems from a mathematical analysis that has led toa unified theory of polymorphic algebraic theories with thefollowing ingredients:- polymorphic signatures that specify arbitrary polymorphic
operators (e.g. as in extended λ-calculi and algebraic effects);- metavariables, both for types and terms, that enable the genericdescription of meta-theories;- multiple type universes that allow a notion of translation between theories that is parametric over different type universes;- polymorphic structures that provide a general notion of algebraic model (including the PL-category semantics of System F);- a Polymorphic Equational Logic that constitutes a sound andcomplete logical framework for equational reasoning.
Our work is semantically driven, being based on a hierarchicaltwo-levelled algebraic modelling of abstract syntax with variablebinding.
Index Terms—polymorphism, equational logic, presheaves, categorical semantics, the Grothendieck construction

I. I NTRODUCTION
The notion of polymorphism introduced by Strachey [32]is one of the most remarkable inventions in programminglanguage theory. The theory of polymorphism started withthe polymorphic λ-calculus of Girard [13] and Reynolds [29],and led to Milner’s striking application to functional programming [25]. Since then, the theory has deepened and its applicability spread broadly. Numerous systems have been extended
to support polymorphism. Nowadays, it is not only supported
in functional languages and proof assistants (e.g. ML, Haskell,
Coq, Agda), but also other systems have been extended to copewith polymorphism, such as the π-calculus [27]. It has further
been incorporated into object-oriented languages (e.g. Java,C++) where it is regarded as a key feature of generic programming. The range of applicability of polymorphism illustrates
that, despite its origins, it is not necessarily based on λ-calculi.
But, what are polymorphic calculi?
In tackling this question, the aim of the paper is to establish
an algebraic framework for analysing and reasoning about
polymorphic systems generally. Indeed, we formalise andstudy the notion of polymorphic algebraic theory, as a formal
theory presented by equations between polymorphically-typed
terms. In doing so, we develop: signatures for polymorphic

term constructors built on top of signatures for polymorphic
types; algebraic theories giving rise to the syntax and semantics of polymorphic types and terms, and thereby to equationalpresentations and their models; and a sound and complete
logical framework for equational reasoning about polymorphic
algebraic theories.
Our approach is not based on a specific polymorphic
λ-calculus. It is more general, and captures varieties of polymorphic systems that include extended λ-calculi as particular
examples. The necessary background for our work follows.
1. Abstract syntax and variable binding. Our starting pointis the algebraic model of abstract syntax with variable binding
in presheaf categories [10]. The prototypical example is thesyntax of untyped λ-terms:
x1 , . . . , xn ` xi

x1 , . . . , xn ` t x1 , . . . , xn ` s
x1 , . . . , xn ` t@s

x1 , . . . , xn , xn+1 ` t
x1 , . . . , xn ` λ(xn+1 .t)
Its abstract syntax is generated by three term constructors: thevariable former, the application @, and the abstraction λ. The
variable former is a nullary operation parameterised by thecontext, while @ is a binary function symbol; λ, however, is
not merely a unary function symbol, as it binds a variable(and thereby decreases the context). To model the general
phenomenon of variable binding (not only for λ-terms), Fiore,
Plotkin and Turi [10] took the presheaf category SetF as
universe of discourse. The category F has finite cardinals{1, . . . , n} (n ∈ N) as objects, for which we henceforth abusenotation and simply write n ∈ F, and all functions between
them as morphisms. Intuitively, this is the category of contexts
of nameless object variables (in the sense of de Bruijn [3])and their renamings. An important result of [10] is that theabstract syntax with variable binding (up to α-equivalence) of
any binding signature (viz. one with variable-binding function
symbols) is characterised as the initial algebra of a prescribed
endofunctor modelling a signature (e.g. for λ-terms).
For example, the signature endofunctor Σλ on SetF for theabstract syntax of λ-terms is given by Σλ (A) = V+A×A+δA
where each summand corresponds to each constructor. The
presheaf of variables V ∈ SetF is given by V(n) = n and theendofunctor δ on SetF , modelling context extension, is given
by δA(n) = A(n + 1).

A Σ-algebra for an endofunctor Σ is a pair (A, α) consisting of a carrier A and an algebra-structure map α : ΣA → A.
The initial Σλ -algebra can be constructed inductively as thepresheaf Λ of all λ-terms modulo α-equivalence. This explains
directly why presheaves are suited to model syntax withbinding; namely
a judgment n ` t

is modelled ast ∈ Λ(n) ,and the renaming of free variables in a λ-term according toρ : n → n0 in F is modelled by the presheaf action Λ(ρ) :Λ(n) → Λ(n0 ).
2. Object variables and metavariables. The above development was limited to the modelling of object-level abstract
syntax. There is however also a need for considering a metalevel. We explain this with an example.
When developing a theory of λ-calculus, one uses bothobject and meta variables. For instance, in the mathematicalvernacular (e.g. in the context of head normal forms), one may
consider the λ-term
λx. y M .
Here “x” and “y” are object-level variables, as the λ-calculus
is the object language; while, at the level of text, “M ” isa meta-level variable, standing for some λ-term. From theviewpoint of substitution, there is a crucial difference between
object variables and metavariables. Because of α-equivalence,
the operation of substituting a term for an object variable is
not a simple textual substitution, e.g (λx.y M )[y := xx] =(λx0 .y M )[y := xx] = λx0 .(xx) M for fresh x0 ; while thesubstitution of a term for a metavariable is:(λx. y M ){M 7→ xx} = λx. y (xx) .

(1)

Note that the object variable x is captured by the binder, something intended at the meta-level. Viewing these phenomena
from the object and meta level viewpoints, the two classesof variables are classified by their respective substitution
operations: capture-avoiding vs. possibly capturing.
3. Free Σ-monoids. Besides object-level abstract syntax, how
can metavariables and the distinction between substitutions forobject and meta variables be incorporated within the algebraic
model of syntax with binding? This problem was explored in
Hamana [16] and in Fiore [5, Part I].
A Σ-monoid (A, α, ν, µ) introduced by Fiore, Plotkin andTuri [10] consists of a Σ-algebra (A, α) and a monoid(ν : V → A, µ : A • A → A) with respect to the substitution
monoidal structure (V, •) on SetF that is compatible with thealgebra structure (i.e. µ ◦ (α • id) = α ◦ (Σµ) ◦ strength). The
unit ν models the variable former; while the multiplication µ
models object-variable substitution (here the tensor product •gives the arity of substitution).
The key is to use free Σ-monoids on presheaves ofmetavariables. Importantly, the free Σ-monoid over a presheafF
X ∈ Set¡ , denoted MX, is ¢constructed inductively as an
initial V + Σ(−) + X • (−) -algebra, and gives a presentation of syntax involving binding and metavariables. In thischaracterisation, the endofunctor V + Σ(−) models syntax
with binding (as in § I-1) and the endofunctor X • (−) models
the syntactic construct of metavariables:
M [t1 , . . . , tk ]where M ∈ X(k) is a metavariable and where the index
k, referred to as the arity of M, designates k free variables
in terms to be substituted for M. The terms t1 , . . . , tk are
replacements for these k free variables after instantiating M.
The freeness of MX states that every map θ : X → A,
for A a Σ-monoid, uniquely extends to a Σ-monoid homomorphism θ] : MX → A. It is here that the notion of
metavariable substitution appears. Syntactically, one understands θ as an assignment for meta-substitution and θ] as thecorresponding meta-substitution operation on terms involving
metavariables from X. For instance, in the language of freeΣ-monoids, example (1) above is formally recast as¡¢¡
θ] λ(x. y@ M[x]) = λ x. y@ (x@x) )for θ = {M 7→ 1@1} where 1 denotes a free variable.
The syntactic theory of abstract syntax with variable binding
and metavariables was introduced by Aczel [1]. This formal
language allowed him to consider a general framework of
rewrite rules for calculi with variable binding. This influenced
Klop’s Combinatory Reduction Systems [21]. Hamana clarified its algebraic semantics using Σ-monoids [17], extended it
to simply-typed case [19], and considered equational logic andrewriting systems with variable binding [18]. Fiore et al. [8,9]considered algebraic theories for such second-order equationalpresentations. The model theory and equational logic of thesewas only developed for sorted (e.g. untyped and simply-typed)
languages.
4. Polymorphic abstract syntax. The work [20] tackled thealgebraic modelling of polymorphically-typed abstract syntax.
A crucial departure from the many-sorted case [24,4] is theneed for a dependent indexing structure on contexts and types
to capture the algebraic structure of polymorphic terms. In apolymorphic system, such as System F, well-typed terms areformulated using judgments of the following form:

(2)
term
type
context context

term

resulttype

The arrows here indicate dependency, as type variables inn ∈ F (which refers to the set {1, . . . , n} of nameless typevariables) may appear in any of the other parts of the judgment.
This dependence is more complex than in the untyped casen ` t (where only n ∈ F is a required index and therefore SetF
suffices). To model such dependent context and type structureswith respect to a universe of types U ∈ SetF , [20] introduced
the category GU of contexts and result types defined asand identified the Grothendieckconstruction [15] (for whichR
we use the notation ) as the key to capture the dependence (2).
The universe of discourse SetGU was then shown to beappropriate for modelling polymorphically-typed object-level
syntax [20], and Fiore [6] further isolated the notion of discrete
generalised polynomial functor as a suitable mathematicalstructure for this purpose. Here U is the “type universe” (withU (n) the set of types under the type context n) and F ↓ (U n)is the category of term contexts with types in U (n).
5. This paper. We develop polymorphic algebraic theories
founded on these earlier works. We incorporate the notionsof metavariables and Σ-monoids reviewed in § I-2 and I-3
into the algebraic polymorphic setting reviewed in § I-4. Syntactically, the framework encompasses meta-types (viz. types
with type metavariables) and meta-terms (viz. terms with bothmeta-types and term metavariables). We explain why this isnecessary next.
Consider the β-axiom of typed λ-calculus:Γ ` (λxσ .M ) N = N [x := N ] : τ .
Is this a single axiom? One usually thinks so, but this is infact a schema of axioms, as M and N are metavariables, andσ and τ are metavariables for types. Therefore, it should be
regarded as a representation of a family of axioms of the object
system, indexed by all possible object terms M, N and object
types σ, τ . This process reflects the formulation of signatures.
Following this line, then, λ-abstraction should also be regarded
as a family of function symbols λσ,τ : (σ)τ → σ ⇒ τ indexedby object types σ, τ . However, one usually keeps σ and τ
as meta-level types (henceforth referred to as meta-types) andconsiders a single λσ,τ to develop a theory.
Here, we will precisely formulate the meta and object variable distinction. In polymorphic algebraic theory, λ-abstraction
is formalised as a single function symbol specified byS : ∗, T : ∗. abs : (S)T → S ⇒ T

where S and T are type metavariables, and where . separates
a metavariable context and the arity information of a function
symbol using meta-types (as e.g. S ⇒ T). This leads to an
important clarification. Up to this point, we have encountered
two type universes for formalising a theory:(i) The universe of all object types (denoted by M0).
(ii) The universe of all meta-types (denoted by MS).
Clearly, the universes of object types and of meta-types musthave similar mathematical structure. What is this precisely?
Moreover, the semantics of the type universe must also havesuch a structure. This is the first step to answer the question
posed at the beginning of the Introduction: “what are polymorphic calculi?”. Namely, we need to clarify at first what isa universe of polymorphic types. Our answer isa universe of polymorphic types should be a Σ-monoid,for Σ a signature of type constructors. Note that M0 is
the initial Σ-monoid, while MS is a free Σ-monoid. The

mathematical theory naturally requires one to deal with such
multiple universes, and it is in this sense that we refer to it as
being multiversal.
6. Organisation. The paper is organised as follows. We
introduce the notion of polymorphic signature in Section II
and their corresponding endofunctors in Section III. We axiomatise type-in-term substitution in Section IV. We further
define polymorphic structures as a general algebraic model in
Section V. In Section VI, we present Polymorphic Equational
Logic. Finally, in Section VII, we exemplify how polymorphic
algebraic theories specify concrete calculi.
7. Future work. Various directions for further work arepossible. A promising one is to apply the mathematical theoryof the paper to mechanised formalisation (such as in Coq [2]).
Polymorphic algebraic theories of effects, which are here
only exemplified, should be worked out in detail.
An algebraic theory for the π-calculus has been given [31].
Along this line, an algebraic theory for the polymorphic πcalculus [27] in the setting of polymorphic algebraic theories
seems a challenging problem.
II. T YPE U NIVERSES AND P OLYMORPHIC S IGNATURES
We start motivating the development with the prototypicalexample of System F, illustrating and explaining how ournotion of polymorphic signature specifies type and term structures.
Example II.1 (System F [13,29]) The polymorphic signatureΣF = (ΣFTy , ΣFTm ) for System F consists of: a type signature
ΣFTy = { b : ∗, ⇒ : ∗, ∗ → ∗, ∀ : (∗)∗ → ∗ } which
specifies type constructors. The signature ΣFTm for terms is
S, T : ∗

. abs
. app
T : (∗)∗. tabsS : ∗, T : (∗)∗ . tapp

S, T : ∗: (S)T: S ⇒ T, S
: hαiT[α]¡¢: ∀ α.T[α]

→ S⇒T
→ T
→ ∀(α.T[α])→ T[S]Let us now see how the term signature faithfully encodes
the vernacular typing rules, considering the term and typeabstraction rules:Ξ | Γ, x : σ ` t : τΞ, α | Γ ` t : τΞ | Γ ` λx : σ. t : σ ⇒ τΞ | Γ ` Λα. t : ∀α. τThe arity of the abs term constructor is parameterised by
two type metavariables S and T, both of arity ∗ and thereby to
be understood as representing types. The source arity (S)Tof abs represents the premise of the term-abstraction rule,
expressing that it consists of a term of type T in a context
extended with a fresh term variable of type S. Note that the
informal metavariables σ and τ are respectively formalised bymeans of the formal metavariables S and T. The target arity
S ⇒ T of abs represents the type of the term in the conclusionof the rule.
The arity of the tabs term constructor is parameterised by ametavariable T of arity (∗)∗ representing an open type with one
type variable. The source arity hαiT[α] of tabs represents thepremise of the type-abstraction rule, expressing that it consistsof a term of open type T[α] in a context extended with a freshtype variable α. Function symbol declarations are meant to
be instantiated to concrete cases. For instance, abs : (S)T →S ⇒ T is instantiated to absθ : (nat)bool → nat ⇒ bool underθ = {S 7→ nat, T 7→ bool}. The formal treatment follows.
Definition II.2 A type signature Σ Ty is a set of type constructors with arities specified as c : (∗n1 )∗, · · · , (∗n` )∗ → ∗with ni ∈ N. The intended meaning here is that of c taking `arguments with the i-th argument binding ni type variables.
Definition II.3 A type metavariable S of arity n ∈ N is
declared as S : (∗n )∗, with the prefix omitted when n = 0. A
set of type metavariables S corresponds to an N-indexed set{S(k)}k∈N where the S(k) are the sets of metavariables in S
of arity k. It`can be considered as the presheaf S ∈ SetF givenby S(n) = k∈N S(k) × F(k, n).
A type signature is a binding signature in the sense of [10]and, as such, induces a signature functor Σ Ty on SetF (cf. § I1). We let MX denote the free Σ Ty -monoid on a presheaf
X ∈ SetF [16,5] (cf. § I-3), being particularly interested inthis construction when performed on a presheaf of typemetavariables.
For a set of type metavariable declarations S, the presheaf
MS ∈ SetF consists of meta-types in context, with metavariables from S. We use the notation (S . n ` τ ) forτ ∈ MS(n). Such a meta-type τ may contain metavariablesfrom S and n type variables. Furthermore, we implicitly use
the technique of de Bruijn levels [3] for representing abstract
syntax with variable binding. For example, in the context of
Example II.1, the meta-type ∀(α.T[α]), where T is a typemetavariable of arity 1, stands for ∀(1.T[1]). Also, the source
arity hαi(T[α]) of tabs stands for h1i(T[1]).
Definition II.4 A type universe U for a type signature Σ Ty isa Σ Ty -monoid. A morphism of type universes is a Σ Ty -monoid
homomorphism.
A typical example of a type universe is M0 (the universeof object types) and, more generally, MS (the universe ofmeta-types with metavariables from S). A non-syntactic typeuniverse features in the PL-category semantics of System F(Example VII.3).
−→
As a notational convention, we use the vector notation (−)
for sequences; the length function for these is denoted | − |.
Definition II.5 A polymorphic signature Σ = (Σ Ty , Σ Tm )consists of a type signature Σ Ty with a term signature Σ Tm
given by a set of function symbols with arities of the form→)τ , . . . , hk i(→−
S . f : hk1 i(−σ
1 1` σ l )τ ` → τ

Example II.6 (Polymorphic FPC [23]) The type signatureΣ Ty is ΣFTy extended with +, × : ∗, ∗ → ∗ and µ : (∗)∗ → ∗.
An excerpt of the term signature follows:
T 1 , T 2 , T : ∗ . case : T 1 + T 2 , ( T 1 ) T , ( T 2 ) T → T
T : (∗)∗
T : (∗)∗. intro: T[µ(α.T[α])]. elim : µ(α.T[α])→ µ(α.T[α])→ T[µ(α.T[α])]An important point to note above is that the source and target
arities of function symbols are written in the language of free
Σ Ty -monoids [16,5] (cf. § I-3), rather than in an informal metalanguage.
Example II.7 (Existential λ-calculus [11]) The type signature is given by⊥:∗ ,¬:∗→∗ ,

∧ : ∗, ∗ → ∗ ,∃ : (∗)∗ → ∗ .

As for the terms, we consider the following two key rules:Ξ | Γ ` s : σ{α := τ } Ξ | Γ ` s : ∃(α.σ) Ξ, α | Γ, x : σ ` t : τΞ | Γ ` hτ , si : ∃(α.σ)Ξ | Γ ` unpack s as hα, xi in t : τ

In the unpack rule, α does not appear free in Γ, τ . The term
signature corresponding to these two rules is thus:¡¢
S : (∗)∗, T : ∗ . pack
: S[T] → ∃ α.S[α]¡¢S : (∗)∗, T : ∗ . unpack : ∃ α. S[α] , hαi( S[α]) T → T
Note that the second argument of the function symbol unpackis specified under a type metavariable context with T : ∗thereby enforcing the side condition of the rule that α does
not appear free in τ .
Example II.8 (Global state) The signature for a basic algebraic theory of global state [28] has type signature L : ∗ forlocations, E : ∗ for expressions, and Bool, Nat : ∗ for Boolean
and natural number values. The term signatureV:∗V:∗. lookup : L, (V)E → E. update : V, L, E → E

provides operations that are parameterised by types. This isunlike the original treatment [28], where the parameterisationis only treated informally. An algebraic theory over this signature is first-order with variable binding and polymorphism,
without recourse to λ-calculi. This style may be useful for
more flexible algebraic characterisation of effects [28].
As shown in the examples, polymorphic signatures are
suitable for the specification of a wide variety of polymorphic languages. Indeed, the notion encompasses polymorphic
types (with variable binding and type metavariables) in the
broad sense of them being variable types, as referred toby Girard [14], together with polymorphic function symbols(parameterised by type metavariables) between them.

(3)
III. P OLYMORPHIC S IGNATURE F UNCTORS

where ` ∈ N and S is a set of type metavariable declarations→
with respect to which S . ki ` −σ i and S . ki ` τ i for all
1 ≤ i ≤ `, and S . 0 ` τ . The intended meaning here isthat of f taking ` arguments with the i-th argument binding−
ki type variables and |→σ i | term variables.

This section presents the categorical semantics of polymorphic signatures. In the spirit of categorical algebra, this is doneby associating signatures with endofunctors that interpret thearity of function symbols (§ III-D). As customary, then, models
arise as endofunctor algebras.

A. Meta-substitution
Definition III.1 For a small category C, we use the notation|C| for the set of its objects; while, for a presheaf P ∈ SetC ,we write |P | for its underlying indexed set in Set|C| . The left
adjoint to the functor | − | : SetC → Set|C| is denoted by(−). (The definition of S in Def. II.3 is the instance of thisconstruction for C = F.)
Definition III.2 Let S be a set of type metavariable declarations and let U be a type universe. An assignment θ : S Ãn U(n ∈ N) is an N-indexed function θ : S → |δ n U | . Henceforth,since [S ⇒ U ](n) ∼= SetN (S, |δ n U |), the exponential presheaf
F[S ⇒ U ] ∈ Set will be regarded as consisting of assignments.
A main result of [5, Part I] established that the free
Σ Ty -monoid monad M is strong with respect to the cartesianclosed structure of SetF . This has two important consequences
for us here: for every type universe U , the universal extension
map internalises as a morphism M(X) × [X ⇒ U ] → U in
SetF and every presheaf δ n U ∼= [ Vn ⇒ U ] ∈ SetF (n ∈ N)
pointwise acquires a canonical type-universe structure. One
thus obtains a meta-substitution operation (or interpretation
function) M(S) × [S ⇒ δ n U ] → δ n U of meta-types underassignments, for which we will use the following notation
S . k ` τ , θ : S Ãn U 7→ τ θ ∈ U (n + k) .
B. Contexts for polymorphism
Following [20], the universes of discourse for the interpretation of polymorphic signatures will be categories ofpresheaves on small categories of contexts that arise from theGrothendieck construction [15].
The (covariant) Grothendieck construction on a functor F : F → C , for C a full subcategory of the large category ofRlocallyRsmall categories and functors, is the categoryI∈Fdenoted F or
F(I) with objects given by pairs I ∈ F
and A ∈ F(I), and morphisms (f, ϕ) : (I, A) → (J, B) withf : I → J in F and ϕ : F(f )(A) → B in F(J).
We use the Grothendieck construction for manufacturingcategories of contexts. For a set T (of sorts),
theopcategory F ↓ T
R n∈F(of T -sorted contexts) is the opposite of
T n . Thus, it
has objects Γ : |Γ| → T with |Γ| ∈ F and morphisms ρ :Γ → Γ0 given by maps ρ : |Γ| → |Γ0 | in F such that Γ =Γ0 ◦ρ : |Γ| → T . Every presheaf T ∈ SetF (of sorts in context)
induces a functor F ↓ (T −) : F → Cat, for Cat the categoryof small categories and functors. The category
Z n∈F
def
F(T ) =F ↓ (T n)(of T -sorted contexts) has objects (n|Γ) with n ∈ F andΓ ∈ F ↓ (T n), and morphisms(ρ, π)→ (n0 |Γ0 ) with¡
¢ : (n|Γ)00
ρ : n → n in F and π : (T ρ) ◦ Γ → Γ in F ↓ (T n0 ).
We will also need to consider indexed versions of thisconstruction. To this end, for a presheaf U ∈ SetF , we define
Z n∈F
def
H(T, U ) =F ↓ (T n) × U n .

This category has objects (n | Γ ` τ ) with (n | Γ) ∈ FT andτ ∈ U n, and morphisms (n | Γ ` τ ) → (n0 | Γ0 ` τ 0 ) given
by maps (ρ, π) : (n|Γ) → (n0 |Γ0 ) in FT such that (U ρ)τ = τ 0 .
The category GU for contexts and result types (cf. § I-4) isdefined as H(U, U ).
C. Generalised polynomial functors
A central technical tool in our development is the notion ofgeneralised polynomial functor introduced in [6]. This fits ageneral abstract scheme for defining polynomial constructions
that also incorporates the notion of dependent polynomial
functor [26,12]. This section reviews the basics, deferring
details to [6]. Recall that every f : X → Y in Cat induces theadjoint situations
f! a f ∗ a f∗ : SetX → SetY
where f ∗ = (−) ◦ f and f! and f∗ are respectively given byleft and right Kan extending along f [15,22]. For instance,
the adjunction (−) a | − | : SetC → Set|C| introduced in
Definition III.1 amounts to i! a i∗ for i the inclusion |C| → C.
s
a /
t /
J
A polynomial P is a diagram A o
I
B in Cat.
The generalised polynomial functor induced by P is
FP = t! a∗ s∗ : SetA → SetB .

(4)

A polynomial diagram`is discrete `when its component` a :I → J is of the form i∈I ∇Li : i∈I Li · Ci → `i∈I Ci
for a set I and finite sets Li , where L · C =`∈L Cand ∇L : L · C → C is the codiagonal [IdC ]`∈L . As wewill see, discrete generalised polynomial functors provide an
expressive and flexible formalism. Indeed, since they admit
inductive constructions of free algebras [6, Prop. 5.1], in thefollowing two sections we will use them to model polymorphic
signatures (§ III-D) and type-in-term substitution (§ IV).
D. Polymorphic signature functors
We define the signature functor corresponding to a polymorphic signature Σ. This is done on a type universe U
for Σ Ty on the universe of discourse given by the presheaf
category SetGU .
To explain the approach, we start by analysing concrete
cases in System F (Example II.1). For the term abstraction
function symbol
S : ∗, T : ∗ . abs : ( S) T → S ⇒ T

the corresponding operation of an algebra A ∈ SetGU should
be given by a natural map
absA : A( n | Γ, σ ` τ ) → A( n | Γ ` σ ⇒U τ ) .
using an assignment θ = {S 7→ σ, T 7→ τ }, where S ⇒ T isinterpreted as σ ⇒U τ . Some operations may also change thecontext for type variables, as in the case of the type abstraction:¡¢tabsA : A( n + 1 | Γ ` τ ) → A n | Γ ` ∀U(τ ) .
To obtain these kind of algebraic operations from the arity
specification of function symbols, one needs to formulatethe instantiation of meta-types in arities by types in theuniverse U by means of meta-substitutions, and incorporate
the extension of contexts for type variables as prescribedby source arities. Technically,¡ this requires¢ the use of theGrothendieck construction H U, [S ⇒ U ] of § III-B, for S
a set of metavariable declarations.
Definition III.3 Let Σ be a polymorphic signature and U atype universe for Σ Ty . To every function symbol f ∈ Σ Tm
we associate the following discrete polynomial Pf
GU o

sf

¢
¡
` · H U, [S ⇒ U ]∇`¡¢/ H U, [S ⇒ U ]

tf

/ GU

where
given by¡ the source and¢ target functors¡ are respectively¢−
sf i, (n | Γ ` θ) = (n + ki | Γi + h→σ i θi i ` τ i θi ) andtf ( n | Γ ` θ ) = ( n | Γ ` τ θ ), where Γi and θi respectively arise from Γ and θ by the presheaf action along the
coproduct injections ki ,→ n + ki .
GUThe signature functor Σ on Set
is defined as the discrete`
generalised polynomial functor f ∈Σ Tm FPf . This is explicitly
given bya Y→
ΣA( n | Γ ` u ) =A( n + k | Γ , −σ θ `τ θ )
i

i

i i

i i

f,θ i∈`

where the coproduct ranges over function symbols→)τ , . . . , hk i(−→(S . f : hk1 i(−σin Σ Tm and1 1` σ ` )τ ` → τ )assignments θ : S Ãn U such that τ θ = u ∈ U (n).

The axioms for type-in-term substitution are analogous
to the ones given for substitution algebras in [10]. To
present them, we need introduce the following notation: forρ : ` → m in F, U ∈ SetF , and A ∈ SetGU , we let ρUn =U (n + ρ) : U (n + `) →¡ U (n + m) and ρA
=
A(n
+
ρ,
id) :
n
¢
U
A(n + ` | Γ ` τ ) → A n + m | ρU
◦
Γ
`
ρ
(τ
)
;
and
conn
n
sider the weakening, contraction, and swapping maps up :0 → 1, con : 2 → 1, and sw : 2 → 2 in F.
Definition IV.1 Let (U, ν, µ) be a type universe. A type-interm substitution for A ∈ SetGU is an algebra ς :↑ A → A in
SetGU subject to the following axioms:a ∈ A(n | Γ ` τ ), σ ∈ Un ` ς n (upAn a, σ) = aAa ∈ A(n + 2 | Γ ` τ )` ς n+1 (a, newUn ) = conn a0a ∈ A(n + 2 | Γ ` τ ), σ ∈ U (n + 1), σ ∈ U (n)U 00` ς n (ς n+1 (a, σ), σ 0 ) = ς n (ς n+1 (swA
n a, upn σ ), σ{σ })where new : 1 → δU (a generic new variable) is the transposeof the point ν : V → U .
The axioms have an intuitive reading; e.g. the first one
expresses that substituting for a type variable not free in aterm does not affect the term.
GU
The presheaf ofis defined as¡ object¢¡variables¢ V ∈ Set
V(n | Γ ` τ ) = F ↓ U n hτ i, Γ ∼= { x ∈ |Γ| : Γ(x) = τ }.
It has a type-in-term substitution structure ς V : ↑ V → V
given by maps that interpret a variable of type τ in context Γas one of type τ {σ} in context Γ{σ}.

IV. T YPE - IN - TERM S UBSTITUTION
The monoid multiplication of a type universe provides anoperation that models simultaneous capture-avoiding typein-type substitution. Polymorphic terms have type variables
and the need for instantiating them leads to a type-in-term
substitution operation that should be modelled. We address
this issue by giving an algebraic axiomatisation of type-interm substitution.
Let (U, ν, µ) be a type universe. For τ ∈ U (n + `)and σ i ∈ U (n) with 1 ≤ i ≤ `, we denote byτ {σ 1 , . . . , σ ` } the multi-variable capture-avoiding substitution µn (τ ; ν n (1), . . . , ν n (n), σ 1 , . . . , σ ` ) ∈ U (n); pointwise
extendingto Γ{σ 1 , . . . , σ ` } ∈ F ↓ (U n) for¡ the notation¢
Γ ∈ F ↓ U (n + `) . Our aim is to define algebraic structure
on a presheaf A ∈ SetGU amounting to functions¡¢
ς n (−, σ) : A(n + 1 | Γ ` τ ) → A n | Γ{σ} ` τ {σ} (5)with (n | Γ ` τ ) ∈ GU and σ ∈ U (n), that we will later on
axiomatise so as to model the substitution of a distinguishedtype variable by a type. We again invoke the formalismof generalised polynomial functors and consider the discrete
polynomial P
GU os

H(δU, δU × U )

t

/ GU

with s(n | Γ ` τ , σ) = (n + 1 | Γ ` τ ) and t(n | Γ ` τ , σ) =(n | Γ{σ} ` τ {σ}). We write ↑ for the discrete generalised
polynomial functor FP on SetGU induced by P , noting thatalgebra-structure maps ↑ A → A amount to (5).

V. P OLYMORPHIC S TRUCTURES
We introduce polymorphic structures. They provide a general basic notion of algebraic model, and thereby of abstract
syntax, for polymorphic algebraic theories.
In the vein of [24,4,20], for A, B ∈ SetGU , we define(A • B) ∈ SetGU by the coend¡ (A • B)(n ¢| Γ ` τ ) =R ∆∈F↓UQ
n
A(n | ∆ ` τ )× 1≤i≤|∆| B n | Γ ` ∆(i) remarking
that (V, •) provides a monoidal structure on SetGU suitable forconsidering monoids with polymorphic algebraic structure.
Definition V.1 Let Σ be a signature and U a type universe.
A (Σ, U )-polymorphic structure consists of(i) a Σ-monoid (A, α, ν, µ) in SetGU for Σ the signaturefunctor on SetGU obtained by Def. III.3, and(ii) a type-in-term substitution ς : ↑ A → A
that are compatible in the sense that the following commute/ Σ ↑A Σς / ΣA
↑ ΣA
α

↑α

²
↑A

↑V

ςV

ν

↑ν

²
↑A

/V

ς

²
/A

ς

↑ (A • A)²/A/ ↑ A • ↑ A ς•ς / A • A
µ

↑µ

²
↑A

ς

²
/A

where ↑Σ(−) → Σ ↑(−) and ↑(−• =) → ↑(−) • ↑(=) areappropriate coercion maps.

→)τ , . . . , hk i(−→
Tm(S . f : hk1 i(−σ
1 1` σ ` )τ ` → τ ) ∈ Σ[ S⇒U ]

θ : S Ãn U

(Var)

(x : τ ) ∈ Γ(Fun)x ∈ NU Z(n | Γ ` τ )−k i = |→αi |θi = ıi(θ) (ıi : n ,→ n + ki )−→−→t ∈ N Z(n + k | Γ, x : σ θ ` τ θ ) (1 ≤ i ≤ `)
i

U

i

i

i i

i i

→. −
→
−
→−
→
fθ ( −
α1 x1 .t1 , . . . , αl. xl .tl ) ∈ NU Z(n | Γ ` τ θ)→−σ = σ 1 , . . . , σ k ∈ U (n)¡¢−→ti ∈ NU Z n | Γ ` τ i { σ }(1 ≤ i ≤ `)(MVar)¡−→−→ ¢Z b σ c[t , . . . , t ] ∈ N Z n | Γ ` τ { σ }Z ∈ Z(n + k | x1 : τ 1 , . . . , x` : τ ` ` τ )

1

`

U



NB: In (Fun), for S = Si : (∗ni ) ∗ 1≤i≤m , the formal concretion fθ may be denoted fθ(S1 ),...,θ(Sm ) or simply f when the omission isinferable from the context. These function symbols bind both type and term variables and we implicitly assume the technique of de Bruijn
levels [3] for their representation. Each θi is essentially the same substitution as θ, shifted to the index n + ki to apply it under the binders
−
→
−
→
−
→
−
→
→
→
→
αi . A meta-term Zb−
σ c[ t ] may be denoted by Z[ t ] when |−σ | = 0, and by Zb−
σ c when | t | = 0.
Fig. 1. Rules for NU Z

Morphisms of (Σ, U )-polymorphic structures, referred toas (Σ, U )-polymorphic translations, are maps that are bothΣ-monoid morphisms and ↑-algebra homomorphisms.
The category of (Σ, U )-polymorphic structures and (Σ, U )polymorphic translations is denoted Poly(Σ, U ).
A. Free polymorphic structures
From the theories of equational systems [7] and of discrete
generalised polynomial functors [6] we have the following
result.
Theorem V.2 The forgetful functor Poly(Σ, U ) → Set
monadic.

GUis

We outline a construction of free (Σ, U )-polymorphic structures, obtaining the underlying indexed set of the free polymorphic structure NU X ∈ SetGU on a presheaf X ∈ SetGU
as a quotient of an indexed set NU |X| ∈ Set|GU | .
For Z ∈ Set|GU | , the indexed set NU Z ∈ Set|GU | has
syntactic character and is defined by the rules of Fig. 1. In
this context, we let |NU X| be given by the quotient of NU |X|
under the congruence generated by the identification→−→
Z b σ c[t , . . . , t] = Z 0 b−
σ c[t , . . . , t 0 ]
(6)
π1

π|∆|

1

|∆ |

→
for n ∈ F, π : ∆ → ∆0 in F ↓ (U n), Z ∈ X(n+|−σ | | ∆ ` τ ),→−00
and Z = X(id, π)(Z) ∈ X(n+| σ | | ∆ ` τ ). This quotientarises from the coend formula of the tensor product •. The
presheaf and polymorphic structures of NU X are essentiallygiven syntactically.
B. Polymorphic abstract syntax with metavariables
We now consider free (Σ, U )-polymorphic structures that
correspond to polymorphic abstract syntax with metavariables.
First, one constructs a syntactic type universe U as a free Σ Ty monoid. On top of this, one constructs polymorphic abstract
syntax as a free (Σ, U )-polymorphic structure over generators
given by indexed sets of term metavariables.
An indexed set Z ∈ Set|GU | is regarded as consisting of→
metavariable declarations, where Z ∈ Z(n | −σ ` τ ) stands for−→the arity declaration Z : hni( σ )τ . Such metavariables are to beinstantiated by terms involving n type variables and variables→of types −σ.
Every indexed set Z ∈ Set|GU | freely gives rise to thepresheaf Z ∈ SetGU . In view of the following characterisation,the (Σ, U )-polymorphic structure NU (Z) ∈ SetGU is given inpurely syntactic terms: |NU Z| ∼= NU Z for Z(n | Γ ` τ )given by
a
£
¤ £
¤
¡
¢
Uρσ ≡ τ × (Uρ) ◦ ∆ ≡ Γ × Z k | ∆ ` σ .
(k | ∆ ` σ) ∈ GU
ρ ∈ F(k, n)

We refer to elements of NU Z(n | Γ ` τ ) as meta-terms.
We will introduce next the notion of assignment and theirinduced interpretation functions, yielding operations of metasubstitution (i.e. substitution for metavariables in meta-terms).
(k|∆)
For (k|∆) ∈ FU (cf.
on¡ § III-B),¢∗ the endofunctor δGU
Set
is defined as d(k|∆) for d(k|∆) the endofunctor
on GU given by d(k|∆)(n | Γ ` τ ) = ( k + n | ∆, Γ ` (τ ) )where (∆, Γ) = (U ı ◦ ∆) + (U  ◦ Γ) for ı and  the first andsecond coproduct injections into k + n.
Definition V.3 Let Z be a set of metavariable declarations
and A a polymorphic structure. An assignment for ϑ :Z Ã(k|∆) A, where (k|∆) ∈ FU , is an |GU |-indexed function
ϑ : Z → |δ (k|∆) A|.
For every (Σ, U )-polymorphic structure A, the presheafδ (k|∆) A inherits a polymorphic structure. As in the case of theextension to a Σ-monoid morphism explained in § I-3, by theuniversal property of NU Z, an assignment ϑ uniquely extends
to a (Σ, U )-polymorphic translation ϑ] giving the interpretation function of a meta-term in a polymorphic structure A.
This is explicitly defined as follows.
Definition V.4 (Interpretation function) For a (Σ, U )polymorphic structure (A, α, ν, µ, ς), the universal extensionof a morphism ϑ : X → A in SetGU is the (Σ, U )polymorphic translation ϑ] : NU Z → A given as follows:ϑ] : NU Z(n | Γ ` τ ) −→ A(n | Γ ` τ )ϑ] (x) = ν(x)
]
]
→.−
→
−
→−
→
A
ϑ] (f (−
α1 x1 .t1 , . . . , α` . x` .t` )) = f ( ϑ (t1 ), . . . , ϑ (t` ) )
−−→¢
¡
→
−
→
−
ϑ] (Zb−σ c[ t ]) = µ ς( ϑ(Z), →σ ); ϑ] (t)where f A is the algebra operation for f in (A, α) andwhere, extending the notation introduced in (5), for a ∈A(n + ` | Γ ` τ ) and¡ σ i ∈ U (n) with 1 ≤ i ≤¢ `, we setς(a, σ 1 , . . . , σ ` ) = ς · · · ς(a, ı1 (σ 1 )) · · · , ı` (σ ` ) for ıi the
coproduct injection n ,→ n + ` − i.
C. The multiverse of polymorphic structures
We combine all (Σ, U )-polymorphic structures, varying
over all type universes U into a single category Poly(Σ). This
category abstractly arises as the Grothendieck construction
Z U
def
Poly(Σ) =Poly(Σ, U )opapplied to a functor Poly(Σ, −) : Σ Ty -Mon → CAT; U 7→
Poly(Σ, U ). This definition relies on that fact that if (U 0 , A0 )is a Σ-polymorphic structure then so is (U, A0 GL−M) for every
morphism of type universes L−M : U → U 0 .
Definition V.5 A Σ-polymorphic structure (U, A) consists ofa type universe U and a (Σ, U )-polymorphic structure A.
A Σ-polymorphic translation between Σ-polymorphic
structures(L−M, ϕ) : (U, A) −→ (U 0 , A0 )consists of a pair of maps:- a morphism L−M : U → U 0 of type universes, and- a (Σ, U )-polymorphic translation ϕ : A −→ A0 GL−M.
The idea behind these maps is that they provide two-levelledtranslations: L−M translates types in U to U 0 and ϕ translateselements from A to A0 taking a shift of universe into account.
The category Poly(Σ) consists of Σ-polymorphic structuresand Σ-polymorphic translations.
Universe shift. The category Poly(Σ) supports a notionof translation between polymorphic structures on possibly
different universes. As an application, we indicate how one
can transport a meta-term on a universe to another one.
Let L−M : W → U be a morphism of type universes,
translating types τ ∈ W (n) to types Lτ M ∈ U (n). The functor
FL−M : FW → FU¡ translates thus
¢ contexts Γ ∈ F ↓ (W n)to contexts LΓM=(F↓L−M)◦Γ∈ F↓(U n). Furthermore,n¯¯
the functor ¯GL−M¯! : Set|GW | → Set|GU | translates a set ofmetavariable declarations Z on the universe W to the setof metavariable¡ declarations¢ LZM on the universe U given
by Z ∈ LZM n | LΓM ` Lτ M⇐⇒ Z ∈ ¯Z( n | Γ¡ ` τ )¢¯.
Finally, we have the assignment Z → ¯NU LZM GL−M ¯,→→
mapping the metavariable Z ∈ Z(n | −x :−σ ` τ ) to the
¡ −
¢
−→
−
→
→
meta-term Z[ x ] ∈ NU LZM n | x : LσM ` Lτ M , that induces
the polymorphic
translation
L−M : NWZ( n | Γ ` τ ) →¡¢NU LZM n | LΓM ` Lτ M whose effect is to translate types
within meta-terms.

VI. P OLYMORPHIC E QUATIONAL L OGIC
We introduce Polymorphic Equational Logic (PEL): a soundand complete logical framework for equational reasoning
about polymorphic algebraic theories.
The equational judgments of PEL are of the form
Z . n | Γ `W s = t : τ(7)where W is a type universe, Z is a set of metavariable declarations and s, t ∈ NWZ(n | Γ ` τ ) are meta-terms. When W
is a universe of meta-types MS for a set of type metavariabledeclarations S (as e.g. in Figs. 3, 4, 5), equational judgments
are written as S | Z . n | Γ ` s = t : τ . Sets of equational
judgments are referred to as axioms.
Definition VI.1 A Σ-polymorphic structure (U, A) satisfies
an equational judgment Z . n | Γ `W s = t : τ if
- for all morphisms of type universes L−M : W → U , and- for all assignments ϑ : Z Ã(k|∆) A(GL−M),
ϑ] (s) = ϑ] (t)holds in A(k + n | LΓ, ∆M ` Lτ M). An algebraic model of aset of axioms E is a polymorphic structure that satisfies all
the equational judgments in E.
A. PELThe deduction system of PEL is given by the inference rulesof Fig. 2. The notation [x := t] used in the (Sub) rule stands
for the capture-avoiding substitution of the object variable x
by the meta-term t. The application ρ(s) (resp. π(s)) replaces
type variables (resp. variables) in s by ρ (resp. π). PEL has
been synthesised from the mathematical model of polymorphic
structures on type universes using the following ideas.
(Ref), (Sym), (Tra): The rules of equivalence relations.
(Ax):
An axiom becomes a theorem.
(USh): Universe shift with respect ¡to the morphism¢ L−M :
NWZ( n | Γ ` τ ) → NU LZM n | LΓM ` Lτ M .
(Sub): Multiplication of the Σ-monoid NU Z.
(Fun): Σ-algebra structure of NU Z.
(MSub): Polymorphic translation ϑ] : NU Z → δ (k|∆) NU Z 0 .
(MVar): (Z • −)-algebra structure of NU Z.
(Act): Presheaf action of NU Z ∈ SetGU (cf. [20, § 3.2
Meaning of arrows]).
(TSub): Type-in-term substitution on NU Z.
Note that besides the equivalence-relation and axiom rules
common to all equational deductive systems, the above consistof congruence rules that reflect the various algebraic aspectsof polymorphic structures.
B. Soundness and completeness
Let U be a type universe. For a set of axioms E, define Z
to be the disjoint union of all the translations of metavariabledeclarations in the axioms of E into U . Consider then the term
polymorphic structure NU Z on U . Derivable equations fromE define an |GU |-indexed equivalence relation =E on |NU Z|,
and we set NUE Z(n | Γ ` τ ) = NU Z(n | Γ ` τ )/ =E .
Lemma VI.2 (U, NUE Z) is an algebraic model of E.

(Ref)(Sym)
Z . n | Γ `U s = t : τ
Z . n | Γ `U t = s : τZ . n | Γ `U t = t : τ(Ax)(Z . n | Γ `W s = t : τ ) ∈ E
Z . n | Γ `W s = t : τ

(USh)

i

i

θi = ıi(θ) (ıi : n ,→ n + ki )−−−−−→
X . n + ki | Γ, xi : σ i θi `U si = ti : τ i θi (1 ≤ i ≤ `)
→.−
→
−
→→
−
−
→−
→
−
→−
→
Z . n | Γ `U fθ (−α
1 x1.s1 , . . . , α`. x`. s` ) = fθ ( αl.x1.t1 , . . . , α`. x`. t` ) : τ θi(MSub)
ϑ : Z Ã(k|∆) NU Z 0(MVar)¡¢
Z : hn + ki(τ 1 , . . . , τ ` )τ ∈ Z−
Z . n | Γ ` s = t : τ {→σ}

Z . n | Γ `U s = t : τZ0]. k + n | ∆, Γ `U ϑ (s) = ϑ (t) : τ
ρ:m→nπ : ρ(Γ) → ∆Z . m | Γ `U s = t : τ(Act)Z . n | ∆ `U πρ(s) = πρ(t) : ρ(τ )−→σ = σ 1 , . . . , σ k ∈ U (n)(1 ≤ i ≤ `)
i
i
−
→
→
→
Z . n | Γ `U Zb σ c[s1 , . . . , s` ] = Zb−
σ c[t1 , . . . , t` ] : τ {−
σ}
U

]

→
k i = |−αi |[ S⇒U ]

θ : S Ãn U

(1 ≤ i ≤ m)

Z . n | x1 : σ 1 , . . . , xm : σ m `U t = t0 : τ−−→−−→
Z . n | Γ ` t[−x−−:=s ] = t0 [−
x−−:=
s]:τ
i

Z . n | Γ `W s = t : τ
L−M : W → U
LZM . n | LΓM `U LsM = LtM : Lτ M

(Fun)→)τ , . . . , hk i(−→
Tm(S . f : hk1 i(−σ
1 1` σ ` )τ ` → τ ) ∈ Σ(Sub)Z . n | Γ ` U si : σ i

U

(Tra)
Z . n | Γ `U s = t : τ Z . n | Γ `U t = u : τ
Z . n | Γ `U s = u : τi(TSub)
Z . n + 1 | Γ `U s = t : τσ ∈ U (n)Z . n | Γ{σ} `U s{σ} = t{σ} : τ {σ}Fig. 2. Polymorphic Equational Logic (PEL)

Vernacular notation(β)(type β)Γ ` (λx. M ) NΓ ` (Λα.M ) σ==

M [x := N ] : τM [α := σ] : τ [α := σ]Formal notation in PEL(β)(type β)S, T : ∗| M : (S)T, N : S . ` app( abs(x. M[x]), N ) =¡¢S : ∗, T : (∗)∗ | M : hαi T [α]. ` tapp tabs(α. Mbαc)
=

M[N]

:

MbSc :T
T[S]Fig. 3. Sample axioms for System F

Vernacular notation(let∧ )
(letη)(∃β)(∃η)Γ ` let hx1 , x2 i = hM1 , M2 i in MΓ ` let hx1 , x2 i = N in M [z := hx1 , x2 i]Γ ` unpack hι, N i as hα, xi in MΓ ` unpack N as hα, xi in M [z := hα, xi]

Formal notation in PEL(let ∧)(let η)(∃β)(∃η)

S1 , S2 , T : ∗| M : (S1 , S2 )T, M1 : S1 , M2 : S2 .
S1 , S2 , T : ∗| M : (S1 ∧S2 )T, N : S1 ∧S2.
¡¢S : (∗)∗, T , U : ∗ | M : hαi S [α] T , N : S[ U].
¡¢
S : (∗)∗, T : ∗| M : ∃(α.S[α]) T, N : ∃(α.S[α]) .

=
=
=
=

M [x1 := M1 , x2 := M2 ] : τM [z := N ]:τM [α := ι, x := N ]:τM [z := N ]:τ¡¢` let pair(M1 , M2 ), x1 .x2 .M[x1 , x2 ] = M[M1 , M2 ] : T¡¢` let N, x1 .x2 .M[pair(x1 , x2 )]= M[N]:T¡¢` unpackS,T packS,U (N), α.x.Mbαc[x] = MbUc[N] : T¡¢` unpackS,T N, α.x.M[packS,α (x)]= M[N]:T

Fig. 4. Sample axioms for the existential λ-calculus λ∃

¡
¢
. `:L
` lookup `, v.update(`, v, X)
= X
:E
¡
¢
¡
¢
V : ∗ | X : ( V, V )E . ` : L` lookup `, w.lookup(`, v.X[v, w]) = lookup `, v.X[v, v] : E¡¢
V:∗ | X:E
. ` : L, v, w : V ` update `, v, update(`, w, X)= update(`, w, X):E

V:∗ | X:E

Fig. 5. Sample axioms for global stateTheorem VI.3 Polymorphic equational logic is sound andcomplete; i.e., for all type universes U , an equational judgment(Z . n | Γ `U s = t : τ ) is derivable from a set of axioms E
in PEL iff it is satisfied by all the algebraic models of E.
VII. E XAMPLES
Example VII.1 Continuing with the examples of § II, sample
axioms of System F, the existential λ-calculus, and global
state are respectively presented as PEL equations in Figs. 3,4, and 5.
Example VII.2 (CPS translation [11]) Fujita [11] gave a
CPS translation from System F to the existential λ-calculus λ∃ .
The translation consists of a type translation (−)• from System
F types to λ∃ -types, together with a ¡CPS translation[[−]] from¢•
System F terms to λ∃ -terms (e.g. ∀(α.τ ) = ¬∃(α.¬τ • )and [[Λα.M ]] = λa. a (λk.unpack k as hα, ci in [[M ]]c)). The
CPS translation is sound and complete:Γ `F s = t : τ⇐⇒ ¬¬Γ• `λ∃ [[s]] = [[t]] : ¬¬τ • . (8)Interestingly, this pair of translations is an example of ournotion of polymorphic translation. Indeed, let TF (resp. T∃ )be the initial type universe for ΣFTy (resp. Σ∃Ty ) and let
ΛF = NTFF 0 (resp. Λ∃ = NTλ∃∃ 0) be the initial algebraic modelfor System F (resp. λ∃ ). The definition of (−)• determinesan ΣFTy -algebra structure on T∃ , and the definition¡ of [[−]]¢
determines a ΣFTm -algebra structure on Λ¬¬=Λ∃ G¬¬(−)∃
for ¬¬ the double negation endomap on T∃ . This yields a ΣF polymorphic structure (T∃ , Λ¬¬∃ ) which, by (8), is an algebraic
modelofSystem
F,
and
we
have
a ΣF -polymorphic translation¡¢(−)• , [[−]] : (TF , ΛF ) → (T∃ , Λ¬¬∃ ).
Example VII.3 (Categorical model of System F [30])Recall that a PL-category consists of a cartesian category C
with objects given by finite powers of a distinguished object Ω,a C-indexed cartesian closed category C(−, Ω) : Cop → CCC,
for CCC the large category of cartesian closed categories, andright adjoints to C(π 1 , Ω) : C(−, Ω) → C(−×Ω, Ω) satisfying
the Beck-Chevalley condition.
From a PL-category, one defines a polymorphic structure(U, PL) for System F by setting¯¯
U = ¯C(Ω(−) , Ω)¯ ∈ SetF ,¡Q¢
PL( n | Γ ` τ ) = C(Ωn , Ω).
1≤i≤|Γ| Γ(i), τ
Seely’s categorical interpretation of the types and terms of
System F determines ΣFTy and ΣFTm algebra structures on U
and PL. For example, for ( ∀ : (∗)∗ → ∗ ) ∈ ΣFTy , thecorresponding algebraic operation ∀U : δU → U is definedby the right adjoint to C(π 1 , Ω) : C(Ωn+1 , Ω) → C(Ωn , Ω).
The multiplication structures of both monoids U and PL
are given by composition.
The type-in-term
substitution for¡¢σ ∈ U(n) arises as C hidΩn , σi, Ω : PL(n + 1 | Γ ` τ ) →PL(n | Γ{σ} ` τ {σ}). Altogether, this yields an algebraic
model of System F.

ACKNOWLEDGMENTS
Makoto Hamana is supported in part by a grant from
Gunma University Foundation for Science and Technology
and the JSPS Grant-in-Aid for Scientific Research (25540002)“A Semantics of Core Haskell”.
R EFERENCES[1] P. Aczel. A general Church-Rosser theorem. Technical report, Universityof Manchester, 1978.
[2] N. Benton, C.-K. Hur, A. Kennedy, and C. McBride. Strongly typed term
representations in Coq. J. Autom. Reasoning, 49(2):141–159, 2012.
[3] N. de Bruijn. Lambda calculus notation with nameless dummies, a tool
for automatic formula manipulation, with application to the ChurchRosser theorem. Indagat. Math., 34:381–391, 1972.
[4] M. Fiore. Mathematical models of computational and combinatorial
structures. In FoSSaCS’05, LNCS 3441, pages 25–46, 2005.
[5] M. Fiore. Second-order and dependently-sorted abstract syntax. In
LICS’08, pages 57–68, 2008.
[6] M. Fiore. Discrete generalised polynomial functors. In ICALP’12, pages
214–226, 2012.
[7] M. Fiore and C.-K. Hur. On the construction of free algebras forequational systems. Theor. Comput. Sci., 410:1704–1729, 2008.
[8] M. Fiore and C.-K. Hur. Second-order equational logic. In CSL’10,
LNCS 6247, pages 320–335, 2010.
[9] M. Fiore and O. Mahmoud. Second-order algebraic theories. In
MFCS’10, LNCS 6281, pages 368–380, 2010.
[10] M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding.
In LICS’99, pages 193–202, 1999.
[11] K. Fujita. Galois embedding from polymorphic types into existential
types. In TLCA’05, pages 194–208, 2005.
[12] N. Gambino and M. Hyland. Wellfounded trees and dependent polynomial functors. In TYPES’03, pages 210–225, 2003.
[13] J.-Y. Girard. Interprétation Fonctionnelle et Élimination des Coupuresde l’Arithmétique d’Ordre Supérieur. Thèse de doctorat d’état, 1972.
[14] J.-Y. Girard. The System F of variable types, fifteen years later. Theor.
Comput. Sci., 45(2):159–192, 1986.
[15] A. Grothendieck. Catégories fibrées et descente (exposé VI). In SGA1,
LNM 244, pages 145–194. Springer-Verlag, 1970.
[16] M. Hamana. Free Σ-monoids: A higher-order syntax with metavariables.
In APLAS’04, LNCS 3301, pages 348–363, 2004.
[17] M. Hamana. Universal algebra for termination of higher-order rewriting.
In RTA’05, LNCS 3467, pages 135–149, 2005.
[18] M. Hamana. An initial algebra approach to term rewriting systems withvariable binders. Higher-Order and Symb. Comput., 19:231–262, 2006.
[19] M. Hamana. Higher-order semantic labelling for inductive datatypesystems. In PPDP’07, pages 97–108, 2007.
[20] M. Hamana. Polymorphic abstract syntax via Grothendieck construction.
In FoSSaCS’11, LNCS3467, pages 381–395, 2011.
[21] J.W. Klop. Combinatory Reduction Systems. PhD thesis, CWI,
Amsterdam, 1980. volume 127 of Mathematical Centre Tracts.
[22] F. W. Lawvere. Adjointness in foundations. Dialectica, 23:281–296,
1969.
[23] R. E. Møgelberg. From parametric polymorphism to models of polymorphic FPC. Math. Struct. in Compt. Sci., 19(4):639–686, 2009.
[24] M. Miculan and I. Scagnetto. A framework for typed HOAS andsemantics. In PPDP’03, pages 184–194. ACM Press, 2003.
[25] R. Milner. A theory of type polymorphism in programming. J. Comput.
Syst. Sci., 17(3):348–375, 1978.
[26] I. Moerdijk and E. Palmgren. Wellfounded trees in categories. Ann.
Pure Appl. Logic, 104:189–218, 2000.
[27] B. Pierce and D. Sangiorgi. Behavioral equivalence in the polymorphic
pi-calculus. J. ACM, 47(3):531–584, 2000.
[28] G. Plotkin and J. Power. Notions of computation determine monads. In
FoSSaCS’02, pages 342–356, 2002.
[29] J. Reynolds. Types, abstraction and parametric polymorphism. Inform.
Process., 83:513–523, 1983.
[30] R. A. G. Seely. Categorical semantics for higher order polymorphic
lambda calculus. J. Symb. Log., 52(4):969–989, 1987.
[31] I. Stark. Free-algebra models for the π-calculus. Theor. Comput. Sci.,
390(2–3):248–270, 2008.
[32] C. Strachey. Fundamental concepts in programming languages. HigherOrder and Symbolic Computation, 13:11–49, 2000.