The Derivative of a Regular Type is its Type of One-Hole Contexts
Extended Abstract

Conor McBride

Abstract

subtraction, an operation inherently troubled by the needto subtract only smaller things from larger, but as the inversion of a kind of addition (see figure 1).

Polymorphic regular types are tree-like datatypes generated by polynomial type expressions over a set of freevariables and closed under least fixed point. The ‘equality types’ of Core ML can be expressed in this form. Givensuch a type expression with  free, this paper shows away to represent the one-hole contexts for elements of within elements of , together with an operation which
will plug an element of  into the hole of such a context.
One-hole contexts are given as inhabitants of a regulartype  , computed generically from the syntactic struc
ture of by a mechanism better known as partial differentiation. The relevant notion of containment is shown tobe appropriately characterized in terms of derivatives andplugging in. The technology is then exploited to give theone-hole contexts for sub-elements of recursive types in amanner similar to Huet’s ‘zippers’[Hue97].

=

Figure 1: a tree as a one-hole context ‘plus’ a subtree
This paper exhibits a similar technique, defined more formally, which is generic for a large class of tree-like data
structures—the ‘regular datatypes’. These are essentiallythe ‘equality types’ of core ML, presented as polynomial
type expressions closed under least fixed point. In particular, I will define and characterize two operations:

1 Introduction

 on types, computing for each regular recursive
datatype its type of one-hole contexts;

Gérard Huet’s delightful paper ‘The Zipper’ [Hue97] defines a representation of tree-like data decomposed into a
subtree of interest and its surroundings. He shows us informally how to equip a datatype with an associated typeof ‘zippers’—one-hole contexts representing a tree with
one subtree deleted. Zippers collect the subtrees forking
off step by step from the path which starts at the hole andreturns to the root. This type of contexts is thus independent of the particular tree being decomposed or the subtree in the hole. Decomposition is seen not as a kind of

Department of Computer Science,
c.t.mcbride@durham.ac.uk+

 on terms, computing a ‘big’ term by plugging a‘small’ term into a one-hole context.
The first of these operations is given by recursion on the
structure of the algebraic expressions which ‘name’ types.
As I wrote down the rules corresponding to the empty
type, the unit type, sums and products, I was astonishedto find that Leibniz had beaten me to them by several centuries: they were exactly the rules of differentiation I had
learned as a child.

University of Durham,

1

btree@

1.1 Motivating Examples
How can we describe the one-hole contexts of a recursive type? Huet suggests that we regard them as journeys‘backwards’ from hole to root, recording what we pass byon the way. I propose to follow his suggestion, except that
I will start at the root and work my way ‘forwards’ to thehole. Both choices have their uses: ‘backwards’ is betterfor ‘tree editing’ applications, but the ‘forwards’ approachis conceptually simpler.

Now imagine similar journeys list ttree for ternary
trees:
ttree  1

ttree3

Each step chooses one of three directions, and remembers
two bypassed trees, so

Consider such journeys within binary trees:
btree 2 btreettree 3 ttree2

leaf node btree btree

It looks remarkably like the type of steps is calculated bydifferentiating the original datatype. In fact, this is exactly
At each point, we are either at the hole or we must step what is happening, as we shall see when we examine how
further in—our journey is a list of steps, list btree for to compute the description of the one-hole contexts forsome appropriate step type btree , but what? At each regular datatypes.
step, we must record our binary choice of left or right,
together with the btree we passed by. We may takebtree 2bool btree

We can define the ‘plugging in’ operation

In order to give a precise treatment of ‘differentiating a
datatype’, we must be precise about the expressions which
define them. In particular, the availability of fixed points
requires us to consider the binding of fresh type variables.
There is much activity in this area of research, but this is
not the place to rehearse its many issues. The approach
I take in this paper relativizes regular type expressions tofinite sequences of available free names. I then explain
how to interpret such expressions relative to an environment which interprets those names.

as follows1

 btree  btree   btreenode 
 true   false  
node !"!# list btree  btree!"! $  btree
%&

$
+$



Presenting the Regular Types

I choose to give inductive definitions in natural deduction style. Although this requires more space than thedatatype declarations of conventional programming lanWe might define btree more algebraically as the sum guages, they allow dependent families to be presented(i.e. ‘choice’) of the unique leaf with nodes pairing two much more clearly: even ‘nested’ types [BM98, BP99]
must be defined uniformly over their indices, whilst thesubtrees—powers denote repeated product:full notion of family allows constructors to apply onlyat particular indices. I also give type signatures to de2
btree  1 btree
fined functions in this way, preferring to present the universal quantification inherent in their type dependency via
Correspondingly, we might write
schematic use of variables, rather than by complex and in1 Huet would write .0/+12143537698;:=<>?353@8A.0/+B:C6
scrutable formulae.

 (')'*!"!

,  !"! -2

D

family Reg in figure 2. Firstly, we embed3 type variDD
ables in Reg , then we give the building blocks for
Let us presume the existence of an infinite2 set Name of polynomials and least fixed point.
names, equipped with a decidable equality. We may thinkD of Name as being ‘string’. The set NmSeq may then be
NmSeq
Ddefined to contain the finite sequences of distinct names.
Reg  Set
Each such sequence can be viewed ‘forgetfully’ as a set.
 D

2.1 Sequences of Distinct Names

Name  Set
D 

E  NmSeq

D 
D NmSeq
 Set

NmSeq
D=H

  Name  NmSeq

DG F

I shall always use names in a well-founded manner. The
D‘explanation’ of some name  from some sequence will
involve only ‘prior’ names—intuitively, those which havealready been explained. It is therefore important to define
DGI
for any such pair, the restriction
 , being the sequenceDof names from prior to  .

PD  Reg DDO    Reg D

0 Reg
Reg
O
 
D
D
O    Reg D

1 Reg
Reg
O
P 
D=H
Reg 
Q  . P  Reg DD D Reg D=H P  RegD=H
O D Reg

Reg
Reg 
 =O

Figure 2: descriptions of regular types

D 
D
 
DGNmSeq
I 

NmSeq
D=H I
D

D=H KJML  I 
DGI
N 



The last two constructors may seem mysterious. However, the redundancy they introduce will save us workwhen we come to interpret these descriptions of types.
We could choose to interpret only Reg E , the closed descriptions, keeping the open types underwater like thedangerous bits of an iceberg. This would require us to
substitute for free names whenever they become exposed,
for example, when expanding a fixed point. We would inturn be forced to take account of the equational properties
of substitutions and prove closure properties with respect
to them. I dispense with substitution.

As equality on names is decidable, I shall freely allow
names to occur nonlinearly in patterns. In order to recover the disjointness of patterns without
JML recourse to pri to mean ‘any
oritizingthem,I
introducethenotationJ
except  ’. Correspondingly, each clause of such a definition holds (schematically) as an equation. I nonetheless The alternative I have adopted is to interpret open descripwrite  to indicate a directed computation rule, reserving tions in environments which explain their free names. The
two unusual constructors above perform the rôles of defi for equational propositions.
nition and weakening, respectively growing and shrinking
the environment within their scope. Definition replaces
substitution and weakening adds more free names without
2.2 Describing the Regular Types
modifying ‘old’ descriptions. This avoids the propagationof substitutions through the syntactic structure and hence
The regular types over given free names, or rather, the ex- concerns about capture—we shall only ever interpret thepressions which describe them are given by the inductive ‘value’ of a variable in its binding-time environment.
2 By ‘infinite’, I mean that I can always choose a fresh name if I needto create a new binding.

3 In fact I am abusing notation by suppressing a constructor symbol.

3

D
 
D
Reg
R  Env % %  &

R
Set
%
%
&&
I
  R  % % RT& & SU


R 
%
%
&
&
% &
 R
  R %%
%
%
&
&
O

 &&
inl  R O
inr   R O%%  &
# R % % &

XZY 
%% &&
X  H YO 
% %  R & &
R 1

R O
%
%
P
P &&
  R
 =% % Q  .P & &

Q
con 
R
 .
%
%
&
%%  &&HP  R %  P =O
 H R&&%%  &&
  R
 =O
  R  =O


2.3 Type Environments
D

A type environment
for a given name sequence assoD
ciates each  in with a type description over the prior
DGI .
names,D 
NmSeq
DEnv  Set
E  Env E
D=H 
D
NmSeqHR  Env D=HEnv 
R  =OO Reg DWe may equip environments with operators for restriction(extracting the prefix prior to a given name) and projection
I(looking up a name’s associated type description). R  isthe environment which explains the free names in RTSU .

Figure 3: the data in regular types

2.5

D
D
D
D
R  I Env
 IR  Env
 I
DG
DG


R 

R SV
T

Env
Reg
H
I

R I
H CJWR L  = O I R =O 

R 
H

R

H KJMR L  = O VS 
N = O VS 

Examples of Regular Types

Let us briefly examine some familiar types in this setting.
We have the unit type 1, so we can use
to build thebooleans:[]\^\_
`a7bMceCfg0h c

O
RTSV



1 X1
Y
inl X Y
inr





D
D

% Reg
% []\+\@_ & &  any   R % % []\+\@_ & &  any Rd
R any RdWe may use Q to build recursive datatypes like the naturalDnumbers and our tree examples, again for any and R , asa fresh bound variable ( below) can always be chosen:

2.4 Interpreting the Descriptions
Now that we have the means to describe regular types,
we must say which data are contained by the type witha given description, relative to an environment explaining
its free names—we must give a semantics
to the syntax.
%%  &
inductively.4
Figure 3 defines the interpretation R

idjWk
l cVamh bMnpoNote that I have not supplied constructor symbols for theembedding rules corresponding to variable-lookup, definition and weakening.
conflations of% % & & These% apparent&&
H
types, e.g. R  = O  with R O , are harmless, as thetypes tell us which embeddings are operative.

Q  . 1 stu
XZYcon  inl X  Y
Hcon inr   

kVkzq{rr` g c fe


}~



Q  . 1 s]  t|XYcon  inl X  X
H
H YYcon inr  }  ` w mxWc4

Q  . 1 -
XYcon  inl ocon inr [ kVq*rrv g c f*e vWw mxWcy

4 The ‘semantic brackets’ do not represent a meta-level operation;

they are intended to be a suggestive object-level syntax for a dependent
family of types.

We may use weakening to define an operation which com- The effect of local type variables is thus reflected at theirputes list types:
place of binding, rather than at their places of use.5_ C k wW g
 ''{!

The significance of the phrase ‘accounted for by the  ’s
in ’ is shown by this simple example:

Q  . 1  pXZY con  inl X 
H Y
con inr  ! 




H v mm g H J
R  E  =X=
`a7bWc `a7bWc H eCfg)h c YeCfg)h c    X `7abWc H eCfg0h c Y   eCfg0h c
The point is thathas typeJ  on account of the  inthis particular R ’s definition of , whereas, irrespective of
R , we can always derive
If we takewe can derive
but not

The finitely branching trees may thus be given bykVq*rre w mxWc, !
Q  . _C  k 

con !


    X HY 

2.6 Subterm Orderings for Regular Types

However, discharging the definition ofJ

in our example:

H v mm g

Let% % us
TakingR E  =% %  & an inductive relation, (  for & & now  defineRR   and , characterizing
the subterms of a term we can derive `a7bWc      = X `7abWc H eCfg0h c YeCfg)h c  X `7abWc H eCfg0h c Y
in accounted for by  ’s in . This relation characterizes     =and
’s rôle as a container of  ’s. I omit the obvious ‘wellBoth  ’s are accounted for by the indicated type, and theformedness’ premises.
derivations follow respectively by the two definition rules.

%% &&  R 
T  A similar phenomenon occurs if we try to specialize this_C ordering to the  ’s contained by a k  , that is, to determine when  T9^ inl T( 
T9^ inr  .1 t      !

  X  H Y
T  ( X  H Y
T  Only the rule for fixed points applies, showing this derived
rule to be complete:1 = . 1 Z      U         !
!
(  ¡5¢ con (|        .  con =   T ]  = .

 T  = |  (    

The premise can only be further simplified by the definition rules: the direct rule finds only the head of the list inJ ; the indirect rule’s second premise finds only the tail in, and the first demands that we search for an  within that
Observe that subterms accounted for by an  in a compos- tail. We thus derive (and show complete) the two rules we
ite type are characterized by a rule for each component
P J of might have hoped for:that type. In particular, the rulesforadefinition=OP
5 It would be interesting to investigate a notion of subterm with afind subterms due to  ’s in and  ’s in O J respectively,P
single rule for definitions capturing ‘£ -subterms within ¤ -term : , rethe latter occurring within subterms due to ’s in . Note membering that ¥ really means ¦ ’: however, we would pay with extrathat the latter rule% % exploits
thewe may see  as complexity in the rule for variables, and with the need to carry extra&&&&
H J fact% % J9thatenvironmental information explicitly.
inhabiting both R O and R
=O
.
5



( 2¡5¢   ')' !   §2¡5¢   !
t''  ! ( 2¡5¢

sion over the syntax of .6 It is defined in figure 4.

D
  
 

We may exploit this ‘containment’ relation to define theusual % subterm%
P & & relation for recursive types, namely    . 
for R Q  . , as follows:T   .
T   . 
T   .
C JML ­
  0 

  O
®


1



   O J P ®  Q . ­

1
0
0



 
 
con 
%% J P &&That is, to find a subterm of con   R Q . , either stopwhere you are, or move down one level to an  containedPby and repeat.  P  cannot go further than one level,
because  is free in !

 

P J
 

[
With a little work, we can specialize these rules for zk q{rr
to

 

  O

z³





¯ 



0

= O ­



D
 
Reg
 Reg D  O P J O J °P ² 
Q^± .  =Q .
P J Q J P ² ±

= .
P J
P J
 
= O ¯
=O

0

 


  O

Figure 4: partial differentiation,¨ ¢ª©¬«"« t ¨  vWw mxW ct,¨ ¢5©«« ¢5©««9*

The first six lines are familiar from calculus. For one-hole
contexts, they tell us thatt ¨  vWw mx c,¨ ¢ª©¬«"« ¢5©««9

 an  contains one  in trivial surroundings
 a J other than  contains no 

3 One-Hole Contexts

 constants contain no  we find an  in anO

Let us now turn to the generic representation of one-hole
contexts for recursive regular types. We shall first need to
see what ‘one step’ is.

 we find an  in an
O





the , or (right) in the

The immediate%%
P & & recursive subterms in some con  ofare those subterms of  which correspondtype R Q  .
P
toH the occurrencesof  in —recall that  has type
%
&
&
P
P
R  =Q  .
. We therefore need to describe the onePP
hole contexts for  ’s in ’s. Since may itself containfixed points, theP primitive operation we need to define willcompute for the type of one-hole contexts for any of its
free names. This operation is exactly partial differentiation.

in either an O or a either (left) in the O , passing
passing the O

Note that partial differentiation is independent of environments: it is defined on the syntax of types alone. Just likethe subterm ordering,it takes no account of the possibilJ
ity that some might, for some R , expand in terms of  .
However, partial differentiation is the basic tool by which
total differentiation is constructed, and this is exactly what
we need when we go under a binder and become liable toencounter local names which potentially do conceal  ’s.
The rule for definitions again handles local variables attheir place of binding, summing the types of contexts for

3.1 Partial Differentiation

6 It is depressing how few mathematics teachers deign to impart thisvital clue to calculus students, giving them rules but no method. I learned
differentiation from the pattern matching algorithm given in [McB70].

The partial derivative of a regular type description withrespect to a free name  is computed by structural recur6

P
directly in , and indirectly in an O buried
 ’s occurringJ

If R

within a . In conventional calculus, this is effectively the‘chain rule’ extended to functions of two arguments´ ¶´ µ ·U|

´{¼
 ´ 
´¹¸ µ º» ´ in the special case where

¶

&& Á
%%
P && Á
 =0  0 then R Q  .
 0

%P

Â



o

o

Writing
for the -fold product of ’s and for theoo
sum of 1’s, we can check (by induction on ), that for

´ 
´{¾
¼¹¿ ¾
´¹½ µ º» ´  z ¸¿ ½
 KÀ  oÄÃÅis  .

%%
R

9

Â && Á o
ÂÆ^Ç
p


Once we know how to differentiate definitions, we canmake the leap to fixed points. If we expand the fixed point Viewed as a one-hole context for  Â , the o tells us whichÂÆÇand apply the ‘chain rule’, we obtain:
 the hole is at, while the records the remaining  ’s.

 J P
  Q . ­



  P
  P


P J Q J P
J =Q J .P 
J =Q J . P
 J P= . °  Q . 

A more involved example finds an  within a list of  ’s_ C kÁ JJ  Q  . 1 st J  J _ CQ^± .   1 st V = k  ²
J J _C  ² ± 1 s] 7V = k 
J
J
J
C
_


²
C
_



Q^± . = k  -p = k t ± ²
 _C  k
 _ C k



Á


It is tempting to solve this recursive equation with a leastÁÁ
fixed point, but does this give the correct
type of one-holeJP
contexts? Yes: every  inside a Q J . must be a piece of‘payload data’ attached to some -node buried at a finite
depth. Hence our journey takes us either to an  at theP
We would indeed hope that a one-hole context for a list
outermost node and stops—hence the  in the ‘baseP
element is a pair of lists—the prefix and the suffix!
incase’—or to a subnode and onwards—hence the _ Cthe ‘step case’: it must stop
eventually. We must weaken Amusingly, the following power series resembles k  ,P
at ± , for ± is not free for . Our journey is clearly linear:ÈÈÈ
the body of the fixed point is syntactically linear in ± . In$;-Ét$@ÊtËSVSzS9 È,Ì for pÍ
deed, the following set isomorphism holds, showing that
our journey is a list of ‘steps’ with a ‘tip’:and conventional calculus tells us that
² ± & ^Á%%% %) _ C k ²
 &&R Q^± .
R
*


O
O


 
@

The rules for differentiating an explicit weakening simply
short-circuit the process if the name we seek is that being
excluded.

3.3

Î

È,Ì

È

Î

 Ï 
t

È,Ì

È

Ï

É

Plugging InGiven a one-hole context in   and an  , we should beable to construct a by plugging the  in the hole. That
Before we develop any more technology, let us check that is, we need an operation which behaves thus:
partial differentiation is giving us the kind of answers we%  &&%% &&%%  &&
expect. Of course, the types we get back will contain lots
R  
R 
R
of ‘0 ’ and ‘1 ’, but the usual algebraic laws which simÐ  ÒÒ ^Ñ  
plify such expressions hold as set isomorphisms. It is also
not hard to show that a recursive type with no base cases
is empty:

3.2 Examples of Derivatives

7

%% &&
ÒÓ R %   &  R Ò Ð   ^Ñ   R % %  &X YÔÐ Ð   ^Ñ 
inl Ò Ð O
  ^Ñ Òinr
X H YÔÐO  ^Ñ ^Ñ 
inl X Ò  YÔÐ OHinr  Ò Ð O J P  ^Ñ ÒQ conX Ò H{inlÕ ! Y  Ð Q J . P  ^Ñ 
con inr.
^Ñ Ò Ð P J =  ^Ñ inl
X H YÖÐ P J O 
inr Ò Ò 
=O
^Ñ 

 uØ-
Ò× 

V³






Ð

inl  Ò Ð O   ^Ñ Ò ^Ñ N
inr
X Ð
Y




H
Ò

X  H Ò O Ð  ^ Ñ   Y
 Ð P ^Ñ°
con  Ò Ð  +Ñ;
Ò P  J Ñ  Õ ! Ð Q J . P  ^Ñ°N7
con
Ò Ð P  +Ñ°Ò Ð P  J Ñ  Ò  Ð  +Ñ;
OÒ  Ð   +Ñ°








Figure 5: plugging in



P

D


Q
How are we to define this operation? should tell us the¹Ùd[  Q . P RegDÒ .  Regshape of the term we are trying to build; should tell us
which path to take and also supply the subterms corre_C  k  PzÙd[ QP
P
sponding to the ‘off-path’ components of pairs. In effect,9
 =Q  .  .
Ò
the operation proceeds by structural recursion on , but its
flow of control involves a primary case analysis on . Of
¹Ù+[ QP . looks likecourse, we need only consider cases where   is not 0. Informally, an inhabitant of
The definition is in figure 5.
Ò Ç

3.4 Subtrees in Recursive Regular Types

')' Ò
É

')'|ÝVÝzÝ

Ò Â

' ' wW g

The   operation picks out  ’s from containers for  ’s. As
suggested above, this gives us the tool we need to pick out A few brief calculations reassure us that
subtrees from our tree-like recursive datatypes, interpreting  as a container for the immediate subtrees of con  .

% % ¹Ùd[  _ C k & & Á% % _C &&
Hence our intuition that contexts for recursive type inR [  zÙd[ & ÁR % % zÙd[k 

%
¹

+
Ù
P
P &&
Q  . habit list P can be made rigorous. The ‘step type’ for hence R
R % % _C   Q à  . [
Á
%
%
&
ß
Q
z

d
Ù
Þ
[
[
kVq*rrkkzq{rr  & &trees in  . is
R
R


 

P

P
 =Q  .

The one-hole contexts for Q  .
given by7ÚÛÜ

7 Abuse of notation—% ¹Ù+[&
R % % ¹Ùd[äkzkVq*rr &kVq*rr
RP

thus inhabit¹Ù+[ Q
P
 .



Á

Á

_ C Câ
RGá2á _ C k  _C  kzkVq*rr É 5ã§ã
k kzq{rr ¬É ã ã
R á2á kThe corresponding notion of ‘addition’ has the signature

Õ !#

is really an operation on ¤8

% % ¹Ùd[ QP && R %% Q  . P &&R Õ
 .
% % Q
P &&
!

R
 .
  . ÕÕFor the ‘ ! ’ depicted above and an appropriate ‘ ’, we Ò or ! for the õ direction. It is moreover the case thatÕÕ
expect !   .  to be
distinct Ò ’s or ! ’s on the right give rise to distinct deriva
tions on the left, and vice versa. I omit the details forreasons of space.
con

Ò Ç

con

Ò
É

con ÝVÝVÝ

Ò Â


4
Of course,   . is defined by iterating
list8 :

Towards an Implementation

Ð P ^Ñ over the Recent extensions to the H ASKELL type system, such as

Jansson and Jeuring’s P OLY P have begun to realise thepotential of generic programming for the developmentwW gof highly reusable code, instantiable for a wide class of Ò'' Õ !   .  Ð P 
datatypes and characterised by equally generic theorems   . con Ò^Ñ Òz   . [JJ97, BJJM98]. However, these systems show no sign ofObserve, for example, that {åæ really behaves like ‘plus’, allowing operations like   which compute types gener¢whilstis effectively ‘append’. It is not hard to show ically by recursion over a closed syntax of type expresP  ¡5¢  ¹Ù+[ Qin general thatand sions, crucially regarding type variables as concrete ob . is a monoid under ‘append’PQjects.
that   . is an action of that monoid on  . .

In a dependent type theory supporting inductive families
Dof datatypes [Dyb91], syntaxes such as Reg can be rep3.5 Subterms and Derivatives
resented as ordinary% data
 & which can then be used to index
the families like R
which reflect them.  becomes
The relationship between the containment orderings and merely an operation on data, requiring no extension toderivatives is an intimate one, and so too is that between the computational power of the theory. A programming
¹Ù+[the subtree orderings and the types computed by. In language based on such a type theory, as envisaged in
effect, the containment ordering is exactly that induced [McB99], would seem to be a promising setting in whichP
by plugging in, while the subtree ordering on Q  . is in- to implement the technology described in this paper. This
duced by   . . What we have done is to give a concrete work is well under way in the Computer-Assisted Reasonrepresentation for the witnesses to these relational prop- ing Group at Durham.
erties. We may prove the following theorems:
The payoffs from such an implementation seem likely tobe substantial, extending far beyond applications to editTheorem (containment)
ing trees. A library of generic tools for working with con%
%
&
&
%
&

For   R  and   R:
texts
would allow us to define functions in terms of these% %  & Ý¹Ò Ð  ( äç è ÒÓ R  
+Ñ;éêhigher-level structures, manipulating data in large chunks,
rather than one constructor at a time. Furthermore, in a
Theorem (subtree)
dependently typed setting, a richer structure on data is%&&PFor º  R Q  . :ipso facto a richer structure on the indices of datatypes.
% % zÙd[ QÕ
P && Õ   . ç è !# R
 . Ý !   . äê
It also seems highly desirable to extend the class ofdatatypes for which one-hole contexts can be manipulated
The proofs of these theorems are easy inductions, on generically beyond the regular types, perhaps to include
derivations for the ë direction, and on the structure of indexed families themselves. A concrete representation
8 Again, Huet would writeof one-hole contexts for a syntax with binding has much.)ì^121Uí36 8ªîzï . ð,ñ <>òì7/ 8¬îVï . ð . con .0ì(ó¤(Bu£ô ñ 6C6
to offer both metaprogramming and metatheory.
9

5 Conclusions and Future Worklor series seems worthy of pursuit and is an active topic ofresearch.

This paper has shown that the one-hole contexts for elements contained in a polymorphic regular type can be represented as the inhabitants of the regular type computedfrom the original by partial differentiation. This technology has been used to characterize data structures equivalent to Huet’s ‘zippers’—one-hole contexts for the subtrees of trees inhabiting arbitrary recursive types in thatclass. The operations which plug appropriate data into
the holes of such contexts have also been exhibited.

In summary, the establishment of the connection between
contexts and calculus is but the first step on a long road—
who knows where it will end?

While this connection seems unlikely to be a mere coincidence, it is perhaps surprising to find a use for the lawsof the infinitesimal calculus in such a discrete setting.
There is no obvious notion of ‘tangent’ or of ‘limit’ fordatatypes which might connect with our intuitions fromschool mathematics. Neither can I offer at present any
sense in which ‘integration’ might mean more than just‘differentiation backwards’.

Acknowledgements
I feel very lucky to have stumbled on this interpretation ofdifferentiation for datatypes with such potential for both
utility and fascination, and has been intriguing me since
the day I made the connection (whilst changing trainsat Shrewsbury). This work has benefited greatly fromhours spent on trains, and enthusiastic discussions withmany people, most notably Konstantinos Tourlas, James
McKinna, Alex Simpson, Daniele Turi, Martin Hofmann,
Thorsten Altenkirch and, especially, Peter Hancock.

One observation does, however, seem relevant: the syntactic operation of differentiating an expression with re- References
spect to  generates an approximation to the change invalue of that expression by summing the contributions [BJJM98] Roland Backhouse, Patrik Jansson, Johangenerated by varying each of the  ’s in the expression in
Jeuring, and Lambert Meertens. Genericturn. The derivative is thus the sum of terms correspondprogramming—an introduction. In S. Doaitse
ing to each one-hole context for an  in the expression.
Sweierstra, Pedro R. Henriques, and José N.
Perhaps the key to the connection can be found by foOliveira, editors, Advanced Functional
cusing not on what is being infinitesimally varied, but on
Programming, Third International Summer
what, for the sake of a linear approximation to the curve,
School (AFP ’98); Braga, Portugal, volume
is being kept the same.
1608 of LNCS, pages 28–115. SpringerVerlag, 1998.
Apart from the implementation of this technology, andthe development of a library of related generic utili- [BM98] Richard Bird and Lambert Meertens. Nested
ties, this work opens up a host of fascinating theoretical
datatypes. In Mathematics of Program Conpossibilities—one only has to open one’s old school textstruction, volume 1422 of LNCS, pages 52–67.
books almost at random and ask ‘what does this mean for
Springer-Verlag, 1998.
datatypes?’.
[BP99]
Richard Bird and Ross Paterson. de Bruijn noThere must surely also be a relationship between thistation as a nested datatype. Journal of Funcwork and Joyal’s general characterization of ‘species oftional Programming, 9(1):77–92, 1999.
structure’ in termsof their Taylor series[Joy87]. For regular types, N É makes a hole for a second  in a one-hole [Dyb91] Peter Dybjer. Inductive sets and families inÂ oMartin-Löf’s type theory. In G. Huet andcontext from  . More generally,  gives all the ouö
G. Plotkin, editors, Logical Frameworks. CUP,
hole contexts for  ’s in ’s in each of the orders with1991.
which they can be found. This strong resonance with Tay10

[Hue97]

Gérard Huet. The Zipper. Journal of Functional Programming, 7(5):549–554, 1997.

[JJ97]

Patrik Jansson and Johan Jeuring. PolyP—a polytypic programming language extension.
In Proceedings of POPL ’97, pages 470–482.
ACM, January 1997.

[Joy87]

André Joyal.
Foncteurs analytiques etespèces de structures.
In Combinatoireénumerative, volume 1234 of LNM, pages
126–159. Springer-Verlag, 1987.

[McB70] Fred McBride. Computer Aided Manipulationof Symbols. PhD thesis, Queen’s University ofBelfast, 1970.
[McB99] Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis,
University of Edinburgh, 1999.

11