ZU064-05-FPR

paper

14 March 2017

20:59

Under consideration for publication in J. Functional Programming

1

The Calculus of Dependent Lambda Eliminations
Aaron Stump
Computer Science, The University of Iowa, Iowa City, Iowa, USA
astump@acm.org

Abstract
Modern constructive type theory is based on pure dependently typed lambda calculus, augmented
with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent
Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New
typing constructs are defined which enable induction, as well as large eliminations with lambda
encodings. These constructs are constructor-constrained recursive types, and a lifting operation tolift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types,
the language is proved logically consistent. The power of CDLE is demonstrated through several
examples, which have been checked with a prototype implementation called Cedille.

1 Introduction
Lambda encodings are schemes for representing datatypes and related operations as purelambda terms. The Church encoding, where data are encoded as their own fold functions,is the best known (Church, 1941), and is typable in System F (Böhm & Berarducci, 1985;
Fortune et al., 1983). Lambda encodings were abandoned as a basis for constructive typetheory almost thirty years ago, due to the following problems, identified some time ago by
several authors (Coquand & Paulin, 1988; Werner, 1992):
1. Accessors (like predecessor for numerals, or head and tail for lists) are provably
asymptotically inefficient with the Church encoding (Parigot, 1989).
2. Induction principles are not derivable for lambda encodings (Geuvers, 2001).
3. Large eliminations, which compute types from data, are not possible with lambdaencoded data, at least not in normalizing type theories. This is because such theories
distinguish different levels of the language, such as terms, types, kinds, etc., and one
cannot apply a function at one level to compute a term at a higher level. Also, using
impredicative quantification ∀X : ? one level up leads to failure of normalization andhence logical consistency (Coquand, 1986).
4. Without large eliminations, it is not possible to prove basic negative facts aboutlambda-encoded data, like 0 6= 1 (Werner, 1992).
On the positive side, there is one powerful benefit of typed lambda-encodings, not available
with primitive datatypes:• Higher-order encodings – where datatypes contain embedded functions whose types
have negative occurrences of the datatype symbol – are permitted without violating

ZU064-05-FPR

paper

2

14 March 2017

20:59

Stump
normalization. With primitive datatypes as in Coq or Agda, negative occurrences ofthe datatype in the datatype definition very easily lead to failure of normalization.

Parigot solved the first problem with an alternative lambda encoding, which is typablein System F plus positive-recursive types, where accessors are computable in constanttime, as expected (Parigot, 1988). By Geuvers’s result, there is no alternative but to add
something to the core impredicative dependent type theory, to solve even just the problem
of induction (Geuvers, 2001). The present paper proposes two new type constructs for
this, called constructor-constrained recursive types and lifting. The former deepens earlier
work by Fu and Stump on System S, which solves the problem of induction using a typing
construct called self types, to allow the type to refer to the subject of the typing via boundvariable x in ιx.T (Fu & Stump, 2014). To prove consistency, they rely on a dependencyeliminating translation to System Fω plus positive-recursive types. This method is notapplicable to analyze a system with large eliminations, where dependence of types onterms is fundamental.
In the present paper, a deeper analysis of intrinsically inductive lambda encodings is undertaken, with a direct lattice-theoretic semantics which can account for large eliminations.
In the rest of this section, the two new features that enable intrinsically inductive lambdaencoding and large eliminations with lambda-encodings, respectively, are surveyed. Then
we turn to the definition (Sections 2 and 3) and analysis (Sections 5 and 6) of the new typetheory incorporating these features, called the Calculus of Dependent Lambda Eliminations(CDLE). This system is a type-assignment system, not suitable for implementation. An
algorithmic approach to CDLE, which has been implemented in a prototype tool called
Cedille, is then considered, together with examples (Sections 7 and 8). A comparison withrelated work is in Section 10. We begin by looking in a little more detail at the problems
with lambda encodings in pure type theory.
1.1 The problems, in more detail
Church’s encoding of natural numbers in untyped lambda calculus defines each numeral n
as follows (Church, 1941):
λ s.λ z. s · · · (s z)| {z }nWith this encoding, every function on the natural numbers is to be computed by iteration,and numbers are identified with iterators. Kleene found a clever way to compute the predecessor of Church-encoded n in this framework, but the operation requires O(n) reduction
steps, instead of the expected O(1). This limitation has been stressed many times in theliterature as a point against lambda-encodings. But Parigot solved this problem some timeago, with an encoding where data are represented not as iterators but as recursors (Parigot,
1988). Every call to the iterated function is presented with the predecessor number as wellas the result of iteration on that number. So 2 is encoded as λ s.λ z. s 1 (s 0 z). Whilein theory the space required for normal forms is exponential, in practice closure-based
implementations of lambda calculus compute efficiently with Parigot encodings, as has
been found in several studies (Stump & Fu, 2016; Koopman et al., 2014). And Parigot
encodings can be typed in a normalizing extension of System F with positive-recursive

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

3

types (cf. (Abel & Matthes, 2004; Mendler, 1988)). So efficiency of accessors is not a
problem for lambda encodings in total type theory, if one uses the Parigot encoding.
Let us consider then the problem of induction. Based on the Church encoding in untyped
lambda calculus, Fortune, Leivant, and O’Donnell proposed an encoding of natural number
n in the second-order lambda calculus (Fortune et al., 1983); i.e., System F (Girard et al.,1989):
ΛX.λ s : X → X.λ z : X. s · · · (s z)| {z }
n(Here we are writing ΛX for abstraction over types.) This idea was extended to a schematic
encoding for a class of inductive datatypes by Böhm and Berarducci (Böhm & Berarducci,
1985). An even more general encoding for inductive datatypes in the Calculus of Constructions (CC) was proposed by Pfenning and Paulin-Mohring (Pfenning & Paulin-Mohring,1989). The type for natural numbers in these typed encodings is
Nat = ∀X.(X → X) → X → X
The constructors Z (zero) and S (successor) are defined this way:ZS

= ΛX.λ s : X → X.λ z : X.z= λ n : Nat.ΛX.λ s : X → X.λ z : X.s (n X s z)

The definition of Nat above is second-order, but not dependent. So it is sufficient forcomputation – and indeed one can define the basic numeric functions using it – but it is notadequate for proofs. For example, one can define addition thus:
add = λ n : Nat.λ m : Nat.n Nat S m
And one might then wish to prove a theorem like commutativity of addition:∀n : Nat.∀m : Nat.Eq Nat (add n m) (add m n)
This is standardly proved by induction (with two subsidiary lemmas also proved by induction). Under the Curry-Howard correspondence widely used in constructive type theory,a proof of such a theorem is a closed term which inhabits that dependent type, using astandard representation of Leibniz equality Eq in type theory. So for induction, needed forproving such theorems, we are seeking an inhabitant of the type
∀P : Nat → ?.(∀n : Nat.P n → P (S n)) → P Z → ∀n : Nat.P n
Geuvers proved that this type cannot be inhabited in second-order dependent type theory,
for any choice of Nat : ?, S : Nat → Nat, and Z : Nat (Geuvers, 2001). This remarkable
result, proved by a model construction, would seem to close the door on lambda encodings
for inductive theorem proving. This is the first main problem.
Another way to see the difficulty is to consider how to extend the definition of Nat
Nat = ∀X.(X → X) → X → X
to a dependently typed version. So the goal is to define numbers not as their own iteration
principles, but rather as their own induction principles. We must go from a type X : ? to a
predicate P : Nat → ?. And instead of step and base case of iteration of type X → X and X

ZU064-05-FPR

paper

4

14 March 2017

20:59

Stump

respectively, we need step and base cases of induction. One could try out something likethe following:
Nat = ∀P : Nat → ?.(∀x : Nat.P x → P (Sx)) → P Z → P ?
There are several issues here. First, the definition needs to be recursive, if we are to define
Nat in terms of predicates P on Nat. Fortunately, the occurrence of Nat on the right-handside of this equation is positive, so we do not violate the positivity requirement needed topreserve normalization. But then we have some puzzles. The definition needs to refer to theconstructors S and Z for this datatype. But how could we hope to define those prior to thisdefinition, since they are operations on the type Nat? Even if somehow some simultaneous
definition were possible, we have the question of what to put for the question mark. An
intrinsically inductive natural number n must prove any given property P for n itself, given
proofs of the step and base cases. It is completely unclear a priori how one could set thisup. Indeed, Geuver’s result implies that there is no way to do this, without an extension to
the type theory. We will how this is solved with CDLE, in Section 1.2.
The second main problem is that of large eliminations, or computing types by recursion
on terms. In System F, with the usual definition of the Nat type, large eliminations are
impossible, since to compute anything recursively from n of type Nat, we must first instantiate the universally quantified type variable in the definiens of Nat, to the type which wewill compute by recursion on n. In order to compute a type, this instantiation should beby ?, since this is the type for types (and we are seeking to compute a type). But it is wellknown that positing that “type” is a type (i.e., ? : ?) leads to failure of normalization for the
language (see (Coquand, 1986), also (Meyer & Reinhold, 1986)).
So there is no way to compute a type by recursion on a Nat in System F; in other words,
large eliminations are not possible. This is bad enough, but there is another undesirable
consequence. The usual proof in type theory that constructors have disjoint ranges – so for
example, 0 6= 1 – relies on large eliminations. Leibniz equality states that equal expressions
satisfy the same predicates, and using large eliminations we can define a predicate P on
natural numbers n which is True if n is zero and False otherwise. Here, True can be taken as
any inhabited type, such as ∀X : ?.X → X; and False as any uninhabited one, like ∀X : ?.X.
If 0 equals 1, then P 0 implies P 1. Since P 0 is True and P 1 is False, we can inhabit False
from an assumption that 0 equals 1. Without large eliminations, this proof method fails,
and indeed as Werner argues, the erasure of the statement of Leibniz equality of 0 and 1 isjust ∀P.P → P, where one erases types of CC by dropping all term parts of types (Werner,
1992). So if we could inhabit (Eq Nat 0 1) → ∀X : ?.X in CC, we could also inhabit
True → False in System Fω (to which one erases CC terms and types); but this type is notinhabited. So not only does the proof method using large eliminations fail, the type 0 6= 1
simply cannot be inhabited, or else its erasure True → False would be, too (and the latter
is not).
Traditionally, the solution proposed to these problems has been to add primitive inductive types to type theory. One way is to follow the methodology of Martin-Löf, andalso Constable et al., and work with open type theories, where new inductive types can be
added as extensions of the theory (Martin-Löf, 1984; Constable et al., 1986). This approachhas been proposed also for impredicative type theory, by Coquand and Paulin (Coquand& Paulin, 1988). Alternatively, one can define a closed type theory with type and term

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

5

constructs for some class of inductive types. This is the approach of the Calculus ofInductive Constructions developed by Werner, which is the foundation of the Coq interactive theorem prover (The Coq development team, 2015; Werner, 1994). One can also findan interesting intermediate approach in the literature: in Pfenning and Paulin-Mohring’s
approach, inductive types are lambda-encoded but their induction principles and associatedreduction rules are added as extensions of the theory (Pfenning & Paulin-Mohring, 1989).
This paper proposes new solutions to the two main problems of induction and large
elimination for lambda-encoded data, in a closed type theory, without primitive inductive
types or primitive induction. Let us take a brief initial look at the two new typing constructs.
1.2 Constructor-constrained recursive types
To define intrinsically inductive lambda-encodings, we begin with the dependent intersection types of Kopylov (Kopylov, 2003). We will denote these types with prefix notation
ιx : T.T 0 instead of Kopylov’s x : T ∩ T 0 . Let S and Z be meta-level abbreviations for
λ n.λ s.λ z.s (n s z) and λ s.λ z.z, respectively. Also, we will make use of a top type U ,inhabited by all closed λ -abstractions. Now at the meta-level, define a sequence of types
by recursion on meta-level natural number k, with increasing support for dependent typing:
Nat0
Natk+1:= U:= ιn : Natk .∀P : Natk → ?.
(∀n : Natk .P n → P (S n)) → P Z → P n

Natk+1 denotes the subset of Natk for which induction holds, for predicates on Natk . We
use intersection types, because the natural proof that n is inductive may be identified, in a
type assignment system such as we will consider, with n itself. This striking observation isdue to Leivant (Leivant, 1983). We will see this in more detail below (Section 4).
Now the goal is to internalize the limit of this sequence of types as a single type N, using
a positive-recursive type. This is not possible with standard forms of recursive types, due
to type dependency. For suppose we tried to define N as
µ Nat : ?. ι n : Nat.
∀ P : Nat → ?. (∀ n : Nat. P n → P (S n)) → P Z → P n
To kind this type, we would have to kind (P Z), which requires showing that λ s.λ z.z canbe assigned type Nat. To do this, we would unfold the definition of Nat, and then before we
could add local variables s and z to the context, we would be forced again to kind (P Z),
since this would be the type for z. There is a circularity here, which System S avoided byusing an ad-hoc form of mutually recursive types (Fu & Stump, 2014).
Here, we handle the problem with a closer connection to the semantics for types wewill develop. We introduce the novel type form ν X :κ | Θ. T 0 , for what we call constructorconstrained recursive types. Here κ is a kind, and Θ is a set of typings that hold for U andare preserved by T 0 . We will define N to beν Nat : ? | S ∈ Nat → Nat, Z ∈ Nat.ι n : Nat.
∀ P : Nat → ?. (∀ n : Nat. P n → P (S n)) → P Z → P n
Semantically, this will be interpreted as the greatest lower bound of the decreasing sequence of meanings for Natk , defined above. The key new idea is to include this set ΘZU064-05-FPR

paper

6

14 March 2017

20:59

Stump

(here, S ∈ Nat → Nat, Z ∈ Nat) of typings which hold for U and are preserved as we
pass further into the sequence. This is so that we can kind the body of the ν-type. For
the semantic analysis, it will turn out to be critical for Θ to hold not just for the decreasing
sequence of meanings, but also for the greatest lower bound of that sequence. Without some
restriction, this appears not to be guaranteed. Here, we require that each typing constraint
in Θ must be of the form Πx1 : T1 . · · · Πxn : Tn . T , where the ν-bound variable occurs only
positively in T1 , . . . , Tn , and only at the head of T (i.e., T is either X or X applied to someX-free expressions). Nat → Nat meets this requirement, as a simple example, but so domore complex types.
CDLE’s type system has a rule for folding and unfolding ν-types. There is also a rule
for typing of constructors: Γ ` t : [N/X]T is derivable for all t ∈ T in the constructor set Θ,
once a ν-type N = ν X : κ | Θ. T 0 has been kinded in context Γ.

1.3 Lifting terms to the type level
The basic idea for supporting large eliminations with lambda encodings is to lift expressions explicitly from the term level of the language to the type level. While it iswell-known that one cannot lift the entire term language to the type level without losing
normalization (Coquand, 1986), there is no problem with lifting simply typed terms. For
example, the term λ s.λ z.s (s z) representing 2 in the Church encoding can be lifted to thetype level as λ s : κ → κ.λ z : κ.s (s z), for any particular kind κ (for example, ?, the kindwhich classifies types). Certainly the ability to do arithmetic with simply-typed lambda
encodings is limited (cf. (Leivant, 1991)). But typically for large eliminations, one seeks
just to do a single fold over the datatype to compute a type from the data. For example,
for statically typed printf, as proposed by Augustsson (Augustsson, 1998), one wishes
to compute the type of the rest of the arguments to printf from the format string. Thisrequires just a single fold.
CDLE introduces a novel construct ↑L t, representing the type obtained by lifting asimply-typed term t to the type level. The type L is a lifting type, which serves to constrain
the type of t to be simply typed, and also shows how that type should be lifted to a kind. For
example, to lift Church-encoded 2 to the type level, one writes ↑(∗→∗)→∗→∗ 2, where ∗ is aprimitive lifting type used to represent the kind ?. We are not lifting 2 at its polymorphic
type ∀X : ?.(X → X) → X → X, of course, as this type is not permitted at the kind level.
Instead, we are lifting an instantiation (X → X) → X → X of this type, where ∗ indicatesthe instantiation points.
One technical issue that must be addressed with this idea is the presence of variables
which occur free inside a lifting expression. For a simple example, suppose we have a freevariable x of type ∀ X : ? : X → X. , and consider this type, where x is being instantiated to∗:↑∗→∗ λ y.x y
It is tempting always to push lifting across λ -abstractions, but if we do that here, we willget:
λ y : ?.↑∗ (x y)ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

7

The body is not typable, because x (instantiated to have type ∗ → ∗) is being applied to a
type, namely y of type ?.
One can imagine several solutions to this problem. Here, we opt not to push lifting acrossa series of λ -abstractions unless the body is of the form x t¯, where x is bound in that series.
We will form type-level β -redexes for the arguments t¯, in case they are not headed by avariable in the series. So we will lift the successor λ s.λ z.s (n s z) of Church-encoded n to
λ s : ? → ?. λ z : ?. s ((↑(∗→∗)→(∗→∗) λ s.λ z.n s z) s z)
Despite this trick, we will still need some additional conversion principles for lifting, which
we will see below.
Note that in this paper, to avoid further technicalities, we only formalize lifting pure
simple types over ∗. The Cedille implementation, however, also supports the obvious
extension of this mechanism to simple types whose domain types are not lifting types,
like ∗ → Nat → ∗. This example lifts to the kind ? → Nat → ?.

2 Syntax
Figure 1 gives the syntax of CDLE. We are separating clauses of the grammars with ||, toavoid confusion with the single vertical bar in the syntax for ν-types. We use ∀ consistently
in the types for functions for which no argument is explicitly given when the function iscalled. So these are implicit products, as introduced by Miquel (Miquel, 2001). Π is used
for explicit products, where an argument is required when applied. We do not use kind-level
implicit products, so the bound variable in any type-level λ -abstraction must be annotated.
The type U is a universal type, inhabited by all closed λ -abstractions. In the construct
νX : κ | Θ.T , the scope of bound variable X is Θ and the body T . We are using ν instead ofµ, because our semantics will make νX : κ | Θ.T the greatest fixed-point of T . Nevertheless,we will focus here on using this type for inductive datatypes, not coinductive ones (which
are outside the scope of this paper). Several rules related to ν-types will make use of anotation Uκ for a top type at kind κ. We define this by recursion on κ:U?
UΠ x:T. κUΠ X:κ. κ 0= U= λ x : T. Uκ
= λ X : κ. Uκ 0

We usually elide the final “, ·” from constructor sets Θ and typing contexts Γ. We use
other standard notations for typed lambda calculus, in particular T → T 0 for Π x : T. T 0
when x is not free in T 0 . The type ι x : T. T 0 is a dependent intersection type, as introduced
by Kopylov (Kopylov, 2003). We use t ∈ T to denote a constraint that term t has type T ,as opposed to a declaration of a variable x to have type T (written x : T ). Here we see one
unusual feature of the type system, which is that the context may contain hypotheses thata term has a given type (t ∈ T ). This feature comes in with the constructor-constrained
recursive types ν X : κ | Θ. T . We will see how to avoid it when we turn to the Cedille
implementation of CDLE (Section 7). We implicitly assume that Γ does not declare any
variable x or X twice, and that bound variables are renamed to enforce this. If the set Θ isempty, we may write ν X : κ. T instead of ν X : κ | Θ. T .

ZU064-05-FPR

paper

14 March 2017

20:59

8

Stump
variables x, X
terms tkinds κtypes T

::=
::=
::=

lifting types L
constructor sets Θ
typing contexts Γ

::=
::=
::=

x || λ x.t || t t 0? || Π x : T. κ || Π X : κ. κ 0
X || Π x : T. T 0 || ∀ X : κ. T || ∀ x : T. T 0 ||
ι x : T. T 0 || ν X : κ | Θ. T 0 || λ x : T. T 0 ||λ X : κ. T || T t || T T 0 || U || ↑L t
∗ || L → L0
· || t ∈ T, Θ
· || Γ, X : κ || Γ, t : T || Γ, t ∈ T

Fig. 1. Syntax of CDLE, and typing contexts

FV(λ x.t) ⊆ decl(Γ)Γ ` λ x.t : U(x : T ) ∈ ΓΓ`x:TΓ ` t : T0 Γ ` T0 .T
Γ`t :TΓ ` t0 : TΓ ` λ x.t : Π x : T. T 0Γ ` t : Π x : T1 . T2 Γ ` t 0 : T1
Γ ` t t 0 : [t 0 /x]T2(t ∈ T ) ∈ ΓΓ`t :TΓ ` κ :  Γ, X : κ ` t : TΓ ` t : ∀ X : κ. T

Γ ` t : ∀ X : κ. T Γ ` T 0 : κΓ ` t : [T 0 /X]TΓ ` t : ι x : T. T 0Γ ` t : [t/x]T 0Γ ` t : ∀ x : T1 . T2 Γ ` t 0 : T1
Γ ` t : [t 0 /x]T2

Γ ` t : ι x : T. T 0
Γ`t :TΓ`t :T Γ`ΘΓ ` t ∈ T, ΘΓ`·Γ ` t : T0

Γ`T :?

Γ`T :?

Γ ` T .T0
Γ`t :TΓ`T :?

Γ, x : T ` (λ x.t) x : T 0

Γ, x : T ` t : T 0

x 6∈ FV(t)Γ ` t : ∀ x : T. T 0
Γ`t :TΓ ` t : [t/x]T 0Γ ` t : ι x : T. T 0
N = ν X : κ | Θ1 ,t ∈ T, Θ2 . T 0Γ ` t : [N/X]Tt =β t 0

Γ`t :TΓ`N:κ

Fig. 2. Typing of terms and constructor sets

3 Type Assignment
We consider now the type assignment rules for CDLE. These include a number of featuresthat would make them unsuitable for direct use in a practical implementation. By acceptingsome nonalgorithmic features, we can more easily establish, in CDLE, a firm theoreticalfoundation for the practical implementation of dependent typing based on pure lambda
encodings. We will see how this works out when we turn to the Cedille implementation(Section 7).
The typing rules for terms and constructor sets are in Figure 2. We also use kinding rules
for types, in Figure 3. Figure 4 gives kinding rules for constructor sets, and superkinding
rules. (Note that the  in the superkinding judgment is considered part of the syntax ofthe judgment, not a separate form of expression.) Figure 6 defines judgements imposing
the restriction mentioned above on the form of types in constructor sets Θ. To express ourpositivity requirement for kinding ν-types, we use a judgment X ∈ p T for p ∈ {+, −}. The

ZU064-05-FPR

paper

14 March 2017

20:59

9

Journal of Functional ProgrammingΓ ` T1 : ? Γ, x : T1 ` T2 : ?
Γ ` ∀ x : T1 . T2 : ?

Γ ` κ :  Γ, X : κ ` T : ?
Γ ` ∀ X : κ. T : ?

Γ ` T1 : ? Γ, x : T1 ` T2 : ?
Γ ` Π x : T1 . T2 : ?

Γ ` T : ? Γ, x : T ` T 0 : ?
Γ ` ι x : T. T 0 : ?

Γ ` T : ? Γ, x : T ` T 0 : κΓ ` λ x : T. T 0 : Π x : T. κΓ ` κ :  Γ, X : κ ` T 0 : κ 0
Γ ` λ X : κ. T 0 : Π X : κ. κ 0

Γ ` T : Π x : T 0. κ Γ ` t : T 0
Γ ` T t : [t/x]κ

Γ ` T : Π X : κ. κ 0 Γ ` T 0 : κΓ ` T T 0 : [T 0 /X]κ 0(X : κ) ∈ ΓΓ`X :κ

Γ`U :?

Γ, X : ? ` t : |L|XΓ ` ↑L t : lift(L)X ∈+ TΓ`κ :
Γ ` [Uκ /X]ΘΓ, X : κ ` Θ : ?
Γ, X : κ, Θ ` T : κ

CtorsX ΘΓ, X : κ, Θ ` [T /X]ΘΓ ` ν X : κ | Θ. T : κ

Fig. 3. Kinding of typesΓ`·:?

Γ`T :? Γ`Θ:?
Γ ` (t ∈ T, Θ) : ?

Γ ` T : ? Γ, x : T ` κ : Γ ` Π x : T. κ : Γ ` κ :  Γ, X : κ ` κ 0 : Γ ` Π X : κ. κ 0 : Γ`?:Fig. 4. Kinding of constructor sets, and superkindingN = ν X : κ | Θ. T
Γ ` N . [N/X]TΓ ` (λ x : T. T 0 ) t . [t/x]T 0Γ`t :Tt ∗ t0Γ ` T t . T t0

X 6∈ FV(T 0 )Γ ` ∀ X : T. T 0 . T 0x̄ 6∈ FV(t) |L̄| = |x̄|Γ ` ↑L̄→L0 λ x̄.(t x̄) . ↑L̄→L0 t

Γ ` (λ X : κ. T ) T 0 . [T 0 /X]T
liftL,0/ (t) = TΓ ` ↑L (t) . T|L̄| = |x̄| = |T̄ |Γ ` (↑L̄→L0 →L λ x̄.t) T̄ ((↑L̄→L0 t 0 ) T̄ ) . ↑L̄→L (λ x̄.(t (t 0 x̄))) T̄

Fig. 5. Computation rules for conversion
CtorTpX T CtorsX Θ t 6∈ terms(Θ)
CtorsX (t ∈ T, Θ)

CtorsX ·X ∈+ T1 CtorTpX T2
CtorTpX Π x : T1 . T2

HeadOnlyX T
CtorTpX T

HeadOnlyX X

X 6∈ FV(T )HeadOnlyX T

HeadOnlyX T
HeadOnlyX (T t)

HeadOnlyX T

X 6∈ FV(T 0 )HeadOnlyX (T T 0 )Fig. 6. Definition of helper judgements for constructor sets

ZU064-05-FPR

paper

14 March 2017

20:59

10

Stump
lift(∗)
lift(L → L0 )==?
lift(L) → lift(L0 )| ∗ |X|S → S0 |X==

X|S|X → |S0 |X

liftL1 →L2 ,v (λ x.t)
liftL,v (x t¯)==

λ x : lift(L1 ). liftL2 ,(v,(x7→L1 )) (t)x liftargsL0 ,v (t¯), if (x 7→ L0 ) ∈ v

liftargsL1 →L2 ,v (t , t¯)
liftargsL,v (·)==((↑v→L1 λ v.t) v) , liftargsL2 ,v (t¯)·

Fig. 7. Meta-level functions related to lifting

definition is unsurprising, so we omit it. Note, however, that a more flexible approach is
proposed in (Abel & Matthes, 2004), using kind-level variance annotations. Adding theseto CDLE should be straightforward future work. We also write FV(T ) for the set of freevariables (term and type) in T , and decl(Γ) for the set of variables (term and type) declaredin Γ via x : T or X : κ. We write terms(Θ) for the set of terms t with constraint t ∈ T listedin Θ for some T .
Our system has a direct-computation typing rule, as in Nuprl (Constable et al., 1986).
This rule uses a relation =β , which is just standard β -equivalence of pure untyped lambda
calculus. Direct computation allows us to use a more general typing rule for λ -abstractions:in the premise, we apply the λ -abstraction, rather than typing its body. Note that the rulealso implies type preservation under β -reduction; the soundness of this will be establishedwith our semantics. CDLE has forward and backward conversion rules for typing, using a
directed conversion relation .. The computation rules (central axioms) for . are given in
Figure 5. Additional rules including transitivity, reflexivity, and rules making the relationa congruence are straightforward, and omitted for space reasons. Note that the congruence rules augment the context when relating the bodies of abstractions. Using a directed(nonsymmetric) relation just means that it may be necessary to perform a sequence of
forward and backward conversions; the key point is that the backward conversions require
an additional kinding derivation. One could also consider a conversion rule for kinding,but simple situations that would require this can be solved by type-level η-expansion,and including kind-level conversion complicates inversion on kinding. So to avoid such
distractions this is omitted from CDLE. We will consider the nature of CDLE conversion
further in Section 5.1 below. Several of the rules deal with lifting. We will see more about
how they work below (Section 9.2).
The kinding rule for types ↑L t (in Figure 3), uses a meta-level function lift(−), definedin Figure 7, which maps lifting types to kinds as follows. The idea is to lift a type like ∗ → ∗to the kind ? → ?. We could also allow a lifting type Π x : T. L to enable lifting the bodies
of abstractions without lifting the classifier for the bound variable, for quantifications overterms. We omit this here for simplicity, and because it is not required for our examples.
We cannot lift implicit products, because CDLE does not have these at the type level, andadding them introduces semantic complications. We also use a meta-level function |L|X ,also defined in Figure 7, to turn a lifting type into a type, replacing ∗ with X.

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

11

Figure 7 defines a third function lift−,− (−), which attempts to lift a term to a type (butmay be undefined). We use vector notation t¯ for a possibly empty sequence t1 , . . . ,tn ofterms, where · denotes the empty sequence. We write |t¯| for the length of the sequence.
The notation x t¯ means that x is applied in a left-nested fashion to the terms t¯. This
lift−,− (−) function attempts to push the lifting operator (↑) down into a λ -abstraction.
Roughly speaking, it tries to turn ↑ (λ x̄. xi t¯) into λ x̄ : κ̄. xi T̄ 0 , where the kinds κ̄ arederived from the lifting type given as the first argument to lift−,− (−), and the types T̄ 0 are
new lifting types derived from the arguments t¯
In describing these syntactic operations, we use some special notational conventions inFigure 7 with the meta-variable v, which ranges over sequences of bindings x 7→ L (where
L is a lifting type). In the first equation for the liftargs−,− (−) helper function, we write λ v.t
to mean that all the variables listed in t should be λ -bound around t, in the order they appear
in v. Also, we write v → L to mean that the lifting types in v should be added as domain
types, in order, for an arrow type around L. And we write t v to mean that the variables
in v should be given as arguments, in order, for an application of t. These notations areused to implement the idea discussed in Section 1.3, of creating type-level β -redexes whenpushing lifting to arguments.

4 Church-encoded natural numbers
As discussed in Section 1.2, we use the following definition for the type N of the natural
numbers, where S and Z are meta-level abbreviations for λ n.λ s.λ z.s (n s z) and λ s.λ z.z:
ν Nat : ? | S ∈ Nat → Nat, Z ∈ Nat.
ι n : Nat. ∀ P : Nat → ?.
(∀ n : Nat. P n → P (S n)) → P Z → P n
These are Church-encoded numbers, because the type for the input s for successor,
namely ∀ n:Nat. P n → P (S n), uses an implicit product (∀). For the Parigot encoding, one
just changes this to an explicit product (Π). We will mostly focus on the Church encodingin this paper, since it is somewhat simpler and more familiar than the asymptotically moretime-efficient Parigot encoding.
Let us see now in detail how to kind this type, using the ν-kinding rule:
X ∈+ TΓ`κ :
Γ ` [Uκ /X]ΘCtorsX ΘΓ, X : κ ` Θ : ?
Γ, X : κ, Θ ` [T /X]Θ Γ, X : κ, Θ ` T : κΓ ` ν X : κ | Θ. T : κ

The first premise is obvious, though note that Nat occurs positively but not strictly positively; the occurrences in the body of the type are in the domain parts of an even number of
abstractions. The second premise is trivial. For the third premise, we can confirm easily thatthe constructor set for this example satisfies CtorsNat , as required. For the fourth premise:with Nat : ? in the context, we can kind the constructor set S ∈ Nat → Nat, Z ∈ Nat. For theZU064-05-FPR

paper

14 March 2017

20:59

12

Stump

fifth, we can assign U → U to S, using our direct-computation rule:Γ, n : U ` λ s.λ z.s (n s z) : U

S n =β λ s.λ z.s (n s z)

Γ, n : U ` S n : U
Γ`S:U →U
We can also assign U to Z.
For the sixth premise, we must show that our constructor set is preserved by the body ofthe ν-type. So in the context (call it Γ) Nat : ?, S ∈ Nat → Nat, Z ∈ Nat, we must show thefollowing typings, where we write NAT to abbreviate the body of the ν-type:• Γ ` S : NAT → NAT• Γ ` Z : NAT
Let us just consider the second (the first also holds). Expanding NAT, we see we must showΓ ` Z : ι n : Nat. ∀ P : Nat → ?.
(∀ n : Nat. P n → P (λ s.λ z.s (n s z))) →P (λ s.λ z.z) → P n
From our constraints in Γ, we have that Γ ` Z : Nat. So we can assign the first type in thedependent intersection. It remains to assign the second type, where n is instantiated with
Z. For this, we can apply some introduction rules (together with direct computation) to
reduce the problem to the following typing, where types like P Z are kindable, from theconstraints in Γ:Γ, P : Nat → ?, s : ∀n : Nat.P n → P (S n), z : P Z ` z : P Z
This holds by the variable typing rule.
For the seventh premise, we must be able to assign kind ? to the body of the ν-type,assuming Nat : ? and the constructor set have been added to the context. The interestingobservation for this is that the applications of P can be kinded. For example, to kind P (S n),
we use the constraint S ∈ Nat → Nat to assign type Nat to S n.
If we have a term of type N, then by unfolding the ν-type and then taking the second
projection of the dependent intersection, we can use that term for dependently typed iterations; for example, inductive proofs. Of course, we can also use it for simply typed
iterations as a special case, so we can implement basic terminating functions like addition,
multiplication, predecessor, and so forth, in the usual way for Church-encoded numbers.
We will see this more in our Cedille implementation below (Section 8).
4.1 A note on equality types
It may be of interest to some readers to know that CDLE validates axiom K for equality
types (Hofmann & Streicher, 1998). K, which is equivalent to uniqueness of identity proofs,
is all one must add to Martin-Löf Type Theory (MLTT) to support dependent patternmatching, and thus is desirable for practical programming with dependent types (Goguen
et al., 2006). But K is incompatible with Homotopy Type Theory (HoTT) (UnivalentFoundations Program, 2013), where distinguishing proofs of the same equality is essential
to the approach. So CDLE is not appropriate, without significant modification, for HoTT.

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming
JK

=

:=

13

λ A : ?. λ a : A. νE : A → ? | λ x.x ∈ E a. λ b : A.
(ιu : E b. ∀P : ∀b : A.E b → ?. (P a λ x.x) → P b u)
∧ (ιu : E a. ∀P : E a → ?. (P λ x.x) → P u))

Fig. 8. Equality type satisfying axioms J and K both

In more detail: CDLE allows one to define an equality type with both J- and K-styleelimination. The definition is in Figure 8, where we are writing T ∧ T 0 for ιx : T. T 0 whenJK
x 6∈ FV(T 0 ). Note that here, the top type UA→? that is used when kinding = is defined (atthe meta-level) to be λ x : A.U . So we indeed have λ x.x in UA→? a, when checking thatthe constructor set is satisfied by the top type. We can easily prove, using similar reasoning
JK
as in Section 4 above, that λ x.x has type ∀A : ?.∀a : A. a = A a.
Any relation purported to be an equality relation in type theory should be substitutive,
JK
and indeed, given t of type a = A b, we may use the first part of its conjunctive type totransform any type containing a into one containing b, as expected. And, as expected for
JK
axiom J, to prove something about such a term t as a proof of a = A b, it suffices to reason
JK
just about λ x.x as a proof of a = A a. But we also have the second conjunct of the type
JK
JK
a = A b, which allows us to prove any property of u of type a = A a by proving it for λ x.xof that type. This is axiom K.
5 Semantics of Types
To define a semantics for types, we need a few preliminary definitions. We will work with
set-theoretic partial functions for the semantics of higher-kinded types. An application ofsuch a function is undefined if the argument is not in the domain of the partial function.
(As standard in set theory, such functions are themselves sets.) We consider any meta-level
expressions, including formulas, which contain undefined subexpressions to be undefinedthemselves. In lemmas and theorems, if we affirm formulas involving possibly undefined
expressions, we are implicitly affirming all those expressions are defined. We write A → B
for the set of meta-level total functions from set A to set B; that is, total functional subsets
of A × B. We write (x ∈ A 7→ b) for the (meta-level) function mapping input x in the set A
to b.
For our semantics, we prove results about closed terms only, though for the semantics ofthe lifting operation we will have to consider open terms. Let L be the set of closed lambda
abstractions (i.e., terms of the form λ x.t with no free variables), and let N ⊆ L be the setof closed normal-form terms. We will write for (full) β -reduction. We also write =cβ forstandard β -equivalence restricted to closed terms, and [t]cβ for the set {t 0 | t =cβ t 0 }. The
latter operation is extended to sets S of terms by writing [S]cβ for {[t]cβ | t ∈ S}. In a few
places we write nf(t) for the (unique) normal form of term t; this is undefined if t has nonormal form. We write Ω for an arbitrary term without normal form, like (λ x.x x) (λ x.x x).
Definition 1 (Reducibility candidates)
R := {[S]cβ | S ⊆ L }.
A reducibility candidate (element of R) is a set of β -equivalence classes of λ -abstractions.
We will use this definition to develop as technically light a semantics as possible, while

ZU064-05-FPR

paper

14 March 2017

20:59

14

Stump

still being sufficient to show logical consistency (Corollary 14 below). Further adaptation
would be necessary to show normalization, but this is not needed for our consistency proof.
One exception is that we will need to reason about normalization for proving soundness oflifting. Throughout the development we will make use of a choice function ζ . Given any
set E of terms, ζ returns a λ -abstraction if E contains one, and is undefined otherwise.
Lemma 2
If E = [λ x.t]cβ , then [ζ (E)]cβ = E
Lemma 3 (R is a complete lattice)
The set R ordered by subset forms a complete lattice, with greatest element [L ]cβ andgreatest lower bound of a nonempty set of elements given by intersection.
Lemma 4[N ]cβ ∈ R, and 0/ ∈ R.
Figure 9 defines our semantics for types and kinds, by mutual structural recursion. The
semantic functions take arguments σ and ρ, in addition to the type or kind to interpret.
We require that σ maps term variables to terms, and ρ maps type variables to sets. Theinterpretations of types and kinds are then also sets. We will get more precise descriptionsof the domains and codomains of the semantic functions later. The interpretation of νtypes uses the notation F n (a) for (meta-level) iteration of the function F n times on a:
F(F(. . . F(a))). The operation ∩κ,σ ,ρ used in the semantics of ν-types, and the value>?,σ ,ρ used in the semantics of U , are defined in Figure 10. The meaning of a type can be
empty, and so in interpreting ∀ x:T. T 0 we must take the intersection using ∩? , which returns
the top element of R if the interpretation of T is empty. The meaning of a kind cannot be
empty, however, so we do not need to worry about this situation when interpreting ∀ X :κ. T .
For the semantics of Πx : T.κ, if JT Kσ ,ρ 6∈ R, then the meaning of the Π-kind is undefined.
An important principle in the definition of this semantics is that if the meaning of a typeis defined, then it satisfies the semantic counterparts of the conversion rules in Figure 5. Soloosely, if T . T 0 and JT K is defined, then JT K = JT 0 K just based on the definition of JT K
(not any auxiliary information). This greatly simplifies the semantic connection between
conversion and typing for the proof of semantic soundness (Theorem 13 below).
Figure 11 defines a semantic lifting function to lift terms to semantic functions at the(set-theoretic) level where they are in the interpretations of kinds. We do not need to carrythe valuations σ and ρ through the definition, since we have restricted lifting types to be
simple types over ∗. A different kind of valuation θ is used, which maps term variables topairs (L, S) where L is a lifting type and S is a set. If we included types Πx : T.L as lifting
types, then we would need to make use of σ and ρ in the definitions in Figure 11.
5.1 About the conversion relation
Most type theories are defined using a congruence relation on types which is then shown
to be algorithmic by proving its confluence and normalization. For CDLE – and, it seems
likely, any system combining dependent and recursive types – the situation is somewhat
more complicated, as indicated by the following theorem:
Theorem 5

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

JXKσ ,ρ
JU Kσ ,ρJΠx : T1 .T2 Kσ ,ρ===J∀X : κ.T Kσ ,ρJ∀x : T.T 0 Kσ ,ρJιx : T.T 0 Kσ ,ρ
Jλ X : κ.T Kσ ,ρ
Jλ x : T.T 0 Kσ ,ρ
JT T 0 Kσ ,ρ
JT tKσ ,ρJνX : κ | Θ.T Kσ ,ρ

=
=
=
=
=
=
=
=

J↑L (t)Kσ ,ρ
J?Kσ ,ρ
JΠx : T.κKσ ,ρ===JΠx : κ.κ 0 Kσ ,ρ

=

ρ(X)
>?
[{λ x.t | ∀E ∈ JT1 Kσ ,ρ .
[[ζ (E)/x]t]cβ ∈ JT2 Kσ [x7→ζ (E)],ρ }]cβ∩{JT Kσ ,ρ[X7→S] | S ∈ JκKσ ,ρ }∩? {JT 0 Kσ [x7→ζ (E)],ρ | E ∈ JT Kσ ,ρ }{E ∈ JT Kσ ,ρ | E ∈ JT 0 Kσ [x7→ζ (E)],ρ }(S ∈ JκKσ ,ρ 7→ JT Kσ ,ρ[X7→S] )(E ∈ JT Kσ ,ρ 7→ JT 0 Kσ [x7→ζ (E)],ρ )JT Kσ ,ρ (JT 0 Kσ ,ρ )JT Kσ ,ρ ([(σt)]cβ )q, whereq = ∩κ,σ ,ρ {F n (>κ,σ ,ρ ) | n ∈ N} and
F = (S ∈ JκKσ ,ρ 7→ JT Kσ ,ρ[X7→S] )};if F(q) = q
hhnf(t)ii0L/R(E ∈ JT Kσ ,ρ → JκKσ [x7→ζ (E)],ρ ),if JT Kσ ,ρ ∈ R(S ∈ JκKσ ,ρ → JκKσ ,ρ[X7→S] )Fig. 9. Semantics for types and kinds (see also Figures 10 and 11)
X ⊆∗,σ ,ρ Y
X ⊆Πx:T.κ,σ ,ρ Y⇔⇔

X ⊆ΠX:κ.κ 0 Y⇔>?
>?,σ ,ρ
>Πx:T.κ,σ ,ρ>ΠX:κ.κ 0 ,σ ,ρ

=
=
=
=

X ⊆Y
∀E ∈ JT Kσ ,ρ .
X(E) ⊆κ,σ [x7→ζ (E)],ρ Y (E)∀S ∈ JκKσ ,ρ .
X(S) ⊆κ 0 ,σ ,ρ[X7→S] Y (S)[L ]cβ>?
(E ∈ JT Kσ ,ρ 7→ >κ,σ [x7→ζ (E)],ρ )(S ∈ JκKσ ,ρ 7→ >κ 0 ,σ ,ρ[X7→S] )


∩? X

=

∩?,σ ,ρ X=∩Πx:T.κ,σ ,ρ X=

∩ΠX:κ.κ 0 ,σ ,ρ X=

∩X, if X 6= 0/>? , otherwise∩X?
(E ∈ JT Kσ ,ρ 7→ ∩κ,σ [x7→ζ (E)],ρ {F(E) | F ∈ X}),if
X 6= 0/>Πx:T.κ,σ,ρ , otherwise

(S
∈
JκK

σ
,ρ 7→

 ∩
κ 0 ,σ ,ρ[X7→S] {F(S) | F ∈ X}),
if X 6= 0/>Πx:κ.κ 0 ,σ ,ρ , otherwise

Fig. 10. Pointwise-extended lattice operations

15

ZU064-05-FPR

paper

14 March 2017

20:59

16

Stump
hhλ x.tiiθL→L
hhx t¯iiLθ

0

=
=

0

L
S ∈ Jlift(L)K0,/ 0/ 7→ hhtiiθ [x7→(S,L)]S (hht1 iiLθ1 ) · · · (hhtn iiLθn ),if θ (x) = (S, L̄ → L) with |L̄| = n = |t¯|

Fig. 11. Semantic lifting hh ii

There is no recursively enumerable convertibility relation between types in context which
is sound and complete with respect to equality of interpretations.
Proof
We can reduce extensional equivalence of primitive recursive numeric functions to thisproblem. That relation is not r. e., since if it were, it would be decidable (inequivalence
is obviously r.e.), and it is known not to be so. Suppose f and g have type N → N, andconsider the following two types, where S denotes successor for Church-encoded numerals
as above:∀ P : N → ?. ν X : N → ?. λ n : N. P ( f n) → X(S n)∀ P : N → ?. ν X : N → ?. λ n : N. P (g n) → X(S n)These types have the same interpretation (with empty functions for σ and ρ) iff f and g
return the same values for all inputs n : N.
So CDLE must be defined using a particular incomplete conversion relation. Further useof the theory will be required to see if further (semantically justified) principles need to be
added for practical use. Additional analysis of this relation, such as studying decidability
or complete formulations for subrelations, must remain to future work.
5.2 Reasoning about lifting
To prove soundness of the conversion and kinding rules for lift types ↑L t, we need some
intricate and interesting reasoning, summarized in the following lemmas. Several of thesecan be viewed as semantic lemmas about simple typing. To justify the main conversion
axiom about lifting, we have this lemma:
Lemma 6
Suppose liftL,v (t) is defined, and suppose that θ (x) = (S, L) holds for some S ∈ Jlift(L)K0,/ 0/
iff v(x) = L. Suppose also that nf(t) is defined, and FV(t) ⊆ dom(θ ). Then hhtiiL0,/ 0,θ
/ =
0
0
0
JliftL,v (t)K0,ρ
/ 0 , where ρ (x) = S iff θ (x) = (S, L ) for some L .
The main lemma needed to justify kinding of lift types is the following, where we first
introduce a definition relating valuations θ used in semantic lifting (Figure 11) and thevaluations σ mapping term variables to terms.
Definition 7 ((θ , R)-constrained)
Suppose θ is a given valuation of the sort used in Figure 11, and R ∈ R is also given.
Then σ is called (θ , R)-constrained iff the following holds: σ (x) ∈ J|L|X K0,[X7/ →R] iff θ (x) =(S, L).
Lemma 8 (Main Lifting Lemma)

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

17

Let t be a possibly open term in normal form, and assume a valuation θ with dom(θ ) ⊇FV(t), and such that for all x ∈ dom(θ ), θ (x) = (S, L) iff S ∈ Jlift(L)K0,/ 0/ . Also, makethe following main assumption about t and L: for all nonempty R ∈ R, for all (θ , R)L
constrained σ , we have [σt]cβ ∈ J|L|X K0,[X7/ 0/ .
/ →R] . Then hhtiiθ ∈ Jlift(L)K0,
This main lemma uses what turns out to be a powerful semantic idea: since the kinding
rule for ↑L t has premise Γ, X : ? ` t : |L|X , we know that we have σt ∈ J|L|X K0,[X7/ →R] , for any
R ∈ R. This additional quantification over R is crucial for getting the proof to go through,and leads to other interesting consequences. First, we get normalization, because we caninstantiate R with [N ]cβ (the set of closed normalizing terms):
Lemma 9Suppose that for all R ∈ R, we have [t]cβ ∈ J|L|X K0,[X7/ →R] . Then t is normalizing.
Next we have to note two lemmas, easily proved by induction on the lifting type L inquestion.
Lemma 10Let ρ = [X 7→ R], where R ∈ R is nonempty. Then J|L|X K0,ρ/ is nonempty.
Lemma 11
Suppose [t1 ]cβ 6∈ J|L1 |X K0,ρ/ where ρ = [X 7→ R] for some nonempty R ∈ R. Then for any
L2 there exists a term of the form λ y.t2 such that [λ y.t2 ]cβ ∈ J|L1 → L2 |K0,ρ
/ but [[t1 /y]t2 ] 6∈
J|L2 |K0,ρ
/ .
With these, we can derive the following strong property about inclusion of interpretations, which is needed for Lemma 8. The proof is interesting enough that it is given here in
full.
Lemma 12 (Trivial semantic subtyping for simple types)
00
Suppose that for all nonempty R ∈ R, J|L|X K0,[X7/ →R] ⊆ J|L |X K0,[X7/ →R] . Then L = L .
Proof
The proof is by induction on the structure of L0 , considering several cases. We will referto the assumption of the theorem as our semantic subtyping assumption. Let L̄ and L̄0 be
sequences of lifting types with |L̄| = |L̄0 | = n, for some n.
Case: Suppose L is L̄ → ∗ and L0 is L̄0 → La → Lb for some La and Lb . Then we can easily
violate our semantic subtyping by instantiating R with [N ]cβ and taking [λ x̄.λ y.Ω]cβ as0an element in J|L|X K0,[X7/ →[N ]cβ ] but not in J|L |X K0,[X7/ →[N ]cβ ] .

Case: Suppose L is L̄ → L̄00 → ?, for some nonempty L̄00 , and L0 is L̄0 → ?. Instantiate R
in our semantic subtyping assumption with {[λ x.x]cβ }. Now we will have λ x̄.λ x̄00 .λ x.x ∈00
000
J|L̄0 → L̄00 → ?|X K0,[X7/ →{[λ x.x]cβ }] , where |x̄ | = |L̄ |. But this term is not in J|L̄ → ?|X K0,[X7/ →{[λ x.x]cβ }](using the fact that the quantifications imposed by the semantics of function types are notvacuous, by Lemma 10).
Case: So we are left with the case where L is L̄ → ? and L0 is L̄0 → ? (and |L̄| = |L̄0 |).
Suppose some Li differs from Li0 , and suppose that i is the greatest position at which thisoccurs. Now let La be Li+1 → · · · → Ln → ?. We can prove that Li0 must be a semantic
subtype of Li , by the following argument. Assume this is not the case. Then there is

ZU064-05-FPR

paper

14 March 2017

20:59

18

Stump
(σ ] [x 7→ t], ρ) ∈ JΓ, x : T K(σ , ρ ] [X 7→ S]) ∈ JΓ, X : κK(σ , ρ) ∈ JΓ,t ∈ T K(0,/ 0)/ ∈ J·K⇔⇔⇔(σ , ρ) ∈ JΓK ∧ JT Kσ ,ρ ∈ R ∧ [t]cβ ∈ JT Kσ ,ρ
(σ , ρ) ∈ JΓK ∧ S ∈ JκKσ ,ρ
(σ , ρ) ∈ JΓK ∧ JT Kσ ,ρ ∈ R ∧ [σt]cβ ∈ JT Kσ ,ρ

Fig. 12. Semantics of typing contexts ΓJκ |X ΘKσ ,ρ
J·Kσ ,ρ
Jt ∈ T, ΘKσ ,ρ={S ∈ JκKσ ,ρ | JΘKσ ,ρ[X7→S] }⇔JT Kσ ,ρ ∈ R ∧ [σt]cβ ∈ JT Kσ ,ρ ∧ JΘKσ ,ρ

Fig. 13. Definition of Jκ |X ΘKσ ,ρ , and semantics of constructor sets Θsome nonempty R ∈ R such that E ∈ J|Li0 |X K0,[X7/ →R] but E 6∈ J|Li |X K0,[X7/ →R] . But then by0
Lemma 11 there is a term λ y.t 0 such that [λ y.t 0 ]cβ ∈ J|Li → La |K0,[X7/ →R] but [[ζ (E)/y]t ]cβ 6∈00J|La |X K0,[X7/ →R] . Consider the term λ x̄.λ y.t . We have [λ x̄.λ y.t ]cβ in J|L̄ → ?|K0,[X7/ →R] , by asimple application of the semantics of function types. But we do not have [λ x̄.λ y.t 0 ]cβ ∈J|L̄0 → ?|K0,[X7/ →R] . This follows (using also Lemma 10 to instantiate the variables x̄) because
00E ∈ J|Li0 |X K0,[X7/ →R] , but we deduced [[ζ (E)/y]t ]cβ 6∈ J|La |X K0,[X7/ →R] . So we have Li as a0semantic subtype of Li , and we may then apply the IH to conclude that Li = Li . This
contradicts the assumption we made that those types are different.
6 Soundness for Typing
Figure 12 defines a semantics for typing contexts, for purposes of the following main
theorem. In that definition, we write σ ] [x 7→ t] to mean σ [x 7→ t] where x 6∈ dom(σ ) (andsimilarly for ρ ] [X 7→ S]). Figure 13 defines Jκ |X ΘKσ ,ρ to be the set of those elementsof JκKσ ,ρ which satisfy the constraints given by Θ for type variable X. These two helper
notions are used in stating the main theorem below.
Theorem 13 (Soundness of typing and kinding)If (σ , ρ) ∈ JΓK, then
1. If Γ ` κ : , then JκKσ ,ρ is defined.
2. If Γ ` T : κ, then JT Kσ ,ρ ∈ JκKσ ,ρ .
3. If Γ ` t : T , then [σt]cβ ∈ JT Kσ ,ρ and JT Kσ ,ρ ∈ R.
4. If Γ ` Θ : ? and Θ = t1 ∈ T1 , . . . ,tn ∈ Tn , then JT1 Kσ ,ρ ∈ R, . . . , JTn Kσ ,ρ ∈ R.
5. If Γ ` Θ, then JΘKσ ,ρ .
6. If Γ ` T . T 0 and JT Kσ ,ρ ∈ JκKσ ,ρ for some kind κ, then JT Kσ ,ρ = JT 0 Kσ ,ρ .
7. Suppose (X : κ) ∈ Γ, and let σ = σ1 ] σ2 and ρ = ρ1 ] ρ2 [X 7→ S]. Suppose also thatS ⊆κ,σ1 ,ρ1 S0 and A ⊆ JκKσ1 ,ρ1 , with A 6= 0.
/(a) If Γ ` T : κ 0 , Jκ 0 Kσ1 ,ρ1 is defined, and X ∈+ T , theni JT Kσ ,ρ[X7→S] ⊆κ 0 ,σ1 ,ρ1 JT Kσ ,ρ[X7→S0 ]ii ∩κ 0 ,σ1 ,ρ1 {JT Kσ ,ρ[X7→S] | S ∈ A} ⊆κ 0 ,σ1 ,ρ1
JT Kσ ,ρ[X7→∩κ,σ ,ρ A]
1 1(b) If Γ ` T : κ 0 and X ∈− T , then JT Kσ ,ρ[X7→S0 ] ⊆κ 0 ,σ1 ,ρ1 JT Kσ ,ρ[X7→S] .

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

19(c) If Γ ` κ 0 : , Jκ 0 Kσ1 ,ρ1 is defined, and X ∈+ κ 0 , theni Jκ 0 Kσ ,ρ ⊆ Jκ 0 Kσ ,ρ[X7→S0 ]ii ∩{Jκ 0 Kσ ,ρ[X7→S] | S ∈ A} ⊆ Jκ 0 Kσ ,ρ[X7→∩κ,σ ,ρ A]
1 1(d) If Γ ` κ 0 :  and X ∈− κ 0 , then Jκ 0 Kσ ,ρ[X7→S0 ] ⊆ Jκ 0 Kσ ,ρ .

8. If JκKσ ,ρ is defined, Γ, X : κ ` Θ : ?, JΘKσ ,ρ[X7→>κ ] , and CtorsX Θ, then (Jκ |X ΘKσ ,ρ , ⊆κ,σ ,ρ, ∩κ,σ ,ρ ) is a complete lattice.
These parts must be proved by mutual induction on the structure of the assumed derivation in each part. Parts (1), (2), and (3) of Theorem 13 are statements that the main
judgements of CDLE – superkinding, kinding, and typing, respectively – are sound withrespect to our semantics. Parts (4) and (5) express soundness of two helper judgements
dealing with constructor sets Θ. Parts (5) and (6) express soundness of directed conversion.
Parts (7) and (8) are critical for reasoning about ν-types. Parts (7ai) and (7ci) express
monotonicity of the semantics for type variables occurring only positively, and parts (7b)and (7d) express antimonotonicity for type variables occurring only negatively. Parts (7aii)and (7cii) are expressing one part of continuity, which is used in establishing that themeaning of a ν-type is indeed a fixed-point of the interpretation of its body; the otherends up following from monotonicity. Part (8) embodies one of the central insights ofconstructor-constrained recursive types: if a constructor set Θ satisfies CtorsX Θ, then it ispreserved not just through the chain of iterates of the interpretation of the body, but also in
the limit of that sequence, its greatest lower bound. Without preservation of Θ in the limit,
we cannot show that the meaning of a ν-type is the appropriate fixed point.
Corollary 14 (Logical consistency)
There is no derivation of · ` t : ∀X : ?.X, for any term t.
Proof
By Theorem 13 part (3) and the semantics of ∀-types, if · ` t : ∀X : ?.X is derivable, thent ∈ ∩R. But ∩R is empty since 0/ ∈ R.
7 Cedille: an Implementation of CDLE
I have implemented a system called Cedille based on CDLE. At first glance, this may
seem difficult, because of typing rules like direct computation and the introduction rulefor dependent intersections, which do not fit well into usual approaches to algorithmic
typing. But one insight emerges which helps us resolve these difficulties. These troublesome features of CDLE are needed solely for kinding recursive types. Once recursive types
are kinded, then it is a relatively simple matter to unfold them when their inhabitants are
eliminated (i.e., applied to arguments). We need never introduce them, if we are content to
use the constructors of the type (from the constructor sets) as the sole means of constructing
inhabitants of recursive types. This rules out defining alternative versions of operations
on lambda-encoded data, such as Rosser’s alternative definitions of multiplication andexponentiation (though supporting these would require additional rules in CDLE, to allow
typing of non-constructor terms with recursive types). But this is an acceptable loss togain the power of higher-order encodings. A final issue is the need to add typings t ∈ T

ZU064-05-FPR

paper

20

14 March 2017

20:59

Stump

to contexts, due to the fact that constructor sets contain typings of arbitrary terms. Thisissue is resolved in Cedille by introducing names for the constructors, which are used inplace of those arbitrary terms. Note that while the type-checking algorithm for annotatedterms implemented by Cedille is based closely on the definition of CDLE above, formallydefining this algorithm and proving the appropriate relation to CDLE must remain to future
work.
Cedille supports top-level definition of recursive types with the following syntax:
rec X params : indices | ctors = T with defs
Here, params and indices are telescopes of bindings, the first for parameters fixed for thewhole type definition, and the second for indices, which are inputs to the type constructor
X which may change in the body T of the definition. The ctors are declarations of constructors; this component of the definition is just like Θ, except that constraints are of the formx : T , where x is a constructor name, rather than t ∈ T . The definitions of the constructors
named in ctors, using whichever lambda encoding is being applied, are given in the defs.
For example, Figure 14 gives definitions of three standard datatypes: Nat is for Churchencoded natural numbers, List is for Parigot-encoded lists, and Vector is for Parigotencoded vectors (lists indexed by their length). Cedille uses the notation −t for an implicit(erased) argument, and Λ as a term-level binder for implicit inputs. Applications of terms
or types to types are written with the · operator for parsing reasons. In datatype definitions
only, the special variable self may be used as an implicitly ι-abstracted variable referringto the subject of the typing.
Let us consider how Cedille kinds the definition of Nat (Figure 14), for a representative
example. Cedille uses Unicode, so Cedille code largely matches the mathematical syntax
we have already considered. The constructor sets must first be typed, assuming the kinding
Nat : ?. Next, the body is kinded, assuming that self has the recursive type (applied toany indices). So in this case, self is assumed to have type Nat when kinding the body.
Finally, each constructor definition (the equations following the with keyword) must be
typed. Cedille types a definition c = t by checking that t has type T under the assumptionthat the recursively defined type is equal to its body, with the self variable explicitly ιabstracted. There a variety of other small checks to perform as well (the conditions imposedby CtorsX , the starting condition for kinding using the top type Uκ , and a few others).
Cedille implements local type inference to cut down on the number of annotations
required in terms (Pierce & Turner, 2000). We are either checking a term against a typeor a type against a kind, or else trying to synthesize a type for a term or a kind for a
type. Cedille seeks to instantiate ι-types introduced by recursive definitons either whenchecking against an introduction form (an implicit or explicit λ -abstraction), or when atype is synthesized for the head of an application. The former is intended just for typing
constructor definitions, while the latter is for use there as well as when terms of recursivetype are eliminated. This simple scheme appears sufficient so far to avoid any explicit
reasoning about dependent intersections on the part of the user.
Cedille implements an algorithmic conversion relation based on normalizing term andtype expressions. While this is not strictly speaking justified by Theorem 13 above, I
conjecture that the proof may, with some effort, be adapted to show not just consistency but
normalization. I have not invested this effort so far, for the following reason. Consistency is

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming21

rec Nat |S : Nat → Nat , Z : Nat =∀ P : Nat → ? .
(Π n : Nat . P n → P (S n)) → P Z → P selfwith
S = λ n . Λ P . λ s . λ z . s n (n · P s z) ,Z = Λ P . λ s . λ z . z.
rec List (A : ?) |Cons : A → List → List , Nil : List =∀ P : List → ? .
(Π h : A . Π t : List . P t → P (Cons h t)) →P Nil →
P selfwithCons = λ a . λ v . Λ P . λ c . λ e . c a v (v · P c e),
Nil = Λ P . λ c . λ n . n .
rec Vector (A : ?) : (n : Nat) |Cons : ∀ n : Nat . A → Vector n → Vector (S n) ,Nil : Vector Z =∀ P : Π n : Nat . Vector n → ? .
(∀ n : Nat . Π a : A . Π v : Vector n .
P n v → P (S n) (Cons -n a v)) →P Z Nil →P n self
withCons = Λ n . λ a . λ v . Λ P . λ c . λ e .
c -n a v (v · P c e) ,Nil = Λ P . λ c . λ n . n .
Fig. 14. Cedille definitions of three standard datatypes

the crucial property for a type theory, as it tells us that we may safely avoid reducing someterms, and still know that they would reduce to canonical values. Normalization is nice intheory, but in practice the enormous computational complexity of functions which can be
written in type theory means that there are terms which will cause type checking to run
so long as to be practically indistinguishable from nontermination. So any type theory that
truly requires a bound on the time required to check terms will have to do more than justprove normalization (and such theories have, of course, been developed; e.g., (Hofmann,
2000)).
Cedille itself is coded in Agda. Agda is a dependently typed programming language
under development (in its Agda 2 form) for around a decade. The main implementation
was done by Ulf Norell, with subsequent additions from other researchers (Norell, 2007).
Cedille makes use of the Iowa Agda Library, an alternative standard library I am developing, currently at a little under 5000 lines of code. This library is the basis for my bookon Agda (Stump, 2016). While I have not verified deep properties of the implementation
using Agda’s theorem-proving capabilities, I have expressed a number of simple program
invariants using dependent types, and used type-level computation to simplify and condense some of the code.

ZU064-05-FPR

paper

22

14 March 2017

20:59

Stump

Eq ⇐ Π A : ? . A → A → ? =λ A : ? . λ a : A . λ b : A . ∀ P : A → ? . P a → P b .
refl ⇐ ∀ A : ? . ∀ a : A . Eq · A a a =Λ A . Λ a . Λ P . λ u . u .
Fig. 15. Leibniz equality

8 Basic Examples
Now let us consider some examples demonstrating the features of CDLE, as implemented
in Cedille.
8.1 Inductive reasoning about Church-encoded numbers
First, let us show that we can indeed perform dependent eliminations with Church-encodednumbers, by proving a basic inductive fact about addition. We can define Leibniz equality
in the usual way, as shown in Figure 15. The statements shown in the figure are of theform x ⇐ e = e0 , for checking expression e0 against classifier (type or kind) e, andthen adding a definition of x to equal e0 to the global context. So here we define the type
Eq for Leibniz equality in a standard way, and then give an inhabitant refl for reflexive
equalities. As noted above, more complex forms of equality can also be defined using
constructor-constrained recursive types, but this is sufficient here.
If we define addition in the standard way, we can then write the following very basic
inductive proof about it, showing that x + 0 = x for all x:
add ⇐ Nat → Nat → Nat =λ n . λ m . n · (λ n : Nat. Nat) (λ n . S) m .
addZ ⇐ Π x : Nat . Eq · Nat (add x Z) x =λ x . x · (λ n : Nat . Eq · Nat (add n Z) n)(λ n . λ u . Λ P . λ v . u · (λ x : Nat . P (S x)) v)(refl · Nat -Z) .
As is well known, this theorem does not hold simply by reducing add x Z, because add
iterates on x. The term we have given as the definition for addZ has an induction on x
matching this iteration. The induction is carried out by a dependent elimination, where x
is applied, in the second line, to the predicate to be proved. The third line of the code gives
the step case, where u is the proof of P (add n Z), for an arbitrary predicate P postulated
by Leibniz equality, and the return value is then the proof of P n. The fourth line gives thebase case, which follows trivially using conversion.
8.2 True not equal to false
Figure 16 defines the Bool datatype using a constructor-constrained recursive type tosupport dependent eliminations on booleans. The figure also gives standard impredicative
definitions for the types True and False.
Using these definitions, we may then write the proof in Figure 17 deriving a contradiction from an assumption that tt (boolean true) equals ff, where the notion of equality

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

23

rec Bool | tt : Bool , ff : Bool =∀ P : Bool → ? .
P tt → P ff → P self
withtt = Λ P . λ a . λ b . a ,ff = Λ P . λ a . λ b . b .
True ⇐ ? = ∀ X : ? . X → X .
triv ⇐ True = Λ X . λ x . x .
False ⇐ ? = ∀ X : ? . X .
Fig. 16. Booleans, and true and false types
tt-not-equal-ff ⇐ Eq · Bool tt ff → False =λ u . u · (λ b . λ v .
(↑ X . b · (λ b . X) : (∗ → ∗ → ∗)) · True · False)
triv .
Fig. 17. Proof that boolean true is not equal to boolean false

is again Leibniz equality. Note that this fact is not provable for Church-encoded booleansin Coq, for instance (Werner, 1992). Here, we instantiate the variable P from the Leibniz
equality with a predicate which uses lifting (the ↑ expression) to compute the type False
from boolean ff and True from tt. This allows us to cast triv from type True to type
False. Using large eliminations is the standard way to prove this fact with primitive
datatypes, but large eliminations are not available for lambda encodings in other theories.
Lifting in CDLE makes this possible. In the Cedille implementation, we must explicitly
introduce the type variable X (immediately following the ↑ sign), which the term being
lifted will use to indicate the positions in the type which are to be lifted to the kind ?.
8.3 Higher-order encoding of System F types
Let us see how CDLE allows large eliminations with higher-order encodings of datatypes.
We would like to represent the types of System F (constructed by universal quantificationand function-space formation from type variables), using a higher-order encoding. So we
do not want to encode the universally bound variables as de Bruijn indices, for example.
Rather, we will use CDLE’s variables to represent these System F type variables.
Figure 18 declares the type tp, of kind ? to represent System F types. The type saysthat for all types X, a tp can take in a function of type X → X → X and also one of type
(X → X) → X, and return a value of type X. The first function is the one to use if thetp ⇐ ? = ∀ X : ? . (X → X → X) → ((X → X) → X) → X.
interp ⇐ tp → ? =λ T . ↑ Y . (T · Y) : ((∗ → ∗ → ∗) → ((∗ → ∗) → ∗) → ∗) ·(λ A . λ B . A → B) ·(λ F . ∀ C : ? . F · C) .
Fig. 18. Higher-order encoding of System F types, and its interpretation

ZU064-05-FPR

paper

14 March 2017

20:59

24

Stump

tp is representing an arrow type (and then the values computed for the domain and range
types will be supplied as the two arguments of type X). The second function takes in a
X → X function and returns a value of type X. Here we see the higher-order aspect of theencoding. Due to the negative occurence of X in the domain type X → X of this type, thiswould not be allowed as part of an inductive datatype definition in Coq or Agda, though it
could be defined in the pure λ -calculus fragment of Coq.
But Coq does not have anything like the lifting operation of CDLE, and so one could
not write the type-level function interp-tp of Figure 18, which interprets a tp as thecorresponding actual type of CDLE. This definition lifts the tp t to the type level, and thenapplies it to functions which compute either the arrow type or the universally quantified
type. In the latter case, the higher-order encoding presents us with F of type ? → ?, whichmaps any input type to the interpretation of the encoded body of the universal type. So wejust introduce a universally quantified C and apply F to that, to compute the interpretation.
For example, we may define the type of polymorphic identify functions as an inhabitantof tp:
polyid-t ⇐ tp = Λ X . λ arrow . λ forall .
forall (λ x . arrow x x) .
If we interpret this value using our interp function, Cedille tells us we get∀ C : ? . (C → C)
To demonstrate the point that we can eliminate data at multiple levels of the type theory,
let us also define a function to compute the size (as a natural number) of a tp:
size ⇐ tp → Nat =λ T : tp .
T · Nat(λ m . λ n . S (add n m))(λ s . S (s one)) .
Cedille reports that normalizing size polyid-t results in Church-encoded four:
λ s . λ z . (s (s (s (s z))))
It is important to note that in this example, we are using lifting only. Constructorconstrained recursive types require positivity, which would not hold here. Even though
we do not get a dependent elimination principle for a datatype like tp, we still gain extra
expressive power in CDLE over other impredicative type theories like that of Coq, due to
CDLE’s lifting operation.
8.4 Strong Σ-types
Strong Σ-types can be defined in CDLE, using constructor-constrained recursive types, asshow in Figure 19. As above, we define the type as its own induction principle. Defining
first and second projections is then straightforward. For fst, we instantiate the predicate
variable P with a trivial predicate that always returns A for any input. But for snd, we use
a nontrivial predicate, so that the type which λ a . λ b . b must inhabit isZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming25

rec Sigma (A : ?)(B : A → ?)| mksigma : Π a : A . B a → Sigma =∀ P : Sigma → ? .
(Π a : A . Π b : B a . P (mksigma a b)) → P selfwithmksigma = λ a . λ b . Λ P . λ c . c a b .
fst ⇐ ∀ A : ? . ∀ B : A → ? . Sigma · A · B → A= Λ A . Λ B . λ p .
p · (λ _ : Sigma · A · B . A) (λ a . λ b . a) .
snd ⇐ ∀ A : ? . ∀ B : A → ? . Π p : Sigma · A · B .
B (fst · A · B p)
= Λ A . Λ B . λ p .
p · (λ p : Sigma · A · B . B (fst · A · B p))(λ a . λ b . b).
Fig. 19. Strong Σ-types

Π a : A . Π b : (B a) . (B (fst (mksigma a b)))This type is convertible with just
Π a : A . Π b : (B a) . (B a)which is inhabited, as required, by λ a . λ b . b. This is a nice example of how
type refinement, as implemented in languages with dependent pattern matching (Coquand,1992), is also available in CDLE.
One might be concerned that despite the claimed Theorem 13 above, definability ofstrong Σ-types could somehow put CDLE afoul of Coquand’s result that the Calculusof Constructions with strong Σ-types is inconsistent (Coquand, 1986). But the system
considered by Coquand allows the formation of large Σ-types ΣX : κ.κ 0 , which are cruciallyused in the proof of inconsistency. In contrast, the Σ-types defined in Figure 19 are small,so Coquand’s result does not apply.
8.5 Statically typed higher-order abstract syntax
The higher-order encoding of System F types in Section 8.3 may leave some readers
wondering if typed abstract syntax can be represented in a similar way. For System F types
have only a trivial kinding structure, which the encoding of Section 8.3 thus did not have totake into account. Figure 20 gives a higher-order encoding of the typed syntax for simply
typed lambda calculus. The figure first defines tp, representing the simple types with asingle base type. Constructors arrow and base for this type are then defined. Then trm isdefined, of kind tp → ?. Then trm T is the type for representations of simply typed terms
t with type represented by T. The definition of trm first takes in the type T for this family ofterms, and then a type X indexed by tp. The cases for application and λ -abstraction comenext. Note that the λ -abstraction case is higher-order: given a function from X T1 to X T2,
the function supplied for this case must deliver a value of type X (arrow T1 T2).
Figure 21 defines example terms id and test, of type trm abb and trm test-tp, respectively, where abb and test-tp represent b → b and (b → b) → (b → b), respectively.

ZU064-05-FPR

paper

26

14 March 2017

20:59

Stump

tp ⇐ ? = ∀ X : ? . (X → X → X) → X → X .
arrow ⇐ tp → tp → tp =λ T1 . λ T2 . Λ X . λ a . λ b . a (T1 · X a b) (T2 · X a b) .
base ⇐ tp = Λ X . λ a . λ b . b.
trm ⇐ tp → ? =λ T : tp.
∀ X : tp → ? .
(∀ T1 : tp . ∀ T2 : tp . X (arrow T1 T2) → X T1 → X T2) →(∀ T1 : tp . ∀ T2 : tp . (X T1 → X T2) → X (arrow T1 T2)) →X T.
Fig. 20. Typed higher-order abstract syntax for STLC terms
abb ⇐ tp = arrow base base.
id ⇐ trm abb = Λ X . λ a . λ l . l -base -base (λ x . x) .
test-tp ⇐ tp = arrow abb abb .
test ⇐ trm test-tp =Λ X . λ a . λ l .
l -abb -abb (λ s .
l -base -base (λ z .
a -base -base s (a -base -base (id · X a l) (a -base -base s z)))).
Fig. 21. Example terms and types in the encoding

The trm id represents λ x.x, and test represents λ s.λ z.s (id (s z)). Because Cedille’s type
inference is currently just basic local type inference, quite a few erased arguments must be
supplied. Improving this situation is future work. The erasure of test, however, is thefollowing, which does encode the test term as expected:
λ a . λ l . (l (λ s . (l (λ z . (a s (a (id a l) (a s z)))))))
Finally, Figure 22 defines a very simple interpreter for trm. This is interp-trm. To
express its type, we first define interp-tp using lifting. This is a simpler version of theinterp-tp function we saw in Figure 18 for System F types. The definition of interp-trm
uses interp-tp (of Figure 22) and dependent types to express the idea that the interpretation of a trm T is a CDLE term of CDLE type interp-tp T. The interpretation isthen completely direct: (typed) application is interpreted as application, and λ -abstraction
is interpreted as λ -abstraction. Interpreting test results in λ s . λ z . (s (s z)),which as expected, has evaluated the term as part of interpreting it (cf. normalization byevaluation (Berger & Schwichtenberg, 1991)).
9 Formatted printing with local definitions
Let us now consider a more complex case of large eliminations with higher-order encodings: adding local definitions to format specifiers for formatted printing as with printf.
Typing printf is now a standard and quite appealing example of dependently typed
programming, introduced by Augustsson (Augustsson, 1998). Here, we will allow format
specifiers – for which we will use a dedicated datatype, not a format string – to contain two
types of let-declarations. flet x y will specify that the arguments required by x should

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

27

interp-tp ⇐ tp → ? =λ T : tp . (↑ X . T · X : ((∗ → ∗ → ∗) → ∗ → ∗))· (λ T1 : ? . λ T2 : ? . T1 → T2)· True.
interp-trm ⇐ ∀ T : tp . trm T → interp-tp T =Λ T . λ t .
t · (λ T : tp . interp-tp T)(Λ T1 . Λ T2 . λ f . λ a . f a)(Λ T1 . Λ T2 . λ r . λ x . r x).
Fig. 22. Interpreting encoded types and terms

be input to the call to format, and then the resulting string which is computed for x will be
substituted into y. More dynamic is fletd x y, which just substitutes x into y, and thus
could duplicate requirements for arguments (leading to additional arguments to the call toformat). We will print lists of booleans rather than lists of characters, to avoid dependence
on a primitive type of characters.

9.1 Agda implementation
Figures 23 and 24 give Agda code for this example (based on the Iowa Agda Library). The
approach used here is not the one which would typically be adopted in Agda, because it
requires that we disable Agda’s positivity checker to use a higher-order encoding, thus sacrificing the termination property which Agda seeks to guarantee. The first point of showing
this solution is explanatory: hopefully it will orient readers familiar with Agda or Haskell,for the subsequent Cedille implementation (Section 9.2). Secondly, though, it is meant tohighlight that this implementation technique – which results in a reasonable solution forthis novel problem – is not available in Agda without compromising termination. Of course
the example itself could be implemented using other methods, such as de Bruijn indices forrepresenting bound variables. But with Cedille, the possibility of a higher-order solution tothis problem is available, without compromising logical soundness.
To turn to the code of Figure 23: we have a datatype formatti which will describe theargument requirements of format specifiers. A format specifier can require an argument(iarg), no argument (inone), or appended requirements (iapp), or requirements governedby a dynamic let (ilet). The type formati is the type for the actual format specifiers.
The interesting cases are for flet and fletd, where we use higher-order encoding. In
the static case (flet), we have a function from inputs with argument requirement inone
to outputs with requirement b, and in the dynamic case, the requirement goes from a tob a. The types of the inputs to these constructors use the formati in negative positions,and hence would be disallowed by Agda without the initial pragma disabling the positivity
check.
The function format-t (Figure 24) computes the type for format from an argument requirement (of type formatti), while format itself (or rather, the helper function formath)is defined by recursion on the format specifier (of type formati). The formath functionuses a continuation so that interpretation of the format directive can take place before any
input arguments are required (by an farg format specifier).

ZU064-05-FPR

paper

14 March 2017

20:59

28

Stump

{-# OPTIONS --no-positivity-check #-}module format-ilet where
open import lib
data formatti : Set whereiarg : formatti
inone : formatti
iapp : formatti → formatti → formatti
ilet : formatti →(formatti → formatti) → formatti
bitstr : Set
bitstr = L B
data formati : formatti → Set where
farg : formati iarg
fapp : {a b : formatti} →formati a → formati b →formati (iapp a b)
flet : {a b : formatti} → formati a →(formati inone → formati b) →formati (iapp a b)
fletd : {a : formatti}{b : formatti → formatti} →formati a →(formati a → formati (b a)) →formati (ilet a b)
fbitstr : bitstr → formati inone
flit : B → formati inone
flit b = fbitstr [ b ]Fig. 23. Datatype definitions for format with local definitions, in Agda

For a test case, we can define
testi : formatti
testi = ilet (iapp iarg (iapp inone inone))(λ x → iapp x (iapp inone x))
test : formati testi
test = fletd (flet farg (λ j → fapp j j))(λ i → fapp i (fapp (flit tt) i))
The format specifier test says that we want to print a string consisting of i followed
by a boolean literal tt (flit tt), and then i again, where i is dynamically defined to be
the static definition flet farg (λ j → fapp j j). This requests one argument to be
named j, and then produces j appended to j. Agda’s normalizer reports that as expected,
format test normalizes to
λ x x1 → x :: x :: tt :: x1 :: x1 :: []ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

29

format-th : formatti → Set → Set
format-th iarg r = B → rformat-th inone r = r
format-th (iapp i i’) r =format-th i (format-th i’ r)format-th (ilet i i’) r = format-th (i’ i) r
format-t : formatti → Set
format-t i = format-th i bitstr
formath : {i : formatti} → formati i →{A : Set} → (bitstr → A) → format-th i A
formath farg f x = f [ x ]formath (fapp i i’) f =formath i (λ s → formath i’ λ s’ → f (s ++ s’))formath (flet i i’) f =formath i (λ s → formath (i’ (fbitstr s)) f)
formath (fletd i i’) f = formath (i’ i) f
formath (fbitstr s) f = f sformat : {i : formatti} → formati i → format-t iformat i = formath i (λ x → x)
Fig. 24. Formatted printing with local definitions, in Agda

9.2 Cedille implementation
Let us now implement this example in Cedille. It is worth emphasizing that no modification
to CDLE is required (whereas we had to disable positivity checking for the example to typecheck in Agda). We should also note that similarly to the example of representing the typesof System F (Section 8.3), we will use higher-order encodings that prevent us from using
constructor-constrained recursive types. Lifting, however, is still available, and is sufficientfor this example. First, we must declare the type formatti for argument requirements.
We break this into two parts: a type-level function formatto, and then the universal typeformatti:
formatto ⇐ ? → ? =λ X : ? . X → X → (X → X → X) → (X → (X → X) → X) → X .
formatti ⇐ ? = ∀ X : ? . formatto · X .
We can define abbreviations for the constructors of this type, the last of which is themost interesting, since it is there that higher-order encoding shows up:
iarg ⇐ formatti = Λ X . λ a . λ n . λ p . λ l . a .
inone ⇐ formatti = Λ X . λ a . λ n . λ p . λ l . n .
iapp ⇐ formatti → formatti → formatti =λ x . λ y .
Λ X . λ a . λ n . λ p . λ l .
p (x · X a n p l) (y · X a n p l).
ilet ⇐ formatti → (∀ X : ? . X → formatto · X) → formatti =λ u . λ f .

ZU064-05-FPR

paper

30

14 March 2017

20:59

Stump

formato ⇐ (formatti → ?) → formatti → ? =λ X : formatti → ? . λ i : formatti.
X iarg →(∀ a : formatti . ∀ b : formatti.
X a → X b → X (iapp a b)) →(∀ a : formatti . ∀ b : formatti.
X a → (X inone → X b) → X (iapp a b)) →(∀ x : formatti . ∀ F : ∀ X : ? . X → formatto · X.
X x →(X x →X (Λ X . λ a . λ n . λ p . λ l . F · X (x · X a n p l)
a n p l)) →X (ilet x F)) →(bitstr → X inone) →X i .
formati ⇐ formatti → ? =λ i : formatti . ∀ X : formatti → ? . formato · X i.
Fig. 25. The type formati for format strings

Λ X . λ a . λ n . λ p . λ l .
l (u · X a n p l) (λ x . f · X x a n p l) .
The argument f to ilet takes in an X and returns a formatto · X, for any type X. Thiscan be viewed as saying that f is a member of an extension of the datatype formatti witha new constructor (since f requires a value of type X for this constructor).
We elide a few easy definitions (Church-encoded booleans, an append operation onlists, and the bsingleton function for creating a singleton list from boolean input). Next
comes the type formati for format specifiers. Again, we break it into two parts, shown in
Figure 25.
The type for the dynamic let (beginning on the eighth line in the figure) is the trickiest, since the argument requirement for the body of the let depends on the argument
requirement x for the let’s definiens. But our definition of ilet requires a F that canbe extended with the value for a variable, which enables expression of this dependence.
For space reasons, we must omit the definitions of constructors for this type, and turn tothe definition of format-th. To make reasoning about this definition more manageable,
we pre-define the type-level functions that will be used for the different cases of a formati
term. The code is shown in Figure 26. The crucial point, of course, is to use lifting to define
the type by higher-order iteration on the input of type formatti.
It is convenient to break out the return type for formath as a separate definition (formathr),
and then we have the code for formath itself, shown in Figure 27. Instead of recursive
calls, the higher-order iteration on a of type formati presents us with results r of recursive
calls, in each case. As we are computing a higher-order function (of type formathr), theseresults are themselves functions, which we call with a continuation to obtain the printing
function for the part of the format string from which the result was iteratively computed.
The final definition of the format function and its return type is then the following,where for the outermost continuation we use a function CList which converts Parigotencoded to Church-encoded lists. This just makes the output produced by Cedille’s inter-

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming31k ⇐  = ? → ? .
Fa ⇐ k = λ r : ? . (Bool → r) .
Fn ⇐ k = λ r : ? . r .
Fp ⇐ k → k → k = λ f : k . λ g : k . λ r : ? . f · (g · r) .
Fl ⇐ k → (k → k) → k = λ f : k. λ g : k → k . λ r : ? . (g · f · r) .
format-th ⇐ formatti → ? → ? =λ i : formatti .
↑ X . i · (X → X) : ((∗ → ∗) →(∗ → ∗) →((∗ → ∗) → (∗ → ∗) → (∗ → ∗)) →((∗ → ∗) → ((∗ → ∗) → (∗ → ∗)) → (∗ → ∗)) →(∗ → ∗)) · Fa · Fn · Fp · Fl .
Fig. 26. Definition of the helper function computing the type for a call to format from a format
stringformathr ⇐ formatti → ? =λ i : formatti . ∀ A : ? . (bitstr → A) → format-th i · A .
formath ⇐ ∀ i : formatti . formati i → formathr i =Λ i . λ x . x · formathr(Λ A . λ f . λ b . f (bsingleton b))(Λ a . Λ b . λ r . λ r2 .
Λ A . λ f . r · (format-th b · A)
(λ s . r2 · A(λ s’ . f (append · Bool s s’))))(Λ a . Λ b . λ r . λ r2 .
Λ A . λ f . r · (format-th b · A)
(λ s . r2 (Λ A . λ f . f s) · A f))(Λ x . Λ F . λ r . λ r2 .
Λ A . λ f . r2 r · A f)
(λ s . Λ A . λ f . f s) .
Fig. 27. Definition of the helper function for |format—

preter more readable in this case. The code is in Figure 28. We can use Cedille’s normalizer
with the same test as we used for the Agda version, to obtain(λ b’ . λ b’’ .
λ c . λ e .
(c b’ (c b’ (c (λ a’ . λ b’’’ . a’) (c b’’ (c b’’ e))))))
This is indeed a Church-encoded version of the answer we computed with the Agda implementation (at the end of Section 9.1).
format-t ⇐ formatti → ? = λ i : formatti . format-th i · (CList · Bool) .
format ⇐ ∀ i : formatti . formati i → format-t i =Λ i : formatti . λ t : formati i .
formath -i t · (CList · Bool) (toCList · Bool) .
Fig. 28. The definition of the format function and its return type

ZU064-05-FPR

paper

14 March 2017

20:59

32

Stump

((↑ X . (λ a . λ n . λ p . λ l . (F (x a n p l) a n p l)): ((∗ → ∗) → (∗ → ∗) → ((∗ → ∗) → (∗ → ∗) → (∗ → ∗)) →((∗ → ∗) → ((∗ → ∗) → (∗ → ∗)) → (∗ → ∗)) → (∗ → ∗)))
· Fa · Fn · Fp · Fl · A)
Fig. 29. A lifting type arising in the flet caseIn typing the formath term of Figure 27, several conversions dealing with lifting are
required. These are the last two conversions shown in Figure 5 above. Let us see briefly
how these arise. In typing the cases for fapp and flet, Cedille must check that the typeformat-th (iapp a b) · A is convertible withformath-th a · (format-th b · A)
The latter type arises from the terms r · (format-th b · A) in both cases, while theformer type is the one required by the elimination of the format specifier x. Since lifting
introduces new lifting redexes for arguments to a head variable, normalizing the first type
would, without the η-contraction lifting conversion of Figure 5 (the first conversion in thelast row of the figure), produce what is essentially an η-expanded version of a to be lifted.
The last conversion of Figure 5 is needed for the fletd case, where Cedille must checkthat format-th (ilet x F) · A is convertible with the type shown in Figure 29. Again,
due to the way lifting produces new lifting redexes, normalization of the first type would
result in a lifting of F being applied to a lifting of x. Those two uses of the lifting operationneed to be consolidated at the top level of the term, in order to match the type of Figure 29.
This is what the final conversion of Figure 5 does.

10 Related Work
We compare the approach of CDLE with some recent works. In “The Gentle Art of Levitation” (Levitation), Chapman et al. present a closed type theory where inductive datatypes
are implemented using a universe of datatype descriptions, which, cleverly, is itself given a
datatype description (Chapman et al., 2010). CDLE does not include a universe, although
as a closed type theory it would make sense to consider extending it with one. Levitationis concerned with encoding universes of datatypes as datatypes themselves, but not withfoundations of induction. Indeed, least fixed points of functors (polynomial, then strictly
positive), and associated induction principles, are included as primitives of the theory.
Some primitive datatypes are included as part of the type theory; indeed, Levitation affirms“We cannot dispose of data altogether!” (Section 4.1). In contrast, CDLE defines data as
their own induction principles, and hence reduces induction to the underlying impredicative
type theory; CDLE does not include any induction principle as primitive, nor any datatypes.
One could imagine attempting to replace the primitive induction principle used in Levitation, with induction as derived in CDLE. But Levitation’s self-describing universe construction crucially relies on a predicative universe hierarchy, which we have omitted here
in CDLE. Levitation also affirms, citing (Geuvers, 2001): “An impredicative Church-style
encoding of datatypes is not adequate for dependently typed programming, as althoughsuch encodings present data as non-dependent eliminators, they do not support dependent
induction”. CDLE overturns the received wisdom that Geuvers’s Theorem implies theZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

33

inadequacy of lambda encodings for dependent type theory. The theorem only shows thisfor second-order dependent type theory, leaving open the possibility that extensions to thattheory could be adequate – as we have seen with CDLE.
It is worth noting at this point that while universe polymorphism might appear to allow
data to be eliminated across levels – thus solving the same problem as CDLE’s proposed
lifting operator – such quantifications are predicative (Harper & Pollack, 1989). Indeed, auniverse-polymorphic type cannot itself be in any of the universes whose levels it quantifies
over, and in Agda is considered to be at ordinal level ω. The computational power ofpredicative polymorphism is quite limited compared with impredicative polymorphism,
as analyzed by Leivant (Leivant, 1991). In contrast, CDLE avoids adding a hierarchy ofuniverses by using a novel lifting operator to move expressions from the term level to thetype level of the language.
Altenkirch et al. pursue a related goal to Levitation’s in “PiSigma: Dependent Types
without the Sugar” (PiSigma): show how to define datatypes (inductive and co-inductive,indexed) and other central constructs of type theory in a minimalistic core language (Altenkirch et al., 2010). Special care is paid to the control of reduction during type checking,for recursively defined types and terms, using lifted types, inhabited by suspended terms.
These are different from CDLE’s lifting types, which actually raise terms to the type level.
PiSigma includes the ? : ? principle, and so levels cannot be distinguished. Furthermore,general recursion is allowed, and questions both of termination and metatheory in generalare deferred to later work. This is in contrast with CDLE, which is proved logically sound,and in which a sound notion of induction is defined.
Let us consider several works more focused on semantics and induction. In “Internalizing Relational Parametricity in the Extensional Calculus of Constructions” (Internalizing),
Krishnaswami and Dreyer develop a version of the Calculus of Constructions with a builtin equality type that enjoys equality reflection (Krishnaswami & Dreyer, 2013): if an equality is provable then it can be used definitionally – the central idea of extensional MartinLöf type theory (Martin-Löf, 1984). They devise a relationally parametric realizability
model, and show how this model validates various extensions of their syntactic theory,
includes strong sum types. But these are true extensions: the type theory proposed byInternalizing does not actually allow typing strong sum types, for example. In contrast, we
saw above (Section 8.4) that strong sigma types can be defined within CDLE (without any
extensions). The same is true for natural-number induction, which again in Internalizing isshown consistent with their proposed syntactic theory, but has to be added as an extension
to the theory. On the other hand, Internalizing gives examples of (semantically) relating
extensionally equal terms which the semantics for CDLE given in Section 5 above would
distinguish (cf. Section 5.4 of Internalizing). Developing extensional models of CDLE,
perhaps along the lines of Internalizing or perhaps following the “extensional collapse”
approach of Tannen and Coquand, remains to future work (Tannen & Coquand, 1988). A
similar goal with some stronger results – notably that every indexed functor has an initial
algebra – was achieved by Atkey et al. (Atkey et al., 2014).
The paper “Fibrational Induction Rules for Initial Algebras” of Ghani et al. proposesa general induction rule for arbitrary functors with initial algebras (Ghani et al., 2010).
The development is categorical, using the idea of a fibration to generalize the logicalnotion of predicate. The paper is focused on categorical semantics, and explicitly avoids

ZU064-05-FPR

paper

34

14 March 2017

20:59

Stump

impredicativity. In contrast, the present work on CDLE develops a new impredicative
type theory, with a concrete realizability semantics. The deeper insights into the nature ofinduction arising from categorical study could provide more refined analysis of the forms
of induction possible in CDLE, but this must remain to future work.
The lifting types of CDLE and its realizability semantics may put one in mind of “Realizability and Parametricity in Pure Type Systems” (Realizability), by Bernardy and Lasson (Bernardy & Lasson, 2011). In this elegant paper, the authors seek to shed light on therelationship between realizability and parametricity, by formally defining both as relations
on terms in a base PTS (first level), using another PTS (second level) viewed as a logic
for the first one. Terms in the first-level PTS are lifted to the second-level PTS, which
may then express statements about them. But in Realizability, lifting, like realizability andparametricity, are expressed as meta-level operations on PTS terms. In contrast, CDLE’s
lifting types are part of the type theory, which enables computation of types from terms,
within the theory. For the PTS corresponding to CC, for example, this is not possible. The
ideas of Realizability may, however, shed further light on CDLE’s lifting types, as well ason the best approach to formalizing CDLE’s metatheory. Note finally that while PTSs are
expressed using a unified syntax for expressions (instead of syntactically different classes
for terms, types, and kinds as in CDLE), some form of lifting is still required to lift a typing
judgment. In Realizability this is at the meta-level, while with CDLE it is in the theory.
Next, let us compare the present approach to the works, already mentioned in Section 1.1, based on adding primitive inductive types to existing type theories (i.e., (Werner,
1994; Pfenning & Paulin-Mohring, 1989; Coquand & Paulin, 1988)). With primitive inductive types, one should determine some set of inductive types which will be acceptedby the type theory, if one wishes to be able to prove any general results about the addition (for an open theory) or declaration (for a closed one) of a new inductive type. For
example, CIC restricts attention to inductive types generated by strictly positive functors(see (Werner, 1994), Definition 2.7). In CDLE, there are more options: if one needs induction and uses constructor-constrained recursive types, then we require only positivity. If
induction is not needed, then there are no restrictions at all on the functors one may use, for
Church-encoded datatypes (for the Parigot-encoding, of course, positive recursive types areneeded). Describing a class of inductive datatypes is not a simple matter. Indeed, Levitation
proposes an intricate solution to the problem. In Werner’s dissertation, one finds quite longtyping rules with lots of vector notation, to handle the variable-arity nature of both theinductive types and their constructors (and constructors’ types). None of this is needed in
CDLE. Finally, with primitive inductive types, one must augment the reduction relation,necessitating a new proof of confluence for reduction. With CDLE, the reduction relation
is just standard β -reduction on untyped terms, so there is no new confluence theorem toprove.
Finally, let us compare with a few works on advanced representations of syntax, suchas typed or higher-order abstract syntax. The idea of using higher-order representations in
typed lambda calculus can be traced back to Church’s Simple Theory of Types, where universal quantification, for example, is defined to be the application of a function Πo(oa) (expressing universality of a propositional function) to a lambda abstraction (Church, 1940).
The term “higher-order abstract syntax” was coined by Pfenning and Elliott for the idea ofrepresenting the syntax of various object languages using typed λ -abstractions (Pfenning

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

35& Elliott, 1988). Many works have explored the idea of shallowly embedding objectlanguage syntax into meta-language syntax. For one example, Mogensen proposed a shallow embedding of the syntax of pure lambda calculus in itself (Mogensen, 1992). For
another, Carette et al. in “Finally tagless, partially evaluated: Tagless staged interpreters
for simpler typed languages” show how to define various metaprograms (interpreters,compilers, and more) by semantically embedding the syntactic structure of an object language into a metalanguage (Carette et al., 2009). This gives a typed (shallowly embedded)
syntax similar to the example of Section 8.5. As Chlipala points out, though, directly
mapping object-language types to metalanguage-language types makes it more complex
to perform type-level operations (Chlipala, 2008). In the cited paper, Chlipala proposesparametric higher-order abstract syntax (PHOAS) for achieving some of the benefits ofhigher-order encodings in Coq (which due to positivity restrictions on datatypes cannot
support HOAS directly). Fegaras and Sheard proposed a method for programming withhigher-order representations in functional programming languages with primitive inductive
datatypes (Fegaras & Sheard, 1996). In contrast to these works, CDLE supports impredicatively typed higher-order syntactic representations.
There are many works proposing two-layer schemes, where object-language expressions
are represented in a typed lambda calculus with a relatively weak function space, while
metaprograms are written in a more powerful lambda calculus with pattern matching on
higher-order representations (Poswolsky & Schürmann, 2009; Pientka, 2008; Schürmann
et al., 2001). In CDLE, in contrast, there is just a single (typed) language for higher-orderrepresentations and programs over these. One might be concerned that the stronger function
space of CDLE will spoil adequacy of encodings. For developments where it is criticalto capture exactly the object-language syntax instead of over-approximate it, one could
use techniques such as proposed by Crary for representing linear logic proof terms in anonlinear metalanguage (Crary, 2010) (see also (Polakow, 2015)), namely Twelf (Pfenning& Schürmann, 1999).

11 Conclusion and Future Work
This paper has demonstrated that lambda encodings can be the basis for a dependent typetheory supporting both induction and large eliminations, via the system CDLE and its implementation Cedille. Induction is enabled by the novel constructor-constrained recursive
types ν X : κ | Θ. T , where Θ is a set of typing constraints on pure lambda terms whichmust be shown to hold for a top type Uκ and then be preserved by the body T . Under
some light restrictions on the use of X in the types in Θ, these typings hold not just for
the elements of the infinite sequence of increasing dependent types one can associatewith the ν-type, but also for the limit of that sequence, which our semantics defines themeaning of the type to be. Large eliminations are enabled by a lifting construct ↑L t, whichlifts simply typed lambda terms to the type level. We gave a rather simple semantics fortypes in terms of complete lattices, and proved the typing rules of CDLE sound withrespect to this semantics. Logical consistency of the system is then a corollary. CDLE
does not use a datatype system, and hence one could hope would be less cumbersome forformal metatheoretic analysis. The most exciting application of CDLE is for dependently

ZU064-05-FPR

paper

36

14 March 2017

20:59

Stump

typed programming with higher-order encodings. We gave several examples, including thenontrivial one of formatted printing with local definitions.
Programming with higher-order lambda-encodings is a delicate matter (cf. (Washburn& Weirich, 2003) for one illuminating example). Much more exploration of this area isrequired. It would be interesting, for example, to see how much formalized metatheory
one could do using higher-order encodings in Cedille. CDLE has shown that one can havedependent typing for higher-order encodings, via lifting. Induction for such encodings,
however, is prevented currently by the positivity requirement for constructor-constrained
recursive types. Thus devising inductive higher-order encodings is the most important next
direction for future work.
Acknowledgments. I gratefully acknowledge NSF support of this project under award
1524519, and DoD support under award FA9550-16-1-0082 (MURI program). I also deeply
thank Madeliene Stump for her support while I was writing this paper. AMDG.

References
Abel, Andreas, & Matthes, Ralph. (2004). Fixed Points of Type Constructors and Primitive
Recursion. Pages 190–204 of: Marcinkowski, Jerzy, & Tarlecki, Andrzej (eds), Computer Science
Logic (CSL), 18th International Workshop.
Altenkirch, Thorsten, Danielsson, Nils Anders, Löh, Andres, & Oury, Nicolas. (2010). PiSigma:
Dependent Types without the Sugar. Pages 40–55 of: Blume, Matthias, Kobayashi, Naoki, &Vidal, Germán (eds), Functional and logic programming, 10th international symposium (flops).
Lecture Notes in Computer Science, vol. 6009. Springer.
Atkey, Robert, Ghani, Neil, & Johann, Patricia. (2014). A Relationally Parametric Model of
Dependent Type Theory. Sigplan not., 49(1), 503–515.
Augustsson, Lennart. (1998). Cayenne - a language with dependent types. Pages 239–250 of:Felleisen, Matthias, Hudak, Paul, & Queinnec, Christian (eds), Proceedings of the third ACM
SIGPLAN international conference on functional programming (ICFP).
Berger, Ulrich, & Schwichtenberg, Helmut. (1991). An Inverse of the Evaluation Functional for
Typed Lambda-calculus. Pages 203–211 of: Proceedings of the sixth annual symposium on logic
in computer science (lics). IEEE Computer Society.
Bernardy, Jean-Philippe, & Lasson, Marc. (2011). Realizability and Parametricity in Pure Type
Systems. Pages 108–122 of: Hofmann, Martin (ed), Foundations of software science andcomputational structures - 14th international conference (fossacs). Lecture Notes in Computer
Science, vol. 6604. Springer.
Böhm, Corrado, & Berarducci, Alessandro. (1985). Automatic synthesis of typed lambda-programson term algebras. Theor. comput. sci., 39, 135–154.
Carette, Jacques, Kiselyov, Oleg, & Shan, Chung-chieh. (2009). Finally tagless, partially evaluated:
Tagless staged interpreters for simpler typed languages. J. funct. program., 19(5), 509–543.
Chapman, James, Dagand, Pierre-Évariste, McBride, Conor, & Morris, Peter. (2010). The gentle artof levitation. Pages 3–14 of: Hudak, Paul, & Weirich, Stephanie (eds), Proceeding of the 15th
ACM SIGPLAN international conference on functional programming (icfp). ACM.
Chlipala, Adam. (2008). Parametric higher-order abstract syntax for mechanized semantics. Pages
143–156 of: Hook, James, & Thiemann, Peter (eds), Proceedings of the 13th ACM SIGPLAN
International Conference on Functional Programming (ICFP). ACM.
Church, Alonzo. (1940). A Formulation of the Simple Theory of Types. J. symb. log., 5(2), 56–68.
Church, Alonzo. (1941). The Calculi of Lambda Conversion. Princeton University Press. Annals of
Mathematics Studies, no. 6.

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

37

Constable, Robert L., Allen, Stuart F., Bromley, Mark, Cleaveland, Rance, Cremer, J. F., Harper,
R. W., Howe, Douglas J., Knoblock, Todd B., Mendler, N. P., Panangaden, Prakash, Sasaki,
James T., & Smith, Scott F. (1986). Implementing mathematics with the nuprl proof development
system. Prentice Hall.
Coquand, Thierry. (1986). An Analysis of Girard’s Paradox. Pages 227–236 of: Proceedings,
symposium on logic in computer science (lics). IEEE Computer Society.
Coquand, Thierry. (1992). Pattern Matching with Dependent Types. Nordström, Bengt, Petersson,
Kent, & Plotkin, Gordon (eds), Electronic proceedings of the third annual bra workshop on logicalframeworks. Available from Coquand’s home page.
Coquand, Thierry, & Paulin, Christine. (1988). Inductively defined types. Pages 50–66 of: MartinLöf, Per, & Mints, Grigori (eds), Colog-88, international conference on computer logic.
Crary, Karl. (2010). Higher-order representation of substructural logics. Pages 131–142 of: Hudak,
Paul, & Weirich, Stephanie (eds), Proceeding of the 15th ACM SIGPLAN International Conference
on Functional Programming (ICFP). ACM.
Fegaras, Leonidas, & Sheard, Tim. (1996). Revisiting Catamorphisms over Datatypes with
Embedded Functions (or, Programs from Outer Space). Pages 284–294 of: Boehm, HansJuergen, & Jr., Guy L. Steele (eds), The 23rd ACM SIGPLAN-SIGACT symposium on principles
of programming languages (popl). ACM Press.
Fortune, Steven, Leivant, Daniel, & O’Donnell, Michael. (1983). The Expressiveness of Simple andSecond-Order Type Structures. J. ACM, 30(1), 151–185.
Fu, Peng, & Stump, Aaron. (2014). Self Types for Dependently Typed Lambda Encodings. Pages
224–239 of: Dowek, Gilles (ed), 25th International Conference on Rewriting Techniques andApplications (RTA) joint with the 12th International Conference on Typed Lambda Calculi andApplications (TLCA).
Geuvers, Herman. (2001). Induction Is Not Derivable in Second Order Dependent Type Theory.
Pages 166–181 of: Typed lambda calculi and applications (tlca).
Ghani, Neil, Johann, Patricia, & Fumex, Clément. (2010). Fibrational Induction Rules for Initial
Algebras. Pages 336–350 of: Dawar, Anuj, & Veith, Helmut (eds), Computer science logic, 24thinternational workshop (csl). Lecture Notes in Computer Science, vol. 6247. Springer.
Girard, Jean-Yves, Taylor, Paul, & Lafont, Yves. (1989). Proofs and types. New York, NY, USA:
Cambridge University Press.
Goguen, Healfdene, McBride, Conor, & McKinna, James. (2006). Eliminating Dependent Pattern
Matching. Pages 521–540 of: Futatsugi, Kokichi, Jouannaud, Jean-Pierre, & Meseguer, José (eds),
Algebra, meaning, and computation, essays dedicated to joseph a. goguen on the occasion of his
65th birthday.
Harper, Robert, & Pollack, Robert. (1989). Type Checking, Universe Polymorphism, and Typical
Ambiguity in the Calculus of Constructions (Draft). Pages 241–256 of: Dı́az, Josep, & Orejas,
Fernando (eds), Tapsoft’89: Proceedings of the international joint conference on theory andpractice of software development, barcelona, spain, march 13-17, 1989, volume 2: Advanced
seminar on foundations of innovative software development II and colloquium on current issues
in programming languages (CCIPL). Lecture Notes in Computer Science, vol. 352. Springer.
Hofmann, M., & Streicher, T. (1998). The groupoid interpretation of type theory. Pages 83–111 of:Twenty-five years of constructive type theory. Oxford Logic Guides, vol. 36. Oxford University
Press.
Hofmann, Martin. (2000). Safe recursion with higher types and bck-algebra. Annals of pure andapplied logic, 104(1–3), 113 – 166.
Koopman, Pieter, Plasmeijer, Rinus, & Jansen, Jan Martin. (2014). Church Encoding of Data Types
Considered Harmful for Implementations. Plasmeijer, Rinus, & Tobin-Hochstadt, Sam (eds), 26th
Symposium on Implementation and Application of Functional Languages (IFL). Presented version.

ZU064-05-FPR

paper

38

14 March 2017

20:59

Stump

Kopylov, Alexei. (2003). Dependent intersection: A new way of defining records in type theory.
Pages 86–95 of: 18th IEEE symposium on logic in computer science (LICS).
Krishnaswami, Neelakantan R., & Dreyer, Derek. (2013). Internalizing Relational Parametricity inthe Extensional Calculus of Constructions. Pages 432–451 of: Rocca, Simona Ronchi Della (ed),Computer science logic 2013 (csl). LIPIcs, vol. 23. Schloss Dagstuhl - Leibniz-Zentrum fuer
Informatik.
Leivant, Daniel. (1983). Reasoning about functional programs and complexity classes associatedwith type disciplines. Pages 460–469 of: Foundations of computer science, 1983., 24th annual
symposium on.
Leivant, Daniel. (1991). Finitely Stratified Polymorphism. Inf. comput., 93(1), 93–113.
Martin-Löf, Per. (1984). Intuitionistic type theory. Napoli: Bibliopolis.
The Coq development team. (2015). The coq proof assistant reference manual. LogiCal Project.
Version 8.4.
Mendler, Nax. (1988). Inductive Definition in Type Theory. Ph.D. thesis, Cornell University.
Meyer, Albert R., & Reinhold, Mark B. (1986). ”type” is not a type. Pages 287–295 of: Proceedingsof the 13th acm sigact-sigplan symposium on principles of programming languages (popl). New
York, NY, USA: ACM.
Miquel, Alexandre. (2001). The Implicit Calculus of Constructions Extending Pure Type Systems
with an Intersection Type Binder and Subtyping. Pages 344–359 of: Abramsky, Samson (ed),Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 2044. Springer.
Mogensen, Torben Æ. (1992). Efficient Self-Interpretations in lambda Calculus. J. funct. program.,2(3), 345–363.
Norell, Ulf. 2007 (September). Towards a practical programming language based on dependent typetheory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University ofTechnology, SE-412 96 Göteborg, Sweden.
Parigot, Michel. (1988). Programming with proofs: a second order type theory. Pages 145–159 of:Ganzinger, H. (ed), European Symposium On Programming (ESOP). Lecture Notes in Computer
Science, vol. 300. Springer.
Parigot, Michel. (1989). On the representation of data in lambda-calculus. Pages 309–321 of: Börger,
Egon, Büning, HansKleine, & Richter, Michael (eds), Computer Science Logic (CSL). Lecture
Notes in Computer Science, vol. 440. Springer.
Pfenning, Frank, & Elliott, Conal. (1988). Higher-Order Abstract Syntax. Pages 199–208 of:
Wexelblat, Richard L. (ed), Proceedings of the ACM sigplan’88 conference on programming
language design and implementation (pldi). ACM.
Pfenning, Frank, & Paulin-Mohring, Christine. (1989). Inductively Defined Types in the Calculusof Constructions. Pages 209–228 of: Main, Michael G., Melton, Austin, Mislove, Michael W., &Schmidt, David A. (eds), Mathematical foundations of programming semantics, 5th international
conference.
Pfenning, Frank, & Schürmann, Carsten. (1999). System Description: Twelf - A Meta-Logical
Framework for Deductive Systems. Pages 202–206 of: Ganzinger, Harald (ed), Automateddeduction - cade-16, 16th international conference on automated deduction. Lecture Notes in
Computer Science, vol. 1632. Springer.
Pientka, Brigitte. (2008). A type-theoretic foundation for programming with higher-order abstract
syntax and first-class substitutions. Pages 371–382 of: Necula, George C., & Wadler, Philip(eds), Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on principles of programming
languages (POPL). ACM.
Pierce, Benjamin C., & Turner, David N. (2000). Local type inference. ACM trans. program. lang.
syst., 22(1), 1–44.

ZU064-05-FPR

paper

14 March 2017

20:59

Journal of Functional Programming

39

Polakow, Jeff. (2015). Embedding a Full Linear Lambda Calculus in Haskell. Pages 177–188 of:Proceedings of the 2015 acm sigplan symposium on haskell. ACM.
Poswolsky, Adam, & Schürmann, Carsten. (2009). System Description: Delphin - A Functional
Programming Language for Deductive Systems. Electr. notes theor. comput. sci., 228, 113–120.
Schürmann, Carsten, Despeyroux, Joëlle, & Pfenning, Frank. (2001). Primitive recursion for higherorder abstract syntax. Theor. comput. sci., 266(1-2), 1–57.
Stump, Aaron. (2016). Verified Functional Programming in Agda. ACM Books.
Stump, Aaron, & Fu, Peng. (2016). Efficiency of lambda-encodings in total type theory. Journal offunctional programming, 26(003).
Tannen, Val, & Coquand, Thierry. (1988). Extensional Models for Polymorphism. Theor. comput.
sci., 59, 85–114.
Univalent Foundations Program, The. (2013). Homotopy type theory: Univalent foundations ofmathematics. Institute for Advanced Study: http://homotopytypetheory.org/book.
Washburn, Geoffrey, & Weirich, Stephanie. (2003). Boxes Go Bananas: Encoding Higher-order
Abstract Syntax with Parametric Polymorphism. Pages 249–262 of: Proceedings of the eighthacm sigplan international conference on functional programming (icfp). ACM.
Werner, Benjamin. (1992). A Normalization Proof for an Impredicative Type System with Large
Elimination over Integers. Pages 341–357 of: Proceedings of the 1992 Workshop on Types for
Proofs and Programs.
Werner, Benjamin. (1994). Une Théorie des Constructions Inductives. Ph.D. thesis, Université ParisDiderot - Paris VII.

ZU064-05-FPR

paper

14 March 2017

20:59

40

Stump

X ∈+ X

X 6= YX ∈p YX ∈ p T X 6= Y
X ∈ p ∀Y : κ.T

X ∈ p T 0 X ∈ p T X 6= x
X ∈ p ιx : T 0 .T

X ∈ p̂ T1 X ∈ p T2
X ∈ p Πx : T1 .T2

X ∈ p̂ T1 X ∈ p T2
X ∈ p ∀x : T1 .T2

X ∈p T
X ∈p T t

X ∈p T 0
X ∈ p λ x : T.T 0

X ∈p T

X 6∈ FV(T 0 )X ∈p T T 0
X ∈ p T 0 X 6= Y
X ∈ p λY : κ.T 0

X ∈ p T X ∈ p Θ X ∈ p T X 6= Y
X ∈ p νY ⊆ T : κ | Θ.T

X ∈p UX ∈p ·X ∈p T X ∈p ΘX ∈ p (t ∈ T, Θ)X ∈p ?

X ∈ p̂ T X ∈ p κX ∈ p Πx : T.κ

X 6= Y X ∈ p̂ κ X ∈ p κ 0
X ∈ p ΠY : κ.κ 0

Fig. A 1. Polarity of occurrences of type variables in types, constructor sets, and kinds

A Omitted Rules
In this section are listed some straightforward rules omitted from the definition of CDLE
in the main text.
A.1 Rules defining judgement X ∈ p T
Rules defining judgement X ∈ p T are in Figure A 1. We write p̂ for the other polarity
besides p.
A.2 Additional rules for directed conversion
Figure A 2 gives additional rules for directed conversion. Computation rules were given
in Figure 5. The additional rules include reflexivity, transitivity, and then congruence rules
equating expressions where the corresponding subexpressions are equal. Passing under abinder extends the context, and passing into the body of a ν-type adds the constructor set
to the context (just like the kinding rule for ν-types).

ZU064-05-FPR

paper

14 March 2017

20:59

41

Journal of Functional ProgrammingΓ ` T1 . T2 Γ ` T2 . T3
Γ ` T1 . T3

Γ ` T .T
Γ ` T . T 0 Γ ` t . t0
Γ ` T t . T 0 t0

Γ ` T1 . T10

Γ, X : κ ` T . T 0Γ ` λ X : κ. T . λ X : κ. T 0

Γ ` T1 . T10

Γ ` T1 . T10

Γ, X : κ ` T . T 0
Γ ` ∀ X : κ. T . ∀ X : κ. T

Γ ` T1 T2 . T10 T20Γ ` ∀ X : T1 . T2 . ∀ X : T10 . T2

Γ ` ·.·

Γ, X : T1 ` T2 . T20

Γ ` Π X : T1 . T2 . Π X : T10 . T2

Γ, X : T1 ` T2 . T20

Γ ` L . L0 Γ ` t . t 0Γ ` ↑L t . ↑L0 t

Γ ` T2 . T20

Γ ` L1 . L10

Γ ` L2 . L20

Γ ` L1 → L2 . L10 → L20
Γ ` t . t 0 Γ ` T . T 0 Γ ` Θ . Θ0
Γ ` t ∈ T, Θ . t 0 ∈ T 0 , Θ0Fig. A 2. Additional rules for conversion

Γ ` T1 . T10

Γ `, X : T1 ` T2 . T20

Γ ` λ X : T1 . T2 . λ X : T10 . T20
Γ ` T . T 0 Γ, X : T ` L . L0
Γ ` Π X : T. L . Π X : T 0 . LΓ ` T1 . T10

Γ, X : T1 ` T2 . T20

Γ ` ι X : T1 . T2 . ι X : T10 . T2
Γ, X : κ ` Θ . Θ0 Γ, X : κ, Θ ` T . T 0
Γ ` ν X : κ | Θ. T . ν X : κ | Θ0 . T 0