Modular Type-Safety Proofs using Dependant Types
Christopher Schwaab

Jeremy G. Siek

arXiv:1208.0535v1 [cs.PL] 2 Aug 2012

University of Colorado at Boulder
{schwaab,jeremy.siek}@colorado.edu

Abstract
While methods of code abstraction and reuse are widespread
and well researched, methods of proof abstraction and reuse
are still emerging. We consider the use of dependent types
for this purpose, introducing a completely mechanical approach to proof composition. We show that common techniques for abstracting algorithms over data structures naturally translate to abstractions over proofs. We first introduce
a language composed of a series of smaller language components tied together by standard techniques from Malcom [2].
We proceed by giving proofs of type preservation for each
language component and show that the basic ideas used in
composing the syntactic data structures can be applied to
their semantics as well.

1.

Introduction

The POPLmark challenge is a set of common programming
language problems meant to test the utility of modern proof
assistants and techniques for mechanized metatheory. In response to this challenge, significant strides have been made
in making it easier to mechanize the metatheory of programming languages, especially regarding variable binding [1].
However, little progress has been made in the direction of
modularity: it is still difficult to separately develop the definitions and meta-theory of language fragments and then
link the fragments together to obtain the definitions and
meta-theory for a language composed of such fragments.
Dependent types have formed the foundation of a broad
and rich range of type systems that allow values and types
to be freely mixed. Programmers can express propositions
as types viewed as sets, and proofs as objects viewed as
inhabitants of those sets. This style of theorem proving suggests the use of familiar engineering abstractions as general
solutions to questions about theorem proving. Rather than
relying on semi-automated proof search such as Coq’s Ltac
we propose a method of proof composition using simple abstractions whereby components are defined piecewise and
“tied” together at the end using a wrapper datatype acting
as a tagged union.
The method of language definition used is iterative. Components are defined separately from one another and are
composable along with their proofs. Thus we would like for

[Copyright notice will appear here once ’preprint’ option is removed.]

1

separate language designers to be able to reuse one anothers’ work without the need for sophisticated proof search
algorithms or with effort spent copying and pasting terms.
The language we present is one of simple expressons using
Agda as the implementation language and proof assistant.
We begin by defining a series of language syntaxes for sums,
options, and arrays. We chose to include arrays because they
not only can result in runtime errors requiring the inclusion
of the Option type but like addition, they use the natural
numbers, forcing consideration of how value types can be
shared across otherwise isolated components. We continue
by defining evaluation semantics and typing rules. The language is defined piecewise, each component is built in isolation alongside a proof of type preservation. We conclude
with a presentation of how these components can be composed and a proof of type preservation for the combined
language can be immediately derived from the componentwise proofs. The motivation for our technique is drawn from
a solution to the expression problem where languages are
defined as the disjoint sum of smaller languages by removing explicit recursion. We show that this idea can be recast
from types and terms, to proofs.

2.

A Review of the Expression Problem

When modeling a problem with a functional flavor often the
natural solution emerges as several recursive cases handled
by some helper functions. The expression problem states
that this type of solution presents us with a choice: we may
ordain our data structure forever unchanging, making it easy
to add new functions without changing the program; or we
may leave our data structure open, making it difficult to
extend the original program with new functions.
While many solutions to the expression problem have
been proposed over the years, here we make use of the
method described by Malcom [2] which generalizes recursion
operators such as fold, from lists to polynomial types. The
problem we encounter arises as a result of algebraic data
types being closed : once the type has been declared, no new
constructors for the type may be added without amending
the original declaration and the solution presented lies at the
heart of our work. The idea is simply to remove immediate
recursion and split a monolithic datatype into components
to be later collected under the umbrella of a tagged union.
Throughout this paper we will work with a simple evaluator over natural numbers and basic arithmetic operators;
in Agda we might first consider
data Expr+ : Set where
atom : N → Expr+
_+_ : Expr+ → Expr+ → Expr+
2018/1/21

This definition has the advantage of being direct and simple,
however a problem lies within the explicit recursion; notice
that when later extending expressions with arrays and option types we can make no reuse of Expr+ due to the closed
nature of algebraic data types. To extend Expr+ we must
define a whole new data type, as in the following definition
of MonolithicExpr.
data MonolithicExpr : Set where
atom : N → MonolithicExpr
esome : MonolithicExpr → MonolithicExpr
enone : MonolithicExpr
nil [ ] : MonolithicExpr
_!!_ : MonolithicExpr → MonolithicExpr
→ MonolithicExpr
[ ] :=_ : MonolithicExpr → MonolithicExpr
→ MonolithicExpr → MonolithicExpr
_+_ : MonolithicExpr → MonolithicExpr
→ MonolithicExpr
fromExpr+ : Expr+ → MonolithicExpr
fromExpr+ (atom n) = atom n
fromExpr+ (n + m) = fromExpr+ n + fromExpr+ m

It is easy to see that this new type is equivalent to
MonolithicExpr up to isomorphism
Expr = µ Expr ′
= Expr ′ (µ Expr ′ )
= Expr ′ Expr
∼
= atom
| esome | enone
| Expr + Expr
| nil[] | −!! − | − [−] := −

2.1

Functors and Agda

The functor F , passed into µ− above, serves as the key
abstraction allowing us to represent expressions as least fixed
points. Functors are a special mapping defined over both
types and functions satisfying the so called functor laws; a
functor F
1. assigns to each type A, a type F A
2. assigns to each function f : A → B, a function map f :
FA → FB

Suppose instead we begin with polymorphic definitions such
as the following.

such that
1. identity is preserved: map id = id, and
2. when f ◦ g is defined: map (f ◦ g) = map f ◦ map g.
One familiar example is the List functor mapping each type
A to List A and each function f : A → B to map f :
List A → List B which applies f to each element of a
list. Here we define the least fixed point over a restricted
class of functors called the polynomial functors. Polynomial
functors are a subset roughly equivalent to the more familiar
algebraic polynomials,
X
An X n

data Expr+2 (A : Set) : Set where
_+_ : A → A → Expr+2 A
data Expr [ ] 2 (A : Set) : Set where
nil [ ] : Expr [ ] 2 A
_!!_ : Expr [ ] 2 A
[ ] :=_ : A → A → A → Expr [ ] 2 A
data ExprOption (A : Set) : Set where
esome : N → ExprOption A
enone : N → ExprOption A
data Lit (A : Set) : Set where
atom : N → Lit A

n∈N⊆N

where addition is disjoint sum and multiplication is cartesian
product. In Agda, Ulf Norell[4] expresses this class as a
datatype F unctor along with an interpretation as a set [−]

We then introduce recursion as follows, combining components as a disjoint sum, written − ⊎ − in Agda.
data RecExpr : Set where
expr : Lit RecExpr
⊎ Expr+2 RecExpr
⊎ Expr [ ] 2 RecExpr
⊎ ExprOption RecExpr
→ RecExpr
More generally, this type of data can be captured using a
“categorical approach” where recursion is introduced as the
fixed point of a functor:

infixl 6 _⊕_
infixr 7 _⊗_
data Functor : Set1 where
X : Functor
A : Set → Functor
_⊕_ : Functor → Functor → Functor
_⊗_ : Functor → Functor → Functor
[ ] : Functor → Set → Set
[X] B = B
[A C] B = C
[F ⊕ G] B = [F] B ⊎ [G ] B
[F ⊗ G] B = [F] B × [G] B
with least fixed point
data µ_ (F : Functor) : Set where
inn : [F] (µ F) → µ F

data µ_ (F : Set → Set) : Set where
inn : F (µ F) → µ F
Expr’ = λ (A : Set) → Lit A ⊎ Expr+2 A
⊎ Expr [ ] 2 A
⊎ ExprOption A
Expr = µ Expr’

Then to reexpress Expr as a polynomial functor we use sum
− ⊕ − to define cases within a type, and product − ⊗ − to
represent arguments of a particular case
Option1 : Functor
Option1 = X ⊕ A ⊤
2

2018/1/21

Array1 : Functor
Array1 = X ⊕ X ⊕ X ⊕ A ⊤ ⊕ X ⊕ X
Sum1 : Functor
Sum1 = X ⊗ X
F1 : Functor
F1 = A N ⊕ Option1 ⊕ Sum1 ⊕ Array1
E1 : Set
E1 = µ F1

Expr : Set
Expr = µ FExpr
What do each of these definitions mean? The maybe type
has two constructors: some, which wraps a single expression;
and none taking no arguments. We define more descriptive
constructors for tagging these two types of values

Unfolding E1 yields the same value calculated above—as we
should hope!
E1 = µ F1
= [A N ⊕ Option1 ⊕ Sum1 ⊕ Array1 ]
= [A N] (µ F1 )
⊎ [Option1 ] (µ F1 )
⊎ [Sum1 ] (µ F1 )
⊎ [Array1 ] (µ F1 )
= N
⊎ (µ F1 ) × ⊤
⊎ (µ F1 ) × (µ F1 )
⊎ (µ F1 ) × (µ F1 ) ⊎ (µ F1 ) ⊎ ⊤ ⊎ (µ F1 ) ⊎ (µ F1 )

: Expr
= inn (inj1 (inj1 (inj2 (inj2 tt))))
: Expr → Expr
= inn ◦ inj1 ◦ inj1 ◦ inj2 ◦ inj1

Giving a convenient constructor for − + − is similarly
straightforward
enat : N → Expr
enat = inn ◦ inj1 ◦ inj1 ◦ inj1
_∔_ : Expr → Expr → Expr
e1 ∔ e2 = inn (inj1 (inj2 (e1 , e2 )))
and to define arrays we have assignment taking an array, an
index, and a value to assign at that index; nil, the empty
array; and lookup which accepts an array and an index

What do values in E1 look like? Written directly they appear
nonsensical, consider 6 + 7
the-sum : E1
the-sum = inn (inj1 (inj2 (
(inn (inj1 (inj1 (inj1 6))))
, (inn (inj1 (inj1 (inj1 7)))))))
Notice here the role that the injections and inn functions
play. Traditionally we would provide a unique name for each
branch in an algebraic datatype, however here we only have
two names inj1 and inj2 so we instead rely on nesting to
create unique prefixes. Once we have tagged a value we must
give it a well known type so that parent expressions can
expect a common child type, this is the role of inn. Although
cumbersome we can hide much of this complexity provided
the right abstractions
the-sum’ : E1
the-sum’ = nat1 6 +1 nat1 7
where nat1 : N → E1
nat1 = inn ◦ inj1 ◦ inj1 ◦ inj1
_+1 _ : E1 → E1 → E1
e1 +1 e2 = inn (inj1 (inj2 (e1 , e2 )))

3.

none1
none1
some1
some1

Syntax and Evaluation Semantics

We are now ready to define a simple language and its
operational semantics. The language is small including just
sums, an option type, and an array with assignment and
lookup. In Agda, the unit type is written ⊤ and has only
one member: tt. ⊤ is used to represent constructors that
take no arguments such as nil, the empty list.
Option : Functor
Option = X ⊕ A ⊤
Array : Functor
Array = X ⊗ X ⊗ X ⊕ A ⊤ ⊕ X ⊗ X
Sum : Functor
Sum = X ⊗ X
FExpr : Functor
FExpr = A N ⊕ Option ⊕ Sum ⊕ Array
3

[ ] :=1 _ : Expr → Expr → Expr → Expr
a [i] :=1 e = inn (inj2 (inj1 (inj1 (a, i, e))))
nil1 : Expr
nil1 = inn (inj2 (inj1 (inj2 tt)))
_!1 _ : Expr → Expr → Expr
a !1 i = inn (inj2 (inj2 (a, i)))
So far the definition of our syntax has used fairly standard
techniques but we have failed to give any sort of meaning to
these expressions. We first define a monolithic static and
dynamic semantics for this language, then show how to
modularize their definition later in this section. Figure 1c
defines a simple set of typing rules using metavariables e to
range over experssions and n to range over values; Figure 1b
gives a small step operational semantics.
While Agda is expressive enough to implement these
rules, directly and indeed they are nearly a direct reflection of that implementation, recall that our goal is to create several independant languages each carrying their own
semantics. We begin by defining monolithic semantics for
Expr and proceed to determine points of failure and to dissect the definition into independant constituents. To simplify
things we define our notion of T ype as a closed ADT
data Type : Set where
TArray : Type
TOption : Type
TNat : Type
and here is the definition of the monolithic type system and
evaluation relation in Agda.
data Welltyped : Expr → Type → Set1 where
ok-value : {n : N} → Welltyped (enat n) TNat
ok-sum : {e1 e2 : Expr}
→ Welltyped e1 TNat → Welltyped e2 TNat
→ Welltyped (e1 ∔ e2 ) TNat
ok-nil : Welltyped nil1 TArray
ok-lookup : {a e : Expr}
→ Welltyped a TArray
→ Welltyped e TNat
→ Welltyped (a !1 e) TOption
ok-ins : {a e n : Expr}
→ Welltyped a TArray
2018/1/21

− ∔ − ∈ Expr → Expr → Expr
n ∈ N ∈ Expr
−[−] := − ∈ Expr → Expr → Expr → Expr
−!− ∈ Expr → Expr → Expr
nil ∈ Expr

(stepl+)

e1 −→ e′1
e1 +̇e2 −→ e′1 +̇e2

(stepr+)

e2 −→ e′2
n1 +̇e2 −→ n1 +̇e′2

(sum)

(a) Syntax

n1 +̇n2 −→ n1 + n2

(stepi)

(lookup)

e −→ e′
a!e −→ a!e′

a!n −→ LJa, nK

(b) Evaluation Semantics

(ok-value)

e1 : N at
e2 : N at
e1 +̇e2 : N at

(ok-sum)

n : N at

(c) Value Typing

(d) Sum Typing

(ok-nil)

(ok-lookup)

(ok-ins)

nil : Array

a : Array
e : N at
a!e : Option

a : Array
n : N at
e : N at
a[n] := e : Array
(e) Array Typing

Notice that we currently do not restrict the values of n
enough in the ok-ins rule; our typing rules require that n
be a value while in Agda we have only required it be an
expression. Some notion of value is needed and a common
solution is to add a tag Value to the Expr type and pattern
match; here Value is called [AN] and in a dependantly
typed context we might then define a predicate over Value.
However because the sum type has only one type of value,
a number, it is simpler to use enat directly.
This method for defining semantics is common with the
advantage of being direct and concise, but similar to our
first implementation of Expr + and MonolithicExpr above:
there is no simple mechanism for code reuse. The answer is
again to delay recursion.

→ Welltyped e TNat
→ Welltyped n TNat
→ Welltyped (a [n] :=1 e) TArray
infix 2 _−→E_
data _−→E_ : Expr → Expr → Set where
stepl : {e1 e1 ’ e2 : Expr}
→ e1 −→E e1 ’
→ e1 ∔ e2 −→E e1 ’ ∔ e2
stepr : {n1 : N} {e2 e2 ’ : Expr}
→ e2 −→E e2 ’
→ enat n1 ∔ e2 −→E enat n1 ∔ e2 ’
sum : {n1 n2 : N}
→ enat n1 ∔ enat n2 −→E enat (n1 +N n2 )
stepi : {e e’ a : Expr}
→ e −→E e’
→ a !1 e −→E a !1 e’
lookup : {a n : Expr}
→ a !1 n −→E LJ a, n K1

3.1

The function LJ−, −K1 is the lookup function that evaluates
to some an when an has been defined and none otherwise.
4

Dissecting the Step Relation

In order to modularize the evaluation rules we define a
separate step relation for each functor making up our Expr
type. First note that −+̇− doesn’t make use of how the step
from e1 to e2 occurs so we can factor this top-level relation
2018/1/21

data _−→+ _ {_−→_ : Expr → Expr → Set}
: Expr → Expr → Set where
stepl : {e1 e1 ’ e2 : Expr}
→ e1 −→ e1 ’ → e1 ∔ e2 −→+ e1 ’ ∔ e2
stepr : {n1 : N} {e2 e2 ’ : Expr}
→ e2 −→ e2 ’
→ enat n1 ∔ e2 −→+ enat n1 ∔ e2 ’
sum : {n1 n2 : N}
→ enat n1 ∔ enat n2 −→+ enat (n1 +N n2 )

→ F Contains F
left : {A B F : Functor}
→ F Contains A ⊕ B → F Contains A
right : {A B F : Functor}
→ F Contains A ⊕ B → F Contains B
Now we can define containment on a functor’s interpretation
as a set

While this is better there is still an undesirable reference
to the datatype Expr. Applying the same factorization
here to the underlying functor requires parametrization by
two extra coercion functions, these are the −+̇− and enat
functions defined previously. The new names lif t+ and lif tN
used here are meant to imply that a subtype is being “lifted”
into its supertype
data _−→+ _ {E : Functor} {_−→_ : µ E → µ E → Set}
{lift+ : [Sum] (µ E) → µ E} {liftN : N → µ E}
: µ E → µ E → Set where
stepl : {e1 e1 ’ e2 : µ E}
→ e1 −→ e1 ’ → lift+ (e1 , e2 ) −→+ lift+ (e1 ’, e2 )
stepr : {n1 : N} {e2 e2 ’ : µ E}
→ e2 −→ e2 ’
→ lift+ (liftN n1 , e2 ) −→+ lift+ (liftN n1 , e2 ’)
sum : {n1 n2 : N}
→ lift+ (liftN n1 , liftN n2 ) −→+ liftN (n1 +N n2 )
Unfortunately this definition falls short too. When we lift
terms into the expression type µE, Agda “forgets” the constituents e1 and e2 —in turn we lose the ability to reason
about these distinct components of the sums en and e′n . This
later becomes a problem when, for example, attempting to
abstract the welltyping relation.
An intelligent human can peel away lif t+ and see that
the terms e1 and e2 in − −→ − and − −→+ − are the same
because lif t+ is injective. However Agda is unconvinced,
and rightfully so, for it does not require a particularly great
deal of ingenuity to find a counterexample, consider taking
E = FExpr so that µE = Expr

infix 3 _֌_
data _֌_ : Set → Set → Set1 where
inj : {F A : Functor}
→ F Contains A → [A] (µ F) ֌ (µ F)
with conversion functions defined as
upcast : ∀ {F A} → F Contains A → [A] (µ F) → µ F
upcast refl = inn
upcast (left t) = upcast t ◦ inj1
upcast (right t) = upcast t ◦ inj2
apply : {A B : Set} → (A ֌ B) → A → B
apply (inj t) = upcast t
Recall the two goals we had in mind. We first wished to take
the inverse of a lift function to gain access to its arguments,
in the case of −+− these were e1 and e2 . By representing an
injection as a delayed application of a subobject—because
the constructor’s arguments are stored as a part of the
coercion—finding left inverses will become a trivial case of
pattern matching. To delay function application allowing
Agda to effectively peel away the lif t functions we define
a LazyCoercion datatype from type A to B representing the
intention of coercing an object a ∈ A while treating it at the
type-level as B. A lazy coercion is then an injection A ֌ B
along with an object in A
data LazyCoercion : Set → Set1 where
inj : {A B : Set} → (A ֌ B) → A → LazyCoercion B
coerce : {B : Set} → LazyCoercion B → B
coerce (inj f e) = apply f e

The problem is that our abstraction is too general. What
we require is a proof that [Sum](µE) and N are subtypes
of the top-level expression datatype µE. The solution to the
problem is drawn from the notion of a categorical subobject.
We proceed by delaying application of injections and view
the objects as injectable, existential terms. The importance
of this approach is two-fold: firstly this allows us to take
inverses of lift functions while we are secondly able to retain
the perspective of operating on a single type µE.

Our second goal was to operate on objects of a single type.
Why is this the case? Recall that the type of our step relation
is indexed by two expressions: (e1 : Expr ) −→E (e2 : Expr ).
We should expect the same of the final abstraction over step
relations because it cannot easily name the underlying type
of its indexing expressions. Instead we have packaged the
indices as existentials which are viewed as the type B.
We seem to be close to a modular step relation − −→+ −,
defining at each point another level of abstraction to delay
immediate application. To modularize datatypes, recursion
is delayed and types are viewed as polynomial functors,
then to modularize step relations, evaluation is parametrized
and expression upcasts are delayed by viewing them as an
intention.

4.

5.

forgetful-lift+ : [Sum] Expr → Expr
forgetful-lift+ (e1 , e2 ) = enat 0

Lazy Coercions

A subobject of a type T is a left invertible function with
codomain T , lift : S ֒→ T . Being restricted to polynomial
functors, we know that all our subobjects lift : S → µE will
be some composition of inn, inj1 and inj2 so a proof that S
is a subtype of µE is merely a description of which direction
to move at each point in a disjoin sum
infix 3 _Contains_
data _Contains_ : Functor → Functor → Set1 where
refl : {F : Functor}
5

Defining a Modular Step Relation

Attempting again to define a step relation for addition we
find very little has changed
data _−→+ _ {E : Functor}
{_−→_ : µ E → µ E → Set1 }
{lift+ : [Sum] (µ E) ֌ µ E}
{liftN : N ֌ µ E}
: LazyCoercion (µ E) → LazyCoercion (µ E) → Set1
where
stepl : {e1 e1 ’ e2 : µ E}
2018/1/21

6.

→ e1 −→ e1 ’
→ inj lift+ (e1 , e2 ) −→+ inj lift+ (e1 ’, e2 )
stepr : {e1 e2 e2 ’ : µ E}
→ e2 −→ e2 ’
→ inj lift+ (e1 , e2 ) −→+ inj lift+ (e1 , e2 ’)
stepv : {n m : N}
→ inj lift+ (apply liftN n, apply liftN m)
−→+ inj liftN (n +N m)

The type preservation lemma states that if a term is welltyped and can step, then the type of the term is preserved
after evaluation
e −→ e′ ∧ e : T ⇒ e′ : T

It appears we’ve littered an otherwise simple definition with
inj but we’ve replaced our arbitrary arrows with objects
having constructors we can match on. Using the above
techniques we can modularize the welltyping relation over
sums for free
data WtSum {E : Functor}
{Wt : µ E → Type → Set1 }
{lift+ : [Sum] (µ E) ֌ µ E}
: LazyCoercion (µ E) → Type → Set1 where
ok-sum : {e1 e2 : µ E}
→ Wt e1 TNat → Wt e2 TNat
→ WtSum (inj lift+ (e1 , e2 )) TNat
The above definitions nearly wrote themselves. The simplicity comes from the fact we are just abstracting as many
terms as possible, keeping in mind we can fill them in naturally later because the abstraction is so general there are
few options available.
5.1

Proving Type Preservation

Arrays

We proceed by defining the step and welltypedness relations
on arrays that can be combined with the relations on sums.
The definitions for evaluation and welltypedness should look
similar to those for sums − −→+ −.
data _−→ [ ] {E : Functor}
{_−→_ : µ E → µ E → Set1 }
{liftA : [Array ] (µ E) ֌ µ E}
{liftN : N ֌ µ E}
{liftO : [Option] (µ E) ֌ µ E}
: LazyCoercion (µ E) → LazyCoercion (µ E) → Set1
where
stepi : {e e’ a : µ E} → e −→ e’
→ inj liftA (a ! e) −→ [ ] inj liftA (a ! e’)
lookup : {a : [Array ] (µ E)} {n : N}
→ inj liftA (apply liftA a ! apply liftN n)
−→ [ ] inj liftO LJ a, n K
To define the typing relation we again follow the format of
WtSum above and we are done.
data WtArray {E : Functor}
{Wt : µ E → Type → Set1 }
{liftA : [Array ] (µ E) ֌ (µ E)}
{liftN : N ֌ µ E}
: LazyCoercion (µ E) → Type → Set1 where
ok-nil : WtArray (inj liftA nil) TArray
ok-ins : {a e n : µ E}
→ Wt a TArray → Wt e TNat → Wt n TNat
→ WtArray (inj liftA (a [n] := e)) TArray
ok-lookup : {e a : µ E}
→ Wt a TArray → Wt e TNat
→ WtArray (inj liftA (a ! e)) TOption

(type-preservation)

Prior to considering how type preservation might look for
each of the previously defined components we should review
what type preservation looks like for the MonolithicExpr
language. The proof is standard, proceeding by structural
induction on the shape of the welltyping tree.
preservation-MonolithicExpr : ∀ {e e’} {τ }
→ e −→C e’
→ WtMonolithicExpr e τ
→ WtMonolithicExpr e’ τ
preservation-MonolithicExpr (stepl ste1 ) (ok-sum wte1 wte2 )
= ok-sum (preservation-MonolithicExpr ste1 wte1 ) wte2
preservation-MonolithicExpr (stepr ste2 ) (ok-sum wte1 wte2 )
= ok-sum wte1 (preservation-MonolithicExpr ste2 wte2 )
preservation-MonolithicExpr
(stepv {n} {m}) (ok-sum wtn wtm)
= ok-nat (n +N m)
preservation-MonolithicExpr (stepi ste) (ok-lookup wta wte)
= ok-lookup wta (preservation-MonolithicExpr ste wte)
preservation-MonolithicExpr
(lookup {a} {n}) (ok-lookup wta wtn)
= proj2 LCJ a, n K
There are three items worth noting here: the first is the
use of the function LCJ−, −K : MonolithicExpr → N →
∃e.WtMonolithicExpr e TOption which we have assumed
produces a pair with first component an expression and
second component a proof that the expression is a welltyped
option; the second is that recursion acts as our induction
hypothesis; and finally that Agda is smart enough to notice
there is only a single possible welltyping constructor for each
step constructor—in Agda all functions are total.
We should expect the modular type preservation lemmas
to look similar because there is little global knowledge involved. The induction hypothesis and values aside, each case
is “contained within its own world” in the sense that each
evaluation rule relies only on the fact that subterms are welltyped but ignoring the reason they are welltyped. To show
type preservation for sums we might start with
preservation-Sum1 : {τ : Type} {E : Functor}
{e e’ : LazyCoercion (µ E)}
→ e −→+ e’
→ WtSum e τ
→ WtSum e’ τ
preservation-Sum1
(stepl {e1 } {e1 ’} {e2 } ste1 ) (ok-sum wte1 wte2 ) = *
however recall that − −→+ − requires the top-level step
relation and proof that E contains both sums and naturals.
There is a second mistake in writing preservation this way—
we would like to show that e′ is welltyped in the expression
language, not just necessarily in the modular sum language,
this reflects our desire to expose as little about each component as possible. A second formulation might then begin as
follows but we again fail.
preservation-Sum2 : {τ : Type}
{E : Functor}
{_−→_ : µ E → µ E → Set1 }

6

2018/1/21

{lift+ : [Sum] (µ E) ֌ µ E}
{liftN : N ֌ µ E}
{Wt : µ E → Type → Set1 }
{e e’ : LazyCoercion (µ E)}
→ _−→+ _ {E} {_−→_} {lift+ } {liftN } e e’
→ WtSum {E} {Wt} {lift+ } e τ
→ Wt (coerce e’) τ
preservation-Sum2 (stepl ste1 ) (ok-sum wte1 wte2 )
= * (ok-sum * wte2 )
preservation-Sum2 (stepr ste1 ) (ok-sum wte1 wte2 )
= * (ok-sum wte1 *)
preservation-Sum2 stepv (ok-sum wte1 wte2 )
= * (n +N m)

→ WtArray {E} {Wt} {liftA } {liftN } (inj liftA e) δ
→ Wt (apply liftA e) δ)
→ (∀ {δ } {e e’} → e −→ e’ → Wt e δ → Wt e’ δ)
→ _−→ [ ] {E} {_−→_} {liftA } {liftN } {liftO } a b
→ WtArray {E } {Wt} {liftA } {liftN } a τ
→ Wt (coerce b) τ
preservation-Array wtopt wt IH
(stepi ste) (ok-lookup wta wte)
= wt (ok-lookup wta (IH ste wte))
preservation-Array wtopt wt IH
(lookup {a} {n}) (ok-lookup wta wte)
= wtopt LJ a, n K

It seems we’re only missing two pieces: we need to be able to
lift welltyped sums and naturals into Wt ; and we need some
way of expressing the induction hypothesis which states that
because e1 is welltyped and stepped, e′1 is welltyped too.
The induction hypothesis is slightly stranger than was the
case in our MonolithicExpr ’s because we know e1 and e′1
are welltyped despite the fact that they are any expressions,
not necessarily just sums. This motivates our solution which
takes the induction hypothesis as an explicit assumption.
preservation-Sum : {τ : Type}
{E : Functor}
{_−→_ : µ E → µ E → Set1 }
{lift+ : [Sum] (µ E) ֌ µ E}
{liftN : N ֌ µ E}
{Wt : µ E → Type → Set1 }
{a b : LazyCoercion (µ E)}
→ ((n : N) → Wt (apply liftN n) TNat)
→ (∀ {δ } {e }
→ WtSum {E} {Wt} {lift+ } (inj lift+ e) δ
→ Wt (apply lift+ e) δ)
→ (∀ {δ } {e e’} → e −→ e’ → Wt e δ → Wt e’ δ)
→ _−→+ _ {E} {_−→_} {lift+ } {liftN } a b
→ WtSum {E} {Wt} {lift+ } a τ
→ Wt (coerce b) τ
preservation-Sum wtnat wt IH
(stepl ste1 ) (ok-sum wte1 wte2 )
= wt (ok-sum (IH ste1 wte1 ) wte2 )
preservation-Sum wtnat wt IH
(stepr ste2 ) (ok-sum wte1 wte2 )
= wt (ok-sum wte1 (IH ste2 wte2 ))
preservation-Sum wtnat wt IH
(stepv {n} {m}) (ok-sum wte1 wte2 )
= wtnat (n +N m)

It would seem we’re nearly done and the final pieces should
be entirely guided by the selected abstractions. The lift
functions each have a unique solution:
lift+
lift+
liftN
liftN
liftO
liftO
liftA
liftA

: [Sum] Expr ֌ Expr
= inj (right (left (refl)))
: N ֌ Expr
= inj (left (left (left refl)))
: [Option] Expr ֌ Expr
= inj (right (left (left refl)))
: [Array ] Expr ֌ Expr
= inj (right refl)

But how should we define welltypedness for Expr ? Again the
notion of what it means to be welltyped has already been
defined and we simply need to “tie the knot” as RecExpr did
above
data WtExpr : Expr → Type → Set1 where
lift-wt-nat : (n : N) → WtExpr (apply liftN n) TNat
lift-wt-option : (m : [Option] Expr)
→ WtExpr (apply liftO m) TOption
lift-wt-sum : {τ : Type} {e : [Sum] Expr}
→ WtSum {FExpr } {WtExpr} {lift+ } (inj lift+ e) τ
→ WtExpr (apply lift+ e) τ
lift-wt-array : {τ : Type} {e : [Array ] Expr}
→ WtArray {FExpr} {WtExpr} {liftA } {liftN }
(inj liftA e) τ
→ WtExpr (apply liftA e) τ
To define a step relation on Expr , − −→ − we provide a
similar wrapping for each language component

We are pleased with how similar this is to the original,
monolithic formulation. Notice again that the solution was
to factor out assumptions about the outside world similar
to the previous abstractions. Proving type preservation for
arrays is similarly natural:
preservation-Array : {τ : Type}
{E : Functor}
{_−→_ : µ E → µ E → Set1 }
{liftA : [Array ] (µ E) ֌ (µ E)}
{liftN : N ֌ µ E}
{liftO : [Option] (µ E) ֌ (µ E)}
{Wt : µ E → Type → Set1 }
{a b : LazyCoercion (µ E)}
→ ((m : [Option] (µ E)) → Wt (apply liftO m) TOption)
→ (∀ {δ } {e }
7

data _−→_ : Expr → Expr → Set1 where
step+ : {e : [Sum] Expr} {e’ : LazyCoercion Expr}
→ _−→+ _ {FExpr} {_−→_} {lift+ } {liftN }
(inj lift+ e) e’
→ apply lift+ e −→ coerce e’
step [ ] : {e : [Array ] Expr} {e’ : LazyCoercion Expr}
→ _−→ [ ]
{FExpr} {_−→_} {liftA } {liftN } {liftO }
(inj liftA e) e’
→ apply liftA e −→ coerce e’
The only piece remaining is to prove type preservation. We
begin in the same way we have for each of the previous proofs
using the step relation’s constructors as a guide. The type
signature should not have changed
preservation : {e e’ : Expr} {τ : Type}
→ e −→ e’ → WtExpr e τ → WtExpr e’ τ
and there are two cases step+ and step[]; moreover we
should expect to merely apply preservation-* to each case,
2018/1/21

supplying the necessary lift functions and the induction
hypothesis. This is indeed the case:
preservation (step+ ste) (lift-wt-sum wts)
= preservation-Sum lift-wt-nat lift-wt-sum
preservation ste wts
preservation (step [ ] ste) (lift-wt-array wta)
= preservation-Array lift-wt-option lift-wt-array
preservation ste wta
Having shown type preservation it is interesting to see the
similarity between how terms are shown to be welltyped and
to evaluate and how the terms are expressed in µFExpr .
Recall that each term in Expr is wrapped by a tag—given
by inj1 and inj2 —and the constructor inn plays the role of
recursion. To reiterate consider the convenience functions,

7.

Related Work

Independent and concurrently with our work, Delaware, et
al. [7] developed a solution to moduler meta-theory in Coq.
Both their approach and ours relies on the principle of representing data types as functors; however they have chosen to
express inductive types using Church encodings and recursive evaluation using Mendler algebras, which requires some
extra sophistication. Here we express types as data members of the family of polynomial functors and apply recursive evaluation directly. Their approach presented is further
along and has shown the important level of robustness required by most languages while there are more unanswered
questions regarding the method presented here.

8.

Conclusion and Future Work

We should ask if we have accomplished the goal that we
set out with. The language Expr was given componentwise
and the boiler-plate necessary to wrap each welltyping and
step relation is minimal. The proof of type preservation was
almost immediate, requiring only an invocation of previously
defined proofs for each component. Moreover there is no
copy and paste necessary and the repetitive components
should be automatically producable given a sophisticated
macro system where terms can be inspected by name—set
equality is non-deterministic—rather than value.
Using Agda as a proof language, although convenient,
leaves the question of consistency open. We regard this as
a minor problem and hope that our implementation would
port to Coq. A more pertinent problem is the definition of
preservation for Expr —Agda is unable to prove termination
and we plan to address this soon.
The language presented is quite simple, unable to express
even Euclid’s algorithm, and the method of polynomial
functor’s used to express Expr precludes the possibility of
first class function types which are critical for functional
programming. Various solutions to this problem have been
proposed [5] and the area of recursion schemes is rich [6].
A real world language calls for much heavier sophistication,
but the ideas presented here are new and their reach is open
to question and requires further exploration.

nilE : Expr
nilE = inn (inj2 (inj1 (inj2 tt)))
nat : N → Expr
nat n = inn (inj1 (inj1 (inj1 n)))
[ ] =_ : Expr → Expr → Expr → Expr
a [n] = e = apply liftA (a [n] := e)
_!E_ : Expr → Expr → Expr
a !E n = apply liftA (a ! n)
_+E_ : Expr → Expr → Expr
e1 +E e2 = apply lift+ (e1 , e2 )
we may then ask: why is the term
exp : Expr
exp = (nilE [nat 0] = nat 1) !E (nat 0 +E nat 1)
welltyped? The answer given by W tExpr is
wt-exp : WtExpr exp TOption
wt-exp = lift-wt-array (ok-lookup wta wt+)
where
wta : WtExpr (nilE [nat 0] = nat 1) TArray
wta = lift-wt-array
(ok-ins (lift-wt-array ok-nil)
(lift-wt-nat 1) (lift-wt-nat 0))
wt+ : WtExpr (nat 0 +E nat 1) TNat
wt+ = lift-wt-sum (ok-sum
(lift-wt-nat 0) (lift-wt-nat 1))

References

The lift−wt−∗ functions play the same role in WtExpr as
inn does in Expr ; however rather than using the generalized
approach of a series of disjoint sums we bundle the tag
and recursion into a single constructor for each language
component. Evaluation displays a similar symmetry

[1] Aydemir, et al. Mechanized Metatheory for the Masses: The
PoplMark Challenge. In International Conference on Theorem
Proving in Higher Order Logics (TPHOLs), August 2005.
[2] Grant Malcom. Algebraic data types and program transformations. Ph.D. thesis, Department of Computing Science,
Groningen University, 1990.
[3] Luc Duponcheel. Using catamorphisms, subyptes and monad
transformers for writing modular functional interpreters.
Utrecht University, 1995.

eval-expr : (nilE [nat 0] = nat 1) !E (nat 0 +E nat 1)
−→ (nilE [nat 0] = nat 1) !E nat 1
eval-expr = step [ ] (stepi (step+ stepv))
What does the proof that (nilE [nat 0] = nat 1) !E nat 1 is
welltyped look like? We can compute it by invoking
preservation eval-expr wt-exp
which evaluates to

[4] Ulf Norell. Dependently Typed Programming in Agda. In Proceedings of the 4th international workshop on Types in language design and implementation (TLDI ’09). ACM, New
York, NY, USA, 1-2.
[5] Erik Meijer and Graham Hutton. Bananas in Space: Extending Fold and Unfold to Exponential Types. In Proceedings of
the seventh international conference on Functional programming languages and computer architecture (FPCA ’95). ACM,
New York, NY, USA, 324-333.

lift-wt-array
(ok-lookup
[6] Tarmo Uustalu, et al. Recursion Schemes from Comonads.
(lift-wt-array
Nordic J. of Computing 8, 3 (September 2001), 366-390.
(ok-ins (lift-wt-array ok-nil) (lift-wt-nat 1) (lift-wt-nat 0)))
[7] Benjamin Delaware, Bruno C. d. S. Oliveira, Tom Schrijvers.
(lift-wt-nat 1))

Meta-Theory à la Carte, unpublished manuscript, July, 2012.

8

2018/1/21

