Last time I talked about the background on defining structurally recursive functions in Type Theory and why you might want it. The key point is that structural recursion is driven by the data that is being analysed, as opposed to just doing its own thing with a side-proof that it always terminates.
The goal here is to come up with a self-contained and syntax-free
definition of a dependently-typed structural recursion principle for a
type A
. To start with, this will be purely for normal structural
recursion over inductively defined types. In future posts I will
extend this to other types by combining existing structural induction
principles.
In this post I'll cover how to present structural recursion and
induction in a generic way. The first is probably well known to most
people reading this, being just the standard stuff about initial
F
-algebras, but hopefully the second will be new.
The generic approach to structural induction I'll describe below underlies how Epigram 2 and my own language Foveran implement structural induction in a generic way. More information on Epigram's representation of data types is available in the paper The Gentle Art of Levitation.
My last post led to a very interesting discussion on
reddit,
which quickly left the measly content of my original behind. Just to
clarify some of the points that came up in that discussion, I am only
talking here about structural recursion/induction over inductively
defined types---by which I mean types that arise as initial fixpoints
of F
-algebras---not co-inductive types (though the general technique
for handling structural induction I'll describe below does extend to
co-induction, at least in a categorical setting).
Structural recursion is often presented as a restriction. In Coq or Agda, the programmer enters a recursive definition, and the system inspects it to make sure it fits the template of acceptable definitions. This "generate and test" approach naturally leads most people to think that the system is just being stupid when it refuses to accept their definition.
An alternative is for the system to be up-front about the definitions it is prepared to accept. Instead of writing recursive definitions and having them rejected, the programmer uses special-purpose recursion combinators to write their programs. This is the basic idea behind recursion schemes, as in the classic paper Functional Programming with Bananas, Lenses and Barbed Wire. An important extra benefit of using recursion schemes, as pointed out in that paper, is that they often also come with reasoning principles.
I am interested in going beyond normal recursion schemes, and doing dependent recursion schemes as well. This allows us to use structural recursion as a method of reasoning as well as a method of definition, and to intertwine the two if we feel like it. First though, I'll go over the standard stuff about how to treat the most basic recursion scheme at a general level.
We can represent structural recursion on lists (with elements from a
set A
) using the right fold function:
foldr : (B : Set) → B → (A → B → B) → List → B
which satisfies the following two equations:
foldr B n c nil = n
foldr B n c (cons a as) = c a (foldr B c n as)
As I mentioned
last time, we can read
these off directly as computation rules: when the implementation of
foldr
sees nil
in its last argument, it knows to use its "nil"
parameter; and when it sees cons a as
in its third argument it knows
to use the "cons" parameter. Thus we have a method for computation,
driven by the structure of the data we are processing.
The well-known category-theoretic generalisation of this makes use of
F
-algebras. The basic idea is that the constructors of our inductive
type are encoded as a functor F : Set → Set
. For instance, the
constructors of lists, with elements from some set A
are encoded
using the functor (I've only defined it here on objects, but the
action on morphisms is obvious):
ListF : Set → Set
ListF X = 1 + A × X
The first two arguments of the foldr
function can now be captured as
a function f : ListF B → B
. A pair of a set B
and such a function
f : F B → B
is called an F
-algebra. Given two F
-algebras (k₁ :
F B → B)
and (k₂ : F C → C)
, we define F
-algebra morphisms to be
functions h : B → C
such that h ○ k₁ = k₂ ○ F h
. It is not too
difficult to see that F
-algebras and their morphisms form a
category, called F
-Alg.
For quite a large class of functors F
, F
-Alg has a (unique up-to
isomorphism) initial object. Spelling this out, we have an F
-algebra
(in : F µF → µF)
such that for any other F
-algebra (k : F B → B)
there is a unique F
-algebra morphism from (in : F µF → µF)
to
(k : F B → B)
.
For the lists example, an initial algebra for the functor ListF
is
the set of lists with elements from the set A
, with (in : ListF
(List A) → List A)
defined simply as the construction of lists using
nil
and cons
. By initiality, if we have a ListF
-algebra (k :
ListF B → B)
we get a function of type List A → B
. Since it is a
ListF
-morphism it satisfies the two equations for foldr
above, so
we can interpret foldr
.
More generally, we can interpret specifications of inductive types as
functors F
, the inductive types themselves as the carriers of
initial algebras and structural recursion on them as making use of the
initiality property to generate homomorphisms. Note that not every F
you can write down necessarily has an initial algebra; for instance,
F X = (X → 2) → 2
doesn't have an initial algebra in the category of
sets and functions.
In the recursion schemes literature, folds are referred to as catamorphisms. Edward Kmett has written a comprehensive Knol on catamorphisms. He also has a field guide to recursion schemes, for both data and codata.
From a high level, (constructive) structural induction is just structural recursion with fancier types. And from a computation viewpoint this is fairly accurate: computation still proceeds by looking at data and then deciding what to do next. But we still need to work out what those types should be.
In pure Type Theory (i.e. without extensions for pattern matching and
recursive definitions), structural recursion is presented in terms of
elimination principles. Continuing the example of lists, we are
provided with a pair of constructors nil : List
and cons : A → List
→ List
and an eliminator:
elimList : (P : List → Set) →
(P nil) →
((a : A) → (l : List) → P l → P (cons a l)) →
(l : List) → P l
This looks very similar to the type of the foldr
function above. The
difference is that the return type depends on the input list, and this
dependency is carried through in the types of the "nil" and "cons"
parameters (the second and third parameters).
As with the foldr
function, elimList
satisfies a pair of
equations, which are almost identical, except for some extra
information being passed in the cons
case.
elimList P n c nil = n
elimList P n c (cons a as) = c a as (elimList P n c as)
In presentations of type theory, the construction of elimination
principles is usually defined syntactically by looking at the types of
the constructors. See, for example, Dybjer's presentation of
inductive
families. This
seems a little ad-hoc: one might hope for a generic way of extracting
dependent eliminators for inductive types just from their
presentations as initial F
-algebras. Happily, this is possible.
F
-algebrasGiven a functor F : Set → Set
that has an initial algebra (in : F
µF → µF)
we first need to derive the type of the generic elimination
principle for µF
. The generic fold operator for µF
has this type:
fold : (B : Set) → (F B → B) → µ F → B
Looking at the similarities between the foldr
function on lists and
the elimNat
eliminator, we can guess that a generalisation should
look like this for general (in : F µF → µF)
:
elimF : (P : µF → Set) →
((x : F µF) → lift F P x → P (in x)) →
(x : µF) → P x
I'll attempt to explain this type with reference to the type of
elimList
. The first parameter, P : µF → Set
is the dependent type
we are eliminating to, and is exactly the same. The second parameter
is the "algebra" component. It is a function that takes a value of
type F µF
. In the case of lists, this would either be inl *
(representing nil) or inr (a,l)
representing cons. So, similarly to
F
-algebras representing the multiple parameters to fold
, we are
encoding all the cases into one. The second argument of the algebra
component is a little trickier. I have assumed a functor lift F : (µF
→ Set) → (F µF → Set)
that takes P
and x
and produces some
set. This part somehow encodes the "inductive hypothesis" for this
structural recursion principle. I'll explain this further
below. Finally, the "algebra" part ought to return a value of type P
(in x)
, corresponding to the P nil
and P (cons a l)
parts of the
elimList
type.
Given such an "algebra" parameter, elimF
promises to take any
element x
of µF
and return a value of P x
.
F
I need to give a definition for lift F : (F µF → Set) → (µ F → Set)
now. In the case of lists, we can see that the following definition
gives the right answer:
lift F P (inl *) = ⊤
lift F P (inr (a,l)) = P l
Unfolding this definition in the type of elim
above, it is easy to
see that it is an encoding of the original type of elimList
.
But how do we do this in general for any F
? Hermida and
Jacobs
did this back in the nineties for polynomial F
(i.e. F
s
constructed from constants, sums, products and the identity functor)
by induction on the structure:
lift Id P x = P x
lift (K A) P a = ⊤
lift (F × G) P (x,y) = (lift F P x) × (lift F P y)
lift (F + G) P (inl x) = lift F P x
lift (F + G) P (inr y) = lift G P y
Note there are two cases for F + G
depending on which component the
(F + G) µH
argument is in. It is easy to see that lift F
is also a
functor, so it has an action on morphisms between µF → Set
objects.
Aside Note that this definition doesn't depend on the type of P
being µ F → Set
. We can actually give lift F
the type (A → Set) →
(F A → Set)
for any A
. So we can extend lift F
to be a functor on
the category Fam(Set)
, where objects are pairs (A : Set, P : A →
Set)
. This extra generality helps when proving that structural
induction is derivable from structural recursion, and for further
applications like doing refinement of inductive
types. Logical relations lovers will
also see that this is the definition of the unary logical relation
derived from the type scheme generated by a polynomial functor.
An important property of lift F
is that it is
truth-preserving. For any x : F µF
, there is a (unique) value of
lift F (λy. ⊤) x
. I read this as saying that x : F µF
completely
determines the shape of lift F (λy. ⊤) x
. We can use this to derive
a useful function, using the functorality of lift F
:
all : (P : µF → Set) →
(x : F µF) →
(k : (y : µF) → P y) →
lift F P x
Knowing that lift F
is truth preserving turns out to be just enough
to prove that the elimF
rule above holds, and also that the
following equation holds:
elimF P h (in x) = h x (all P x (elimF P h))
Spelling this out for the case of lists, it is pretty easy to see that
this gives us back the original elimination rule for lists. It is also
true that elimF P h : (x : µF) → P x
is the unique function that
satisfies this equation, at least in the categorical setting. See
Neil, Patty and Clem's
paper for the
category-theoretic proof that this works. The proof only demands that
we have an initial algebra for F
and a truth preserving lifting. As
a hint of the proof, note that if we regard lift F
as an endofunctor
on Fam(Set)
then the premises of the elimF
function amount to
taking a (lift F)
-algebra with carrier (µF, P)
to a morphism (x :
µF) → K₁ µF x → P x
, where K₁ µF x = ⊤
. The proof consists of
showing that K₁ µF
is the carrier of the initial (lift F)
-algebra.
F
I have only defined lift F
for polynomial F
so far, but it is
possible to characterise lift F
for any arbitrary F
, as hinted by
Hermida and Jacobs and fleshed out by Neil, Patty and Clem. Assuming
we had extensional equality, we could define lift F
as:
lift F P x = Σy : F (Σz : µF. P z). F π₁ y = x
where Σx : A. B x
denotes a dependent pair type, and π₁
is the
first projection. It is fairly easy to see that this is always
truth-preserving, and that it coincides with the definition above for
polynomial functors. This is particularly nice because it gives an
extensional (i.e. we don't care about how F
is constructed)
definition of what the lifting is. It is also possible to give a
generic description that works in any fibration with the right
structure, so we can generalise to indexed types, types over
categories of domains and so on.
When actually implementing this in a intensional type theory, like in
Epigram 2 or Foveran, it is better, both because of the lack of
extensional quality and for pragmatic reasons, to define the lifting
directly in terms of the descriptions of the functors. However, the
extensional definition does give a guide as to the form that lift F
ought to take when we move beyond polynomial functors.
My goal in the next post is to show that structural induction on the
structure of an inductively defined type is only one form of
structural induction. Generalising from the set up above, my current
thought for what a "structural induction principle" for some A : Set
should look like consists of:
B
, which records the "sub-structure" of A
k : B → A
H : (A → Set) → (B → Set)
tr : (b : B) → H (λa. ⊤) b
elim : (P : A → Set) → ((b : B) → H P b → P (k b)) → (a : A) → P a
satisfying the equality
elim P h (k b) = h b (all P b (elim P h))
where all
is derived from the witness to truth-preservation.
I should say that I'm not totally fixed on the details. My current
thought is that I might need multiple constructors, or that more
structure of H
is required. But I'm pretty sure that an explicit
description of how elements of the data type we are analysing are
constructed is essential to any description of structural induction,
because it allows us to state the computation rule. My plan is to push
through examples and see what is required.
Previous work on this includes Nils Anders Danielsson's definition of
Recursor
in the Agda standard library, but this doesn't include a notion of
constructor, or a computation rule. Conor also has a definition called
Below
which is pretty much identical.
Obviously structural induction on an inductively defined type fits
into this schema, with B = F µF
, and H = lift F
. It is not so
obvious that more general ones do. In the next few posts I'll cover
how to generate new structural induction principles from old ones. For
those of you that want to read ahead you can look at an outdated
implementation, using an old definition of structural induction
principle in the Foveran
repository.