A Foundation for GADTs and Inductive Families
Dependent Polynomial Functor Approach
Makoto Hamana

Marcelo Fiore

Gunma University
hamana@cs.gunma-u.ac.jp

University of Cambridge
Marcelo.Fiore@cl.cam.ac.uk

Abstract
Every Algebraic Datatype (ADT) is characterised as the initial algebra of a polynomial functor on sets. This paper extends the characterisation to the case of more advanced datatypes: Generalised
Algebraic Datatypes (GADTs) and Inductive Families. Speciﬁcally, we show that GADTs and Inductive Families are characterised as initial algebras of dependent polynomial functors. The
theoretical tool we use throughout is an abstract notion of polynomial between sets together with its associated general form ofpolynomial functor between categories of indexed sets introduced
by Gambino and Hyland.
In the context of ADTs, this fundamental result is the basis
for various generic functional programming techniques. To establish the usefulness of our approach for such developments in the
broader context of inductively deﬁned dependent types, we apply
the theory to construct zippers for Inductive Families.
Categories and Subject Descriptors D.3.3 [Language Constructs
and Features]: Data types and Structures; F.3.3 [Logics andMeaning of Programs]: Studies of Program Constructs—Type
structure
General Terms Theory, Languages
Keywords Dependent types, categorical semantics

1.

Introduction

It is well-known that every Algebraic Datatype (ADT) is characterised as the initial algebra of a polynomial functor, see e.g.
(Hagino 1987). This representation of ADTs is the basis for various generic functional programming techniques, such as:• fold and fusion techniques (Meijer et al. 1991; Sheard and Fegaras 1993; Launchbury and Sheard 1995; Takano and Meijer 1995; Hu et al. 1996; Ghani et al. 2005; Katsumata andNishimura 2008; Hinze 2010),• polytypic programming (Jansson and Jeuring 1997),• Generic Haskell (Hinze and Jeuring 2003),• program reasoning (Danielsson et al. 2006), and• generic zippers (McBride 2001; Morihata et al. 2009).

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor proﬁt or commercial advantage and that copies bear this notice and the full citationon the ﬁrst page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior speciﬁc permission and/or a fee.
WGP’11, September 18, 2011, Tokyo, Japan.
c 2011 ACM 978-1-4503-0861-8/11/09. . . $10.00
Copyright °The scene of functional languages is however rapidly shifting
to incorporate programming with some kind of dependent types.
Hence, the generic programming techniques listed above should be
extended also to this setting. To tackle the problem in a principledmanner one needs ﬁrst to consider algebraic foundations for inductively deﬁned dependent types, exhibiting them as initial algebras
of a class of polynomial functors. These can then be used to reformulate and extend the known generic programming techniques for
ADTs.
This paper is concerned with inductively deﬁned dependent
types as given by Generalised Algebraic Datatypes (GADTs) andInductive Families (IFs). We show that they are characterised as
initial algebras of dependent polynomial functors between indexed
sets (as induced by an abstract notion of polynomial between sets)
introduced by (Gambino and Hyland 2003). This fundamental result provides links between ADTs, GADTs, and IFs. Thus enabling
the transfer of technologies developed in one world (e.g. ADTs)
to another one (e.g. GADTs) using the following relationships
amongst these classes of datatypes:

ADTs

extend toextend to /GADTs k,Inductive Families

mimicked by
As an application of the theory realising the above, we give a
construction of zipper data structures for IFs that extends the one
for ADTs.
Contributions. The contributions of the paper are:• elaboration on the polynomial representation of various GADTs
and IFs that automatically generate polynomial functors forthem;• presentation of a simple proof of the existence and constructionof initial algebras of polynomial functors for GADTs and IFs;
• development of zippers for IFs.
Our work aims to establish foundations for generic programming with dependent types as understood in the following two
senses:• datatype generic, in that programs that may be instantiated todifferent types are not redeﬁned for each one;• type-theory generic, in that programming principles apply universally (for any language that supports dependent types, suchas Haskell, Agda (Norell 2007), Coq, Epigram (McBride 2004),
Marin-Löf Type Theory, and the Calculus of Inductive Constructions (CIC)).
The foundations of ADTs by means of initial algebras of polynomial functors have achieved these two goals. For instance, princi-

ples based on this representation hold in any language that supports
ADTs.
This paper achieves the goal of datatype genericity. As for thesecond goal of type-theory genericity, we restrict attention to total
type theories and programming. Thus targeting the total fragmentsof Haskell and Agda.
The development of type-theory generic foundations requires anabstract mathematical approach, not relying on syntactic formulations. Thus, encoding formalisms within some particular powerfultype theory (as e.g. CIC) does not match our purposes. Hence, wetake a category-theoretic approach. We are however not concerned
here in providing the most general categorical framework covering
all known languages and type theories. Instead, we work with aconcrete mathematical universe appropriate for the total type theory and functional programming settings, viz. the category of sets.
Organisation. The paper is organised as follows. We recall the
notions of polynomial between sets and of polynomial functors
between categories of indexed sets in Section 2. We characterise
GADTs and IFs, by means of polynomials, as initial algebras forpolynomials functors in Sections 3 and 4. In Section 5, we apply thetheory to the construction of zipper data structures for IFs. Finally,in Section 6, we discuss related work.

2.

Polynomials

Indexed sets. The universes of discourse for modelling GADTs
and IFs considered in this paper are categories of indexed sets.
For a set I, the category SetI has• objects: A : I → Set, i.e. I-indexed sets {A(i) | i ∈ I};• arrows: I-indexed functions f : A → B,
i.e. a family of functions ( f (i) : A(i) → B(i) | i ∈ I).
We note that this construction is parametric in the indexing set, andwe will indeed need to use it in a variety of cases SetI , SetJ , SetI×J ,SetU , etc.
We need recall three important functors between categories ofindexed sets. These arise from a function h : I → J as follows:defh∗ : SetJ → SetIh∗ (A) = A ◦ h ,Σh : SetI → SetJ

Σh (A)( j) =def

∑ A(i) ,i∈Ij≡h(i)defΠh : SetI → SetJ

Πh (A)( j) =∏ A(i) .

i∈Ij≡h(i)

We call the functor h∗ reindexing, the functor Σh dependent sum,and the functor Πh dependent product. Note that in the deﬁnitionof the latter two the index i is subject to the condition j ≡ h(i),where “≡” denotes the equality of elements in a set. Note also thata functor F : SetI → SetJ can be regarded as “curried”, so that it
takes two arguments X ∈ SetI and j ∈ J to give F(X)( j) ∈ Set.
Polynomials. We consider an abstract form of polynomials andpolynomial functors due to (Gambino and Hyland 2003). Thesemathematical structures will be used to express GADTs and IFs.
Deﬁnition 2.1 A (dependent) polynomial P is a triple P = (d, p, c)of functions between sets as follows:
d
Io

E

p

/B

c

/J.

Given a polynomial as above, respectively applying the reindexing, dependent product, and dependent sum to each of its functions,one obtains the series of functors
SetI

d∗ /
SetE

Πp

/ SetBΣc /SetJ .

(1)

Note that reindexing reverses the direction of the arrow.
Deﬁnition 2.2 The (dependent) polynomial functor FP associatedto a (dependent) polynomial P = (d, p, c) is deﬁned as the composite (1); that is, FP : SetI → SetJ deﬁned bydef

FP (X) = Σc (Π p (d ∗ (X))).
We typically omit the subscript P when the polynomial is clear
from the context.
A functor between categories of indexed sets is said to be polynomial whenever it is isomorphic to one induced by a polynomial.
We strictly distinguish between the intensional descriptions provided by polynomials and the extensional counterparts that theygenerate in the form of polynomial functors. This can be understood as in ordinary mathematics, where one distinguishes the syntactic expression x2 and the mathematical function that squares its
argument.
Polynomial functors on Set are instances of dependent polynomial functors for I = J = 1. On the other hand, by expanding
Def. 2.2, dependent polynomial functors can be described concretely as systems of polynomial functors in many variables. Indeed, the description
Polynomial functor of a polynomial P = (d, p, c):
FP (X)( j) =∑∏ X(d(e))

e∈Eb∈Bj≡c(b) b≡p(e)exhibits the dependent polynomial functor FP : SetI → SetJ as a“sum of products” functor. More precisely, it is a J-indexed systemof polynomial functors in I variablesª© ¡FP X)( j) | j ∈ J¡with FP X)( j) given by the sum over b in B j = {b ∈ B | c(b) ≡ j}of the monomials consisting of the product of the X(d(e)) for eranging over Eb = {e ∈ E | p(e) ≡ b}.
Polynomials have several interesting closure properties, seee.g. (Gambino and Hyland 2003; Kock 2009; Gambino and Kock2010). Indeed, they are closed under sums, products, composition,
parameterised initial algebras, and differentiation.
In this paper, we use the fundamental result that every polynomial endofunctor has an initial algebra (see Thms. 3.5 and 4.1, andProps. 3.9 and 4.2) and the operations of sum and differentiation.
The sum of a family of polynomials {Pk = (dk , pk , ck ) | k ∈ K}, for
K an arbitrary set, is the polynomial[dk ]k∈K[c ]Σk∈K pk/ Σk∈K Bk k k∈K/ J
Σk∈K Ek
Σk∈K Pk = I o
for which FΣk∈K Pk ∼= Σk∈K FPk . The operation of differentiation is
discussed in §5.

3. GADTs as Polynomials
We begin with the general deﬁnition of GADTs.
We let α, ε range over type variables, and τ, σ range over monotypes as deﬁned by the grammar
τ ::= α | b | τ → τ0 | D τwhere b is a base type and D is a type constructor. We use thenotation αn for a sequence α1 , . . . , αn of length n (the superscript n
may be omitted). Hereafter, we only treat mono types, and just callthem types.
A GADT D is a type constructor speciﬁed in the following
Haskell-like syntactic form (Schrijvers et al. 2009).
data D : ∗n → ∗ whereK : ∀αl , εm . τ1 → · · · → τk → D σ
Here ∗n → ∗ denotes ∗ → · · · → ∗ → ∗ (with → iterated n-times), K
is a constructor, the type σ can only contain type variables from α,
and each type τi can contain both type variables from α and ε. The
type variables ε can be seen as existentially quantiﬁed, as they do
not appear in the conclusion of the constructor (i.e. the right-handside of the ﬁnal →).
Notation 3.1 Throughout the paper we will adopt the above format to present datatype declaration schema. While the scheme contains only one constructor, we implicitly assume that the declaration provides ﬁnitely many of them. This simpliﬁes the presentation.
An example of GADT is the GADT Fin of “bounded natural
numbers”, see e.g. (Johann and Ghani 2008), deﬁned by in Haskell
notation asdata Z; data S adata Fin :: * -> * where
Zero :: Fin (S a)Succ :: Fin a -> Fin (S a)Here Z and S a are distinct types (not data), deﬁned to be empty.
Universal quantiﬁcation is omitted in Haskell’s GADT declarations. The example does not involve existential type variables. The
type Fin n types natural numbers below n, e.g.
Succ Zero :: Fin (S (S Z)).
In particular, the type Fin Z is not inhabited.
In the following subsections, we proceed to give initial-algebra
semantics for GADTs by means of polynomials. We do thisin a stepwise fashion, considering in turn Simple GADTs, Simple GADTs with constant types, and Positive GADTs. We assume
that there are no mutual deﬁnitions of GADTs in a program. Thus,
any datatype appearing in the declaration of a GADT D must be
constructed without using D.
3.1

Simple GADTs

We consider ﬁrst the following restricted form of GADTs, referred
to as Simple GADTs.

To model a Simple GADT declaration as a polynomial
Io

d

p

E

data D : ∗n → ∗ whereK : ∀αl , εm . D(d1 [α, ε]) → · · · → D(dk [α, ε]) → D(c[α])Assumption: D does not appear in every di and c.
The notation e[α] stands for an expression e that may contain typevariables in α. The di and c are sequences of types of length n.
Simple GADTs provide the most basic form of GDTs thatdepart from ADTs. Fin is an example of a Simple GADT, wherec = S, and there is no ε.

/Jcwe need ﬁrst to deﬁne the sets I, E, B, J. In general, elements ofthese sets are indices of types. What are the indices of a GADT D?
They are themselves types. Hence we need to collect all types used
for deﬁning the GADT D. The set of all closed types U is thus
deﬁned as
U 3 τ ::= b | τ → τ0 | D τ.
Modelling Fin. We start by showing how to model the GADT Fin
as a prototypical example of a Simple GADT. We then generalise
the analysis to arbitrary Simple GADTs.
First, we describe each constructor as a polynomial. We denoteby ! the unique function from the empty set ∅ to a set. The
constructor Zero :: Fin (S a) is modelled by the polynomial
U oZero =

!

∅

/U

!

/ U.

S

The polynomial for Succ :: Fin a -> Fin (S a) is
U o

Succ =

id

U

id

/U

/ U.

S

These deﬁnitions are systematically generated according to theconstructor speciﬁcation. For instance, forSucc :: Fin a -> Fin (S a),the domain Fin a corresponds to the ﬁrst id in the polynomial
Succ, and the codomain Fin (S a) corresponds to the S in thepolynomial. The middle id is due to Succ being unary.
Applying the construction (1) to each polynomial we obtain
their corresponding polynomial functors.
FZero :
FSucc :

SetU
SetU

!∗
id

∗

/ Set∅

Π!

/ SetUΠid/ SetUΣS/ SetU/ SetUΣS/ SetUThe polynomial functor FFin : SetU → SetU for the GADT Fin isdeﬁned as the sum
defFFin (X)(τ) = FZero (X)(τ) + FSucc (X)(τ)= ΣS Π! !∗ (X)(τ) + ΣS Πid id∗ (X)(τ)= ∑ ∏ X(!(e)) + ∑a∈U e∈∅
τ≡S a= ∑ 1 + ∑ X(a)
a∈U
τ≡S a

a∈U
τ≡S a

∏ X(id(e))

a∈U e∈Uτ≡S a a≡id(e)= ∑ 1 + X(a)
a∈U
τ≡S a

The deﬁnition of this functor is equivalent to the deﬁnition by
pattern-matching
FFin (X)(S a) = 1 + X(a)FFin (X)(a) = ∅Simple GADT

/B

otherwise.

It is a general phenomenon that the equality constraint under which
dependent sums are subject expresses pattern-matching. This isalso known as the Henry Ford encoding (see the discussion in §6).
Crucially, one can ensure that the functor FFin has an initial
algebra by a general construction (see Thm. 3.5). This can becalculated as the union of the ω-chain20 ⊆ FFin (0) ⊆ FFin(0) ⊆ · · ·where 0 = {∅ | u ∈ U} ∈ SetU . For n > 0, the ω-chain at an index
Sn a is∅ ⊆ {Zero} ⊆ {Zero} + {Succ a | a ∈ {Zero}} ⊆ · · ·The union Fin ∈ SetU of these, for a ∈ U, is thus described as
Fin(S a) = {Zero, Succ Zero, · · · , Succn

Fin(a) = ∅n−1Zero},

otherwise.

This certainly models the GADT Fin.
General case. Let D be a Simple GADT with constructors
K1 , . . . , Kl . Since di [α, ε] is a sequence of types of length n,seen as taking types α, ε as inputs, it is modelled as a function di : U l+m → U n . Similarly, c[α] is modelled as a function
c : U l → U n.
Notation 3.2 Given two functions f : A → C, g : B → C, we
write [ f , g] : A + B → C for the function [ f , g](x) = f (x) if x ∈ A,
[ f , g](x) = g(x) if x ∈ B. We also use the function ∇ = [idA , idA ] :A + A → A, and more generally ∇k : kA → A as its k-folded version(here kA denotes the k-fold sum A + · · · + A).
The polynomial Pi for a constructor Ki of a Simple GADT isdeﬁned as
Un o[d1 , . . . , dk ]∇kkU l+mcπl/ U l+m/ Un

where πl : U l+m → U l is the projection: πl (τ l , τl+1 , . . . , τl+m ) = τ l .
nnThis induces the polynomial functor FPi : SetU → SetU given by
FPi X(τ) =∑X(d1 (α, ε)) × · · · × X(dk (α, ε))α∈U l ,ε∈U mτ≡c(α)

Here Q introduces “constant types” as a sequence of arbitrary types
that may contain type variables, D does not appear in Q, and c is asequence of types of length n.
Comprehension of an indexed set. We present a construction thatcollects all elements of an indexed set. This is needed to deﬁne thepolynomial for GADTs with constants.
Let A ∈ SetI . The disjoint union of the family {A(i) | i ∈ I} isusually deﬁned by the union of index-labelled sets as
def]i∈I A(i) = ∪i∈I {i} × A(i)= {(i, a) | i ∈ I, a ∈ A(i)}.
Hence the disjoint union operation constructs a single set from anindexed set. We use the new notation {{A}} for ]i∈I Ai , and call it
the comprehension of A, as it comprehensively collects all elementsof A. For a pair (i, a) ∈ {{A}} , the ﬁrst component is an index i ∈ I,
and the second an element a ∈ A(i). We deﬁne the “projection”
function π that selects the corresponding index of an element by
π : {{A}} → I;

π(i, a) = i.

(The theoretical background for the notion of comprehension is
discussed in §6.5).
Polynomial for a constant. Using comprehension, one can deﬁne
a constant type Q ∈ SetU as the polynomial PQ
U o!

/ {{Q}}

!

∅

π

/U .

Indeed, calculating the polynomial functor FPQ : SetU → SetU , wehave
FPQ X(τ) = Σπ Π! !∗ (X)(τ)

Notation 3.3 As above, for ease of reference, we hereafter present
the polynomial of a datatype within double-framed boxes and indicate its corresponding polynomial functor with a left vertical bar.
n

The polynomial functor FP : SetU → SetU
ple GADT D is the sum of the above:n

for the Sim-FP X(τ) = FP1 X(τ) + · · · + FPl X(τ).
(Recall that as noted in §2 the sum of polynomial functors is again
a polynomial functor.)
We record the following corollary of Thm. 3.5.
Proposition 3.4 The polynomial functor of a Simple GADT has an
initial algebra.
3.2

Simple GADTs with constant types

Simple GADTs lack constant parameters within their deﬁnition.
Consider the GADT Vec of length-indexed lists, called vectors.
data Vec :: * -> * where
Nil :: Vec Z
Cons :: Int -> Vec n -> Vec (S n)This declaration involves the constant type Int, not covered by
the previous account. So we extend the class of Simple GADTs
as follows.
Simple GADT with constant types
data D : ∗n → ∗ whereK : ∀αl , εm . Q[α, ε] → D(d1 [α, ε]) → · · · → D(dk [α, ε])→ D(c[α])

=

∑

1=

(i,t)∈{{ Q}}τ≡π(i,t)∑1=∑ 1∼= Q(τ).

(τ,t)∈{{ Q}}t∈Q(τ)The important points in this derivation are: (τ,t) ∈ {{Q}} ⇔ t ∈ Q(τ)(by deﬁnition) and ∑s∈S 1 ∼= S (for every set S).
Interpretation of a type. We also prepare the way to interprettypes. The polynomial of a GADT D is denoted PD , and we use theshorter notation FD for its associated polynomial functor FPD . The
initial FD -algebra is denoted µ FD . Each base type b is associatedwith some set B; e.g. Int is associated with Z.
The interpretation [[αl ` τ]] of a mono type τ under the type varilable context α is an indexed set in SetU , taking closed types σ ∈ U ll
to give the set [[α ` τ]](σ) interpreting τ instantiated at σ. The definition is as follows:[[α ` αi ]](σ) = [[ ` σi ]][[α ` b]](σ) = B[[α ` τ → τ0 ]](σ) = [[α ` τ]](σ) → [[α ` τ0 ]](σ)[[α ` D τn ]](σ) = (µ FD )([[α ` τ1 ]](σ), · · · , [[α ` τn ]](σ))
We remark that, even though a polynomial PD may use the interpretation function, the deﬁnition is not circular because we do notconsider mutual GADTs in this paper.
Polynomial for a Simple GADT with constant types. We deﬁne
the polynomial for Simple GADTs with constants.
Suppose the “constant type” part Q[α, ε] in a declaration of a
Simple GADT with constant types to be a sequence Q1 [α, ε], . . . , Q p [α, ε]ei =of types. Each type Qi [α, ε] is modelled as the indexed set Q
U l+me=[[α, ε ` Qi ]] ∈ Set, and the type Q[α, ε] is modelled as Q
l+m
U
e
e
Q1 × · · · × Q p ∈ Set. The expressions c are modelled as functions c : U l → U n . The polynomial PD for a Simple GADT withconstants is[d1 , . . . , dk ] ◦ kπe}Un ok{{ Q}∇kcπl π/ {{Q}
e}nThis gives the polynomial functor FD : SetU → SetU
FD X(τ) =An important difference with the previous representations is thatthe domain of Var is a type variable a. The use of this type variable
is essential to get an element (i.e. de Bruijn variable) from an
instantiated type. The interpretation of the type variable in Var is[[α ` α]] ∈ SetU , hence

/ Un

n

e ε) × X(d1 (α, ε)) × · · · × X(dk (α, ε))∑ Q(α,

α∈U l , ε∈U mτ≡c(α)

Theorem 3.5 For every Simple GADT D with constant types, thepolynomial functor FD has an initial algebra D. Moreover, D canbe explicitly constructed asD(u) =[FDi (0)(u)i∈Natfor every u ∈ U n .
Proof It is well-known that there are adjoints: Σh a h∗ a Πh(see §6.2). Thus, being left adjoints, ([d1 , . . . , dk ]π)∗ and Σcπl πpreserve colimits (see e.g. (Mac Lane 1971)). Moreover, since Π∇kis ﬁnitary (see e.g. (Gambino and Kock 2010, Sec. 1.19)), thecomposite FD preserves ﬁltered colimits. Hence one can apply the
Basic Lemma of (Smyth and Plotkin 1982) to construct the initial
algebra. This is as stated because colimits in categories of indexed
sets are given pointwise. ¤Example 3.6 (Well-scoped λ-terms) Consider the GADT ofwell-scoped untyped λ-terms.
data Lam :: * -> * where
Var :: Fin n -> Lam n
App :: Lam n -> Lam n -> Lam n
Abs :: Lam (S n) -> Lam nThis is a Simple GADT with constant types because it contains
Fin n. Using Fin ∈ SetU as constructed in §3.1, we deﬁne thepolynomials
Var =

U o

App =

∇
U o

Abs =

U o

!

S

∅

!

/ {{Fin}}

π

2U

∇ /
U

id /
U

U

id /
U

id /
U

/U

Var =

U o

App =

U o

∇

Abs =

U o

Incr

!

∅

!
2U
U

/ {{[[α ` α]]}}

/U

∇

/U

id

/U

id

/U

id

/U

These yield the polynomial functor FLam : SetU → SetU
FLam X(τ) = [[ ` τ]] + X(τ)×X(τ) + X(Incr τ)Here we assume that U does not contain types of the form Lam σ.
This is practically unproblematic because the type variable a isusually expected to be instantiated with type level natural numbers. The reason for this exclusion is that [[ ` τ]] uses µFLam when
τ = Lam σ. The complete solution to cope with this mutual reference may be formulated in the framework of indexed inductionrecursion (Dybjer and Setzer 2006) or using the technique of nested
inductive types (Abbott et al. 2004).

Example 3.8 (Typed expressions) Consider the GADT of typed
expressions.
data Expr :: * -> * where
Const :: Int -> Expr Int
IsZero :: Expr Int -> Expr Bool
If:: Expr Bool -> Expr a -> Expr a -> Expr a
We set KZ = {Z | u ∈ U} ∈ SetU , and deﬁne KInt , KBool : U → U
by KInt (τ) = Int, KBool (τ) = Bool. The polynomials are
Const =U o!

IsZero =

U o

KInt

If =

U o

[KBool ,id,id]∅
U
3U

KInt π

!

/ {{KZ }}

/U

id

/U

KBool

/U

∇3

/U

id

/U

These yield the polynomial functor F : SetU → SetU

Applying Def. 2.2 yields the polynomial functor F : Set → Set
UU

FX(τ) = (τ ≡ Int) × Z

FX(n) = Fin(n) + X(n)×X(n) + X(S n)+ (τ ≡ Bool) × X(Int)

which is the same as the well-known one from (Fiore et al. 1999).
The initial algebra Lam can be explicitly calculated by repeatedly
applying F to 0 ∈ SetU as in the case of Fin.

+ X(Bool) × X 2 (τ).

Example 3.7 (Nested datatype style λ-terms) Bird and Patersongave a slightly different representation of well-scoped λ-terms using a so-called nested datatype (Bird and Paterson 1999b). It can bepresented as a GADT as follows.

def

where (τ ≡ σ) = {? | τ ≡ σ}; i.e. (τ ≡ σ) is the singleton set {?} ifτ = σ, and the empty set if τ 6= σ. This is equivalent to the deﬁnition
by pattern-matching
FX(Int) = Z + X(Bool) × X 2 (Int),
FX(Bool) = X(Int) + X(Bool) × X 2 (Bool),data Incr :: * -> * where
Zero :: Incr a
Succ :: Incr a -> Incr adata Lam :: * -> * where
Var :: a -> Lam a
App :: Lam a -> Lam a -> Lam a
Abs :: Lam (Incr a) -> Lam aπ

FX(τ) = X(Bool) × X 2 (τ)
3.3otherwise.

Positive GADTs

We ﬁnally consider the most general case, allowing the constructors
to be parameterised by functions.

Here I = I1 × · · · × In , J = J1 × · · · × Jl ,and E = E1 × · · · × Em , Q = Q1 × · · · × Qq .

Positive GADT
data D : ∗n → ∗ whereK : ∀αl , εm . Q[α, ε] → (S1 [α, ε] → D(d1 [α, ε])) → · · ·Assumption: D does not appear in I, J, E, Q

→ (Sk [α, ε] → D(dk [α, ε])) → D(c[α])Assumption: D does not appear in Q and every Si .
l+m
Each Si is modelled as Sei ∈ SetU . We deﬁne the function d :e × (Se1 + · · · + Sek )}} → U n by d((α, ε),t, (i, s)) = di (α, ε), where{{Q
each d1 , . . . , dk is modelled as di : U l+m → U n . We also deﬁnee ε), s ∈ Sei (α, ε), 1 ≤ i ≤ k.
p1 ((α, ε),t, (i, s)) = ((α, ε),t) for t ∈ Q(α,Considering the previous accounts, we let the polynomial for a
Positive GADT D be given by

Un o

d

e × (Se1 + · · · + Sek )}}
{{Q

p1

cπl π
/ Un
/ {{Q}e}This gives the polynomial functor
FD X(τ) =∑e}((α,ε),t)∈{{ Q}τ≡c(α)=∏X(di ((α, ε), s))e } ×(Se1 +···+Sek )((α,ε),t,(i,s))∈{{ Q}e ε) × (Se1 (α, ε) → X(d1 (α, ε))) ×· · ·∑ Q(α,

α∈U l ,ε∈U mτ≡c(α)× (Sek (α, ε) → X(dk (α, ε)))These polynomial functors have weaker preservation properties than those of the previous cases: they preserve κ-colimits forκ a limit ordinal greater than the cardinality of every Sei (α, ε) (sothat, for instance, they preserve ω-colimits when every Sei (α, ε)is a ﬁnite set). In this case, the existence and explicit construction of initial algebras is guaranteed by a transﬁnite version of
the Basic Lemma (Smyth and Plotkin 1982) previously developedby (Adamek 1974). Hence we also have the following.

We assume I, J, E to be product types to avoid clutter. Of course,
our modelling works also for the usual presentation in curried form.
In a Simple IF declaration, E is a type other than D. Eachd1 , . . . , dk , c is a sequence of expressions of length n. Also j : Jdenotes a sequence ( j1 , . . . , jl ) : J1 × · · · × Jl (though we avoid thetedious notation j for it), as so does e : E.
To compare the scheme for Simple IFs to the one for Simple GADTs with constants, note that the variable j and the type E
in a Simple IF respectively correspond to the type variables α andthe constant part Q in a Simple GADT.
The essential difference is that in a Simple IF the parameter jdoes not stand for a tuple of types but for a tuple of elements oftypes J1 , . . . , Jl . This scheme is more natural than GADTs in many
practical examples because one does not need to use a type classtechnique to express constraints.
The scheme of Simple IFs practically covers almost all everyday
uses of IFs. Indeed, except for the use of large type parameterssuch as (A : Set), all examples in (Oury and Swierstra 2008) are
Simple IFs.
Polynomial for a Simple IF. Our polynomial modelling follows.
• The types J1 , . . . , Jl are modelled as sets by means of the initialdef• The type Q is modelled as an indexed set Q ∈ SetJ×E .
• Each expression di [ j, e] is modelled as a function di : J × E → I.
• The expression c is modelled as a function c : J → I.
The polynomial PD for this scheme is the same as the polynomial for Simple GADTs with constant types.
[d1 , . . . , dk ] ◦ kπ
k{{ Q}}
Io

Proposition 3.9 The polynomial functor of a Positive GADT has
an initial algebra.

4.

Inductive Families as Polynomials

Dybjer introduced the notion of Inductive Family (IF) as a powerfulschema for inductively deﬁned dependent types (Dybjer 1994). For
brevity, we treat here a slightly cut down version of this notion. As
before, we do this in a stepwise fashion, considering ﬁrst Simple IFs
and then Basic IFs.
In this section, we use Agda notation (Norell 2007). Furthermore, we assume that there are no mutual deﬁnitions between IFs
in a program. That is, any type appearing in the declaration of an
IF does not refer to it.
4.1

Simple Inductive Family
data D : I → Set whereK : ( j : J) → (e : E) →Q[ j, e] → D(d1 [ j, e]) → · · · → D(dk [ j, e]) → D(c[ j])∇k/ {{Q}}

c πl π/I

It gives the polynomial functor FD : SetI → SetI
FD X(m) =∑ Q( j, e) × X(d1 ( j, e)) × · · · × X(dk ( j, e))j∈J, e∈Em≡c( j)Theorem 4.1 . For every Simple IF D, the polynomial functor FD
has an initial algebra D. Moreover, D can be explicitly constructedasSimple Inductive Families

We consider ﬁrst a simple, yet practical, class of IFs close to
Simple GADTs with constant types.

defalgebra semantics, and J = J1 × · · · × Jl ∈ Set. Likewise, E =E1 × · · · × Em ∈ Set.

D(u) =[FPi (0)(u)i∈Natfor every u ∈ I.
Proof Analogous to Thm. 3.5. ¤4.2

Basic Inductive Families

We introduce an extension to the scheme of the previous section.

Basic Inductive Family
data D : I → Set whereK : ( j : J) →(e : E[ j]) → ((s : S1 [ j, e]) → D(d1 [ j, e, s])) → · · ·→ ((s : Sk [ j, e]) → D(dk [ j, e, s])) → D(c[ j])where I = I1 × · · · × In , J = J1 × · · · × Jl , E = E1 × · · · × Em .
Assumption: D does not appear in I, J, E and every Si .
This scheme is similar to that of Positive GADTs (with the variable e corresponding to the type variables ε) but generalised to constructors parameterised by dependent functions.
Polynomial for a Basic IF. Modelling Basic IFs is a further
elaboration on the previous developments.
• J, c are modelled as before.

5.1• E is modelled as an indexed set E ∈ SetJ .
• Each type Si is modelled as an indexed set Si ∈ Set{{E}} ; so that
S1 + · · · + Sk ∈ Set{{E}} , and hence {{S1 + · · · + Sk }} ∈ Set.
• Each expression di [ j, e, s] is modelled as a function
di : {{Si }} → I.
• The function d : {{S1 + · · · + Sk }} → I is deﬁned byd(( j,t), (i, s)) = di ( j,t, s)
The polynomial PD for a Basic IF D is
Iod{{S1 + · · · + Sk }}π/ {{E}}cπ /IThis gives the polynomial functor FD : SetI → SetIFP X(u) =∑j∈Ju≡c( j)∼=∑∏X(di ( j, e, s))(i,s)∈(S1 +···+Sk )( j,e)

∏ X(d1 ( j, e, s)) × · · · × ∏ X(dk ( j, e, s))j∈J, e∈E( j) s∈S1 ( j,e)u≡c( j)in a tree, and a context consisting of the list of depth-one linear
contexts obtained after navigation. Zippers have only been considered on ordinary ADTs (Huet 1997; McBride 2001; Adams 2010;
Morihata et al. 2009), such as lists and trees.
McBride found the interesting phenomenon that the derivative of the polynomial functor associated with an ADT provides the type of depth-one linear contexts for the zipper on thedatatype (McBride 2001). For instance, for the ADT of binary
trees with associated polynomial functor FX = 1 + X × X, theformal derivative F 0 X = X + X gives the type of depth-one linear
contexts because: when the cursor goes to the left (resp. right) childof a tree, one needs to push the right (resp. left) subtree to a stack
for later navigation; so that the left (resp. right) summand in F 0 X isfor the right (left) depth-one linear context.
In this section, we consider partial derivatives for dependent
polynomial functors, observe that the notion is again well-suited forthe representation of depth-one linear contexts, and thereby develop
zippers on IFs and GADTs.

s∈Sk ( j,e)

As in Prop. 3.9 we have the following.
Proposition 4.2 The polynomial functor for a Basic IF has an
initial algebra.

We saw in Example 3.6 that the polynomial functor for well-scoped
λ-terms is F : SetNat → SetNat deﬁned by
FX(n) = Fin(n) + X(n)×X(n) + X(S n)where Nat is the ADT of natural numbers.
We now want to built the zipper for λ-terms. This is of practicalimportance; for instance, to develop programs for navigating andmodifying λ-terms (in a structured editor, in an interpreter, etc.)
represented by the GADT or IF of this polynomial functor. To
deﬁne the zipper, we need the type of depth-one linear contexts.
This we will build from the partial derivatives of the polynomial
functor.
For the case of well-scoped λ-terms, the partial derivative of F
with respect to m ∈ Nat is ∂m F : SetNat → SetNat given by∂m F(X)(n) = (m ≡ n) × (X(n) + X(n)) + (m ≡ S n) × 1. (2)In general, the index m of the partial derivative ∂m F designates theindex of the cursor of the zipper. In the case of the GADT or IF of
λ-terms, an index of the datatype is an environment (i.e. a set of all
possible free variables). The summands of (2) are the type of depthone linear contexts in the environment n. At the technical level one
can see this by observing that there is a canonical function
plug : µ F(m) × ∂m F(µ F)(n) → µ F(n)that plugs a λ-term in environment m into a depth-one linear context for λ-terms in environment n to construct a λ-term in environment n. Indeed, according to the three summands of (2), thefunction plug is built from the following three functions

Basic IFs are very similar to the Inductive Families of (Dybjer
1994). The differences are that in the latter

plugL : µ F(m) × µ F(m) → µ F(m) , plugL(t, c) = App t c
plugR : µ F(m) × µ F(m) → µ F(m) , plugR(t, c) = App c t
plugI : µ F(S m) → µ F(m), plugI(t) = Abs t(i) every sequence of types is a so-called telescope (namely, latertypes may depend on earlier types in the sequence), and(ii) the large type Set is allowed as a type of a parameter.
The model above can be extended to cope with these: (i) is
easily modelled by using the dependent sum of sets corresponding
to the types; as for (ii), modelling large types can be treated in theframework of induction-recursion (Dybjer and Setzer 2003, 2006).

5.

Application: Dependent Zippers

As an application of the use of polynomial functors, we consider
zippers for IFs.
A zipper is a datatype for navigating a tree-like structure (Huet
1997). It is given by a pair of the current focus (called the cursor)

Partial derivatives of the polynomial functor for λ-terms

that respectively plug a term in the left-hand-side of an application,in the right-hand-side of an application, and inside an abstraction.
Formula (2) is obtained as an instance of a general formula forpartial derivation that we introduce next.
5.2

Differentiation

The differentiation operator ∂ maps a polynomial functor F :SetI → SetJ to a polynomial functor ∂F : SetI → SetI×J . It is
assembled from the partial derivatives of F with respect to i ∈ I,
for which we write ∂i F : SetI → SetJ , in a pointwise fashion as
follows∂F(X)(i, j) = ∂i F(X)( j).

data Ctx : I → Set where [] : {m : I} → Ctx(m)



K
:
{
j
:
J}
→
{e
:
E}
→
Q[
j,
e]
→
i






D(d
[
j,
e])
→
·
·
·
→
D(d
[
j,
e])
→
Ctx(c[
j])
→
Ctx(d
[
j,
e])
i
1
k




|
{z
}




with only D(di [ j, e]) missingi∈[k]data Zipper : I → Set where. : {m : I} → D(m) → Ctx(m) → Zipper(m)failure : {m : I} → Zipper(m)downi : { j : J} → {e : E} → Zipper(c[ j]) → Zipper(di [ j, e])downi (K q a1 . . . ai−1 ai ai+1 . . . ak . C) = (ai . Ki q a1 . . . ai−1 ai+1 . . . ak C)
upfromi : { j : J} → {e : E} → Zipper(di [ j, e]) → Zipper(c[ j])upfromi (ai . Ki q a1 . . . ai−1 ai+1 . . . ak C) = (K q a1 . . . ai−1 ai ai+1 ak . C)
Figure 1. Zipper for a Simple IF D
The partial derivative operators are to satisfy the following basic
laws.
d

!

id

• For every monomial M = (I ←− E −→ 1 −→ 1) with induced
monomial functor FM (X) = ∏e∈E X(d(e)),∂i FM (X) ∼=∑∏X(d(e)).

∑∑j∈J, e∈E( j) (i,s)∈S( j,e)n≡c( j)m≡di ( j,e,s)• For a family of polynomial functors {Fk : SetI → SetJ | k ∈ K},∼ ∑k∈K ∂i Fk (X).
∂i (∑k∈K Fk )(X) =pdc

It follows that for a polynomial P = (I ←− E −→ B −→ J) withinduced polynomial functor∑

Proposition 5.2 The partial derivatives of the polynomial functor
for a Basic IF D are∂m FD (X)(n) =`∈E e∈E\{`}i≡d(`)FP (X)( j) =The partial derivatives of the polynomial functor for λ-termsof (2) are an instance of the above proposition.

∏ X(d(e))

X(di0 ( j, e, s0 ))(i0 ,s0 )∈S( j,e)\{(i,s)}∏defwhere S = S1 + · · · + Sk .
Polynomials are indeed closed under differentiation; as one hasthat∂FP (X) ∼= F∂P (X)
for

e∈E
b∈B
j≡c(b) b≡p(e)

p

def

d0

p0

c0

∂(I ←− E −→ B −→ J) = (I ←− E 0 −→ B0 −→ I × J)dits partial derivative should be given by

c

where
Ei,b = {` ∈ E | i ≡ d(`), b ≡ p(`)} ,Partial derivatives of polynomial functors∂i FP (X)( j) =

∑

∑

E0 =

∏ X(d(e))

b∈B `∈Eb e∈Eb \{`}j≡c(b) i≡d(`)

B0 =

def

Eb = {e ∈ E | b ≡ p(e)}Intuitively, this deﬁnition of partial derivative can be understoodas follows. The set Eb consists of the available indices of the
product part of the polynomial functor FP . If the index of the cursor
of a zipper uses ` ∈ Eb , then the indices of the rest depth-one linear
context are the elements in Eb except for ` (as this index is being
used as that for the cursor).
We instantiate the general formula for partial derivatives in two
concrete cases.
Proposition 5.1 The partial derivatives of the polynomial functor
for a Simple IF D are∂m FD (X)(n) ∼= ∑∑ Q( j, e) × ∏ X(d` ( j, e))defwhere [k] = {` ∈ N | 1 ≤ ` ≤ k}.

∑ ∑ Eb \ {`} ,∑∑ Ei,b ,(i, j)∈I×J b∈Bj≡c(b)

wherej∈J,e∈E i∈[k]n≡c( j) m≡di ( j,e)∑(i, j)∈I×J b∈B `∈Ei,bj≡c(b)(3)`∈[k]\{i}d 0 ((i, j), b, `, e) = d(e) ,p0 ((i, j), b, `, e) = ((i, j), b, `) ,c0 ((i, j), b, e) = (i, j) .
Finally, and importantly for what follows, we note that for apolynomial functor F : SetI → SetI , its partial derivatives comeequipped with canonical functions(i) µ F(m) × ∂m F(µ F)(n) → µ F(n), and¡¢(ii) µ F(n) × ∑b∈B Em,b → 1 + µ F(m) × ∂m F(µ F)(n)for (i) plugging-in data in a depth-one linear context, and (ii) for,whenever possible, disassembling data at a given index, into a
datum and a depth-one linear context.
5.3

Dependent zippers

The zipper for a polynomial functor F : SetI → SetI is the indexed
set Zipper ∈ SetI deﬁned asdef

Zipper(m) = µ F(m) × Ctx(m)whereCtx(m) ∼= 1 + ∑ ∂m F(µ F)(n) × Ctx(n).

(4)

n∈I

As such, Zipper consists of pairs of the current focus and a context.
A context in Ctx is a list of depth-one linear contexts for the focus.
Simple IFs. Figure 1 gives an implementation of the zipper
datatype for a Simple IF D in Agda. It is based on the partial
derivatives of the associated polynomial functor FD as explained
above, and provides the navigation operations down and upfrom.
The implementation of Ctx by means of the datatype Ctx isderived as follows. By (4), the type of a constructor of Ctx shouldbe∑ ∂m FD (D)(n) × Ctx(n) → Ctx(m).

n∈IBy expanding ∂m FD (D)(n) for the case of the Simple IF D (seeProp. 5.1), this type is isomorphic to∑∑∑ Q( j, e) × ∏ D(d` ( j, e)) × Ctx(n) → Ctx(m).

n∈I j∈J,e∈E i∈[k]n≡c( j) m≡di ( j,e)`∈[k]\{i}By instantiating the equality constraints for n and m, and swapping
the second and the third sum, this is in turn isomorphic to∑ ∑ Q( j, e) × ∏ D(d` ( j, e)) × Ctx(c( j)) → Ctx(di ( j, e))i∈[k] j∈J
e∈E

from which one can in principle implement the type Zipper together with the navigation operations, the kind of dependentlytyped programming required may be too involved. The issue here is
the implementation of the “set difference” S( j, e) \ {(i, s)} used in
the deﬁnition of ∂m F(X)(n) (see Prop. 5.2). This operation invokes
computations and equality in the deﬁnition of the datatype Ctx withthe effect that the pattern matching in the down and upfrom operations requires explicit proofs to be passed to the type checker. (Thiscomplication does not appear in the case of Simple IFs because therequired “set difference” was implemented by explicitly omitting
an argument from the type of a context Ki in the deﬁnition of Ctx.)
Fortunately, almost all dependently-typed data structures foundin the literature (Oury and Swierstra 2008; Norell 2008; Bove andDybjer 2008) are Simple IFs. Hence there seems to be no current
need for zippers on non-simple inductive families. We hope that the
difﬁculty discussed above will be resolved when dependently-typed
programming is mature.
In the case of Positive GADTs the situation is worse, as Haskell
seems not to be powerful enough to manipulate the needed complex
types for indexing.

`∈[k]\{i}which is the type used for the constructor Ki in the declarationof Ctx in Figure 1. Thus, we implement Ctx as the datatype Ctx
with depth-one linear contexts given by constructors Ki , where iindicates the missing argument of the original constructor K.
The navigation operations are deﬁned schematically for every K and Ki . Failure cases are omitted for simplicity. The function (downi z) expresses “going down to the i-th child in the D-partin the zipper z”. Similarly, (upfromi z) expresses “going up fromthe i-th child”. Going down and up to a child in the Q-part in a zipper are deﬁned similarly; as so are change, insertion, and deletion
operations on zippers.
Instantiating this general zipper for the datatype of λ-terms, we
obtain the zipper on well-scoped λ-terms. The zipper at the rootof a λ-term t is (t . []), expressing that the cursor is focusedon t and that the current context is empty. Starting from this, thenavigation operations enable any traversal of the structure of the
λ-term. In this process, a context increases or decreases as needed.
Note that the crucial operations of stripping and adding binders on
λ-terms by means of down and upfrom are deﬁned using suitableindexes on the type Zipper. Hence the operations maintain theinvariant of terms being well-scoped. This is one of the principles ofdependently-typed programming: program correctness is ensured
by typing.
Note also that our schema is generic in the sense that its instantiation to any Simple IF yields a zipper. We say that a datatype iszipperable whenever there is a zipper datatype for it that supports
navigation operations. As we have seen, then, every Simple IF is
zipperable.
A Simple IF can be simulated by a Simple GADT with constanttypes because the polynomials obtained for these are the same. Thisis an example of what we have referred to in the Introduction as“enabling the transfer of technologies (the zipper) developed in
one world (IFs) to another one (GADTs)”. It follows that every
Simple GADT is zipperable.
Basic IFs. Is a Basic IF zipperable? In theory, yes; though in practice this is unclear. This is because even though we have obtained
an explicit formula for the partial derivatives of arbitrary Basic IFs

6. Discussion and Related Work
6.1

Henry Ford encoding and GADTs

The departure of GADTs from ordinary ADTs resides in that thecodomain of each constructor may have various instances, e.g.
data Expr :: * -> * where
Const :: Int -> Expr Int
IsZero :: Expr Int -> Expr Bool
If:: Expr Bool -> Expr a -> Expr a -> Expr aUsing equality constraints, however, this can be rewritten asdata Expr :: * -> * where
Const :: (a ~ Int) => Int -> Expr a
IsZero :: (a ~ Bool) => Expr Int -> Expr a
If:: Expr Bool -> Expr a -> Expr a -> Expr awhere (a ~ τ) is the equality constraint a ≡ τ on types. In thismanner, GADTs can be regarded as parameterised ordinary ADTs,
with all constructors having the same codomain type, but underequality constraints. This technique is known from the early daysof GADTs (Hinze 2003) and has been used in the formulation oftype inference for GADTs (Schrijvers et al. 2009).
In fact, the idea was already known for IFs before GADTs
were proposed by the Haskell community. McBride explained thegeneral technique using Henry Ford’s phrase: “You can have anycolor you like, as long as it’s black.” (McBride 1999, Sec. 3.5). In
this light, the use of the equality type in a constructor declarationsuch as the one below
Const : ∀α.(α ≡ Int) → Int → Expr(α)
expresses that “you can have any type α you like, as long as it’s
Int”.
6.2

Left Kan extensions and GADTs

Another technique to make all codomains of a GADT declaration
have the same type (by appropriately shifting the varying types tothe domain side) involves the use of the category-theoretic concepts of Kan extension and adjunction1 . These notions play a fundamental role in what regards to the three functors used to deﬁne
1 In the context of functional programming, the concept of right Kan exten-

sion has been used to derive generalised fold for nested datatypes (Bird andPaterson 1999a; Abel et al. 2005). Various adjunctions, including those forKan extensions, are applied to develop “adjoint fold” techniques in (Hinze
2010).

polynomial functors, and so we review that ﬁrst. Subsequently, we
consider encodings for GADTs by left Kan extensions.
Kan extensions. It is well-known in categorical logic and type theory that the dependent sum functor Σh , the reindexing functor h∗ ,and the dependent product functor Πh form a string of adjunctions.
Explicitly, for every h, we have the following two adjoint pairs offunctors (Lawvere 1969)∗Σh a h a Π h .

Lanh a (− ◦ h) a Ranh .
Here Lanh , left Kan extending along h, is the left adjoint to theprecomposition functor (− ◦ h) = h∗ . Dually, Ranh , right Kan extending along h, is the right adjoint to h∗ .
In the presence of enough categorical structure, left and rightKan extending can be respectively described by means of coends
and ends (Mac Lane
R 1971, Chap. X.4), for which one typicallyuses the notation due to Yoneda (Yoneda 1960). (A coend is
a colimit, readily described as a coequalizer between coproducts;
dually, an end is a limit, readily described as an equalizer between
products.) In the context of indexed sets, the (co)end formulae forKan extending along h : I → J are:
Z i∈I

J(h(i), j) × X(i) ∼=∑ X(i) = Σh (X)( j)i∈Ij≡h(i)(Ranh X)( j) =Z
i∈I

[J( j, h(i)) ⇒ X(i)] ∼=NSucc : (LanS Fin)( j) → Fin( j)is mathematically equivalent to give
Succ : Fin( j) → Fin(S( j)).
The Lan encoding is thus equivalent to the original deﬁnition.

This fact was used in arguing for the existence of initial algebras.
This adjointness is an instance of another well-known adjointness characterising Kan extensions:(Lanh X)( j) =That is, precomposition with S in the codomain can be transported
to left Kan extension along S in the domain2 . Hence, by adjointness, to give

6.3

Henry Ford and Lan encodings

We observe that the Henry Ford and Lan encodings are equivalent.
Indeed, using that (LanS Fin)( j) ∼= ∑i∈U, j≡S(i) Fin(i), one equivalently has thati∈Uj≡S(i)

This is a set-theoretical expression of the Henry Ford encoding
Succ :: (j ~ S i) => Fin i -> Fin jstating “you can have any j you like, as long as it’s S(i) (forsome i)”.
6.4 Polynomial functor approach
The polynomial functor approach structurally subsumes the Henry
Ford and Lan approaches. We explain this in the light of the previous example.
Recall that the polynomial associated to the constructor
Succ :: Fin a -> Fin (S a)∏ X(i) = Πh (X)( j)isSucc = U oi∈Ij≡h(i)

Note that a set J is considered as a discrete category. Hence thehomset J(h(i), j) is either empty or consists only of the identity,
which entails the equality constraining j ≡ h(i).
Lan encoding for GADTs. Johann and Ghani have studied atechnique to provide initial-algebra semantics for GADTs using
left Kan extensions (Johann and Ghani 2008). Their approach is to
reduce the problem to the case of ordinary initial-algebra semantics
of ADTs. For example, in this theory, the GADT Fin is transformed
to the following one
data Fin :: * -> * where
NZero :: Lan S One j -> Fin j
NSucc :: Lan S Fin j -> Fin jdata One j= Onedata Lan h _X j = forall i. Lan (Eql j (h i), _X i)data Eql i jwhere Refl :: Eql i iThis seems mysterious; though, as we proceed to explain, the transformed datatype is equivalent to the original one.
First, the type Lan is an implementation of the left Kan extension formula for Lanh X( j) as ∑i∈U ( j ≡ h(i)) × X(i). The
set-theoretic sum with equality is implemented by an existential
type (NB: this forall means ∃) with the equality type Eql on
Haskell types.
Second, since Lanh is left adjoint to − ◦ h, there is a one-to-one
correspondence as follows
f : Fin → Fin ◦ S
fˇ : LanS Fin → Fin∑ Fin(i) → Fin( j).

NSucc :

(5)

id

U

id /
U

S

/U .

Its associated polynomial can be presented in the following threeequivalent forms∑|

X(i) ∼=i∈U, j≡S(i){z= ΣS X( j)}= ΣS Πid id∗ (X)( j) .
∑ ( j ≡ S(i)) × X(i) ∼

|

i∈U

{z

∼
= LanS X( j)

}

|

{z

}

= FSucc X( j)It is from these that the three approaches to modelling the type ofSucc arise; namely(Henry Ford encoding)∑i∈U, j≡S(i) Fin(i) → Fin( j)(Lan Encoding)

LanS Fin( j) → Fin( j)(Polynomial Functor)

FSucc Fin( j) → Fin( j)The Henry Ford and Lan encodings are just ways in which totransfer indexing structure from the codomain to the domain. As
such, then, they correspond to the polynomial functor approach
restricted to polynomials of the form
Io

id

I

id /
I

c

/J.

What is the advantage of the polynomial functor approach?
There are at least three advantages.
2 This is the fundamental principle underlying adjunctions (and Galois con-nections). Currying may be the most well-known adjunction for functional
programmers:
f : A → (B ⇒C)(6)fˇ : A × B → C
Observe the formal similarity between (5) and (6).

[I] The ﬁrst advantage resides in the general form
Io

d

E

p

/B

c

/J

taken by polynomials, that allows one to express varying multi-ary
forms for the argument types of a constructor. This has been a main
topic of the paper. For instance, we saw in §3.1 that Simple GADTs
are modelled by a polynomial of the form
Un o[d1 , . . . , dk ]kU l+m∇k/ U l+mcπldoes not only sufﬁces to model total functional programming withinductively deﬁned datatypes, but also with coinductively deﬁned
ones. Indeed, since d ∗ and Π p preserve limits, and Σc preserves
limits of ωop -chains, it follows that every polynomial functors has aﬁnal coalgebra. These are non-well-founded data structures. Hence,
the lazy datatypes of Haskell and the codata feature of Agda might
be modelled in this setting. The details are left as future work.
6.7 Further related work

/ Un .

An algebra for the associated polynomial functor is an indexed
set X together with an indexed function∑ X(d1 (i)) × · · · × X(dk (i)) → X( j)i∈Uj≡c(i)

that provides a k-ary constructor with varying indexing as speciﬁedby each of the di . As shown in §3.3 and §4.2, more involved forms
for the domain (e.g. with dependent function spaces) can be also
expressed.
[II] The second more important advantage is that every polynomial
functor has an initial algebra constructed by (a possibly transﬁnite)
iteration. This property is not enjoyed by the Henry Ford and Lan
approaches. In them initial algebras are only guaranteed when thearguments to Σ or Lan are well-behaved. Hence the polynomial
functor approach is generic, and more appropriate than the othertwo approaches for modelling GADTs and IFs; making clear thepolynomial character of these datatypes.
[III] The third prospective advantage is the generality of the framework. The original notions of polynomial and polynomial functor (Gambino and Hyland 2003) are more general that consideredhere and were developed within an ambient lccc (locally cartesianclosed category), viz. a category for which every slice category iscartesian closed. The slice categories of the ambient lccc are used
for indexing, and polynomial functors are induced by means of adjoints Σh a h∗ a Πh between slices available for every map h. The
set-theoretic setting is the special case for the lccc Set.
While in this paper we have restricted attention to the settheoretic setting, it is interesting to consider domain-theoretic settings (i.e. categories of CPOs) and more involved models of higherorder polymorphism that more tightly match with Haskell. In thisrespect, lcccs may not be general enough and the more generalclosed comprehension categories may be more appropriate (Jacobs 1999, Sec. 10.6). These cover the domain-theoretic case andmodel dependent sums, reindexing, dependent products, and comprehension. As such, thus, they support our polynomial modellingof GADTs and IFs. This direction will be pursued in future work.
6.5 On comprehension
The construction of the set {{Q}} for an indexed set Q of §3.2 canbe understood from various categorical viewpoints. While this fact
has not been used explicitly in the paper, it might be useful for further generalisation and so we note it here. For presheaves, this construction was ﬁrst used by Yoneda and is often called the categoryof elements. More generally, it is also seen as the Grothendieckconstruction of an indexed category with the projection π forming
a ﬁbration. The notation {{−}} is taken from that for “comprehension” in a comprehension category (Jacobs 1999, Sec. 10.4.7).
6.6 Coinductive datatypes
We have chosen the set-theoretic setting in this paper to concretely
show the correspondence between datatype declarations, polynomials, and polynomial functors with minimal categorical notions,and aiming at the application to generic programming. This setting

Gambino and Hyland introduced dependent polynomial functors
between slices of an ambient lccc and show that they have initial
algebras provided that the ambient category admits W-types (Gambino and Hyland 2003). In this paper, we reveal the polynomials
for GADTs and IFs, and thereby provide a simple and direct initialalgebra semantics by means of dependent polynomial functors thatgeneralise the polynomial functors for ADTs. This characterisation
is well-suited for exchanging technologies between functional programming and type theory.
The mathematics of polynomial functors is investigated in (Kock2009; Gambino and Kock 2010). This work might be useful for further applications to GADTs and IFs with our analysis.
Inductive Families were formulated by (Dybjer 1994). (Dybjer and Setzer 2003) gave an initial-algebra characterisation of
inductive-recursive deﬁnitions, which covers all IFs. Since oneneeds to model an extra inductive-recursive feature, the form offunctors for IFs is not that clear in that presentation.
Indexed containers (Altenkirch and Morris 2009) are a typetheoretic rendering of dependent polynomial functors. Morris andAltenkirch gave a type-theoretic characterisation showing that indexed containers can express IFs.
Differentiation has been considered for generalised species ofstructures (Fiore 2005) and for (non-indexed) containers (Abbott
et al. 2005). In both cases, derivatives can be characterised aslinear exponentials. This extends to dependent polynomial functors
between categories of indexed sets.
There are a number of works on generic programming withindependent type systems based on modelling dependent types in adependent type theory (Altenkirch and McBride 2002; Benke et al.
2003; Chapman et al. 2010). These models are very often foundedon some mathematical semantics of dependent type theory, such as(indexed) induction-recursion (Dybjer and Setzer 2003, 2006) orcontainers (Abbott et al. 2005; Altenkirch and Morris 2009), implementing these semantics at the level of type theory. The polynomial
functor approach will be also realised in this way. This will serve asa basis for transporting generic functional programming techniques
to dependent type theory.

Acknowledgments
We thank Tarmo Uustalu and Varmo Vene for discussions related
to a shapely typed zipper in Agda, and Makoto Takeyama for
information about the Henry Ford encoding. Makoto Hamana is
supported in part by the JSPS Grant-in-Aid for Scientiﬁc Research(22700004).

References
M. Abbott, T. Altenkirch, and N. Ghani. Representing nested inductive
types using W-types. In ICALP’04, pages 59–71, 2004.
M. Abbott, T. Altenkirch, C. McBride, and N. Ghani. ∂ for data: Differentiating data structures. Fundam. Inform., 65(1-2):1–28, 2005.
A. Abel, R. Matthes, and T. Uustalu. Iteration and coiteration schemes forhigher-order and nested datatypes. Theor. Comput. Sci., 333(1-2):3–66,
2005.
J. Adamek. Free algebras and automata realizations in the language ofcategories. Comment. Math. Univ. Carolina, 15(589602), 1974.

M. D. Adams. Scrap your zippers: A generic zipper for heterogeneous
types. In WGP ’10, pages 13–24. ACM, 2010.
T. Altenkirch and C. McBride. Generic programming within dependently
typed programming. In Generic Programming, pages 1–20, 2002.
T. Altenkirch and P. Morris. Indexed containers. In LICS’09, pages 277–
285, 2009.
M. Benke, P. Dybjer, and P. Jansson. Universes for generic programs andproofs in dependent type theory. Nord. J. Comput., 10(4):265–289, 2003.
R. Bird and R. Paterson. Generalised folds for nested datatypes. Form. Asp.
of Comput., 11(2):200–222, 1999a.
R. Bird and R. Paterson. De Bruijn notation as a nested datatype. J. of
Funct. Program., 9(1):77–91, 1999b.
A. Bove and P. Dybjer. Dependent types at work. In LerNet ALFA Summer
School, pages 57–99, 2008.
J. Chapman, P. Dagand, C. McBride, and P. Morris. The gentle art oflevitation. In Proc. of ICFP’10, pages 3–14, 2010.
N. A. Danielsson, J. Hughes, P. Jansson, and J. Gibbons. Fast and loose
reasoning is morally correct. In Proc. of POPL’06, pages 206–217, 2006.
P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440–465,
1994.
P. Dybjer and A. Setzer. Indexed induction-recursion. J. Log. Algebr.
Program., 66(1):1–49, 2006.
P. Dybjer and A. Setzer. Induction-recursion and initial algebras. Ann. Pure
Appl. Logic, 124(1-3):1–47, 2003.
M. Fiore. Mathematical models of computational and combinatorial structures. In Proc. FOSSACS 2005, LNCS 3441, pages 25–46, 2005.
M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In
Proc. of 14th Annual Symposium on Logic in Computer Science, pages
193–202, 1999.
N. Gambino and M. Hyland. Wellfounded trees and dependent polynomial
functors. In TYPES’03, pages 210–225, 2003.
N. Gambino and J. Kock. Polynomial functors and polynomial monads.
ArXiv:0906.4931, 2010.
N. Ghani, P. Johann, T. Uustalu, and V. Vene. Monadic augment andgeneralised short cut fusion. In Proc. of ICFP’05, pages 294–305, 2005.
T. Hagino. A typed lambda calculus with categorical type constructors. In
Pitt et al., editor, Category Theory in Computer Science’87, LNCS 283,
pages 140–157. Springer-Verlag, 1987.
R. Hinze. Fun with phantom types. In The Fun of Programming, pages
245–262. Palgrave Macmillan, 2003.
R. Hinze. Adjoint folds and unfolds. In Proc. of MPC’10, pages 195–228,
2010.
R. Hinze and J. Jeuring. Generic Haskell: Practice and theory. In Generic
Programming, LNCS 2793, pages 1–56, 2003.

B. Jacobs. Categorical Logic and Type Theory. Studies in Logic and theFoundations of Mathematics 141. North Holland, Elsevier, 1999.
P. Jansson and J. Jeuring. Polyp - a polytypic programming language. In
POPL, pages 470–482, 1997.
P. Johann and N. Ghani. Foundations for structured programming withGADTs. In Proc. of POPL’08, pages 297–308, 2008.
S. Katsumata and S. Nishimura. Algebraic fusion of functions with anaccumulating parameter and its improvement. J. Funct. Program., 18(5-6):781–819, 2008.
J. Kock. Notes on polynomial functors. Manuscript, version 2009-08-05,
2009.
J. Launchbury and T. Sheard. Warm fusion: Deriving build-cata’s fromrecursive deﬁnitions. In Proc. of FPCA’95, pages 314–323, 1995.
F.W. Lawvere. Adjointness in foundations. Dialectica, pages 281–296,
1969.
S. Mac Lane. Categories for the Working Mathematician, volume 5 of
Graduate Texts in Mathematics. Springer-Verlag, 1971.
S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First
Introduction to Topos Theory. Springer-Verlag, 1994.
C. McBride. Epigram: Practical programming with dependent types. In
Advanced Functional Programming, pages 130–170, 2004.
C. McBride. The derivative of a regular type is its type of one-hole contexts.
Manuscript, 2001.
C. McBride. Dependently Typed Programs and their Proofs. PhD thesis,
University of Edinburgh, 1999.
E. Meijer, M. M. Fokkinga, and R. Paterson. Functional programming withbananas, lenses, envelopes and barbed wire. In Proc of FPCA’91, pages
124–144, 1991.
A. Morihata, K. Matsuzaki, Z. Hu, and M. Takeichi. The third homomorphism theorem on trees: downward & upward lead to divide-andconquer. In POPL’09, pages 177–185, 2009.
U. Norell. Towards a practical programming language based on dependent
type theory. PhD thesis, Chalmers University of Technology, 2007.
U. Norell. Dependently typed programming in Agda. In Advanced Functional Programming, pages 230–266, 2008.
N. Oury and W. Swierstra. The power of Pi. In Proc. of ICFP’08, pages
39–50, 2008.
T. Schrijvers, S. L. Peyton Jones, M. Sulzmann, and D. Vytiniotis. Complete and decidable type inference for GADTs. In ICFP’09, pages 341–
352, 2009.
T. Sheard and L. Fegaras. A fold for all seasons. In Proc. of FPCA’93,
pages 233–242, 1993.
M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive
domain equations. SIAM J. Comput, 11(4):763–783, 1982.

Z. Hu, H. Iwasaki, and M. Takeichi. Deriving structural hylomorphisms
from recursive deﬁnitions. In Proc. of ICFP’96, pages 73–82, 1996.

A. Takano and E. Meijer. Shortcut deforestation in calculational form. In
Proc. of FPCA’95, pages 306–313, 1995.

G. Huet. Functional pearl: The zipper. Journal of Functional Programming,
6(5):549–554, 1997.

N. Yoneda. On Ext and exact sequences. Jour. Fac. Sci. Univ. Tokyo, pages
507–576, 1960.