1Dependent Polynomial Functors
for Inductive Families

Makoto Hamana
Gunma University, Japan

Joint work with
Marcelo Fiore, University of Cambridge
AIM-DTP joint day
14 September, 2011.

2This WorkB Dependent polynomial functor representation ofInductive Families
Background
N. Gambino and M. Hyland,
Wellfounded Trees and Dependent Polynomial Functors, TYPES’03.
J. Kock, Notes on Polynomial functors,
manuscript, 412 pages, Version 2009-08-05.

2This WorkB Dependent polynomial functor representation ofInductive Families
Background
N. Gambino and M. Hyland,
Wellfounded Trees and Dependent Polynomial Functors, TYPES’03.
J. Kock, Notes on Polynomial functors,
manuscript, 412 pages, Version 2009-08-05.

Problem I Not clear what are dependent polynomials for IFs.
in these papers
Aim I Recipes for giving dependent polynomials for IFs

3ADTs and Programming Techniques
ADTs have a solid foundation: ordinary polynomial functors
It is the basis for various programming techniques:
B Fold and fusion techniques[Meijer et al.’91][Launchbury,Sheard’95][Takano,Meijer’95][Hu et al.’96][Katsumata,Nisimura’08][Ghani et al.’05][Hinze’10]

B Polytypic programming [Jansson,Jeuring’97]
B Generic Haskell [Hinze,Jeuring’03]
B Program reasoning [Danielsson et al.’06]
B Generic zippers [McBride’01][Morihata et al.’09]
I Polynomial functor representation is useful4This Talk
To extend this story to IFs[I] Polynomial representation of Inductive Families
that generates dependent polynomial functors[II] Zippers for Inductive Families

ADTs/ Inductive Families

polynomial ft.s

dependent polynomials & ft.s

zippers, etc.

5

Review: Meaning of Algebraic Datatypes
data List = Nil| Cons Int List
B Semantics = the initial F -algebra α : F A∼=-A

F : Set → Set
F (X) = 1 + Z × X
B Point: polynomial functor F characterises List
B How can we extend this to IFs?

6

I. How to Model Inductive Families

7

Inductive Families
B Bounded natural numbers
data Nat : Set where
Z : Nat
S : Nat -> Natdata Fin : Nat -> Set where
Zero : {n : Nat} -> Fin (S n)Succ : {n : Nat} -> Fin n -> Fin (S n)

B Fin n types natural numbers below n
B Nat is characterised as the initial 1 + (−)-algebra N ∈ Set

8Modelling Fin
data Fin : Nat -> Set where
Zero : {n : Nat} -> Fin (S n)Succ : {n : Nat} -> Fin n -> Fin (S n)

B What is the polynomial functor for Fin?

8Modelling Fin
data Fin : Nat -> Set where
Zero : {n : Nat} -> Fin (S n)Succ : {n : Nat} -> Fin n -> Fin (S n)

B What is the polynomial functor for Fin?
NN
B Answer: F:Set→Set
F in

FF in (X)(S a) = 1 + X(a)FF in (X)(Z)=∅N[[Fin]] = the initial FF in -algebra Fin ∈ Set
B How to derive? What are “polynomials”?
B Dependent polynomials

9The Universe of DiscourseADTs

Inductive Famines
Fam(Set)SetÃ

SetIfor every I ∈ Set

the category of sets

the categories of indexed setspolynomial ft.

dependent polynomial ft.

10Category of Indexed Sets
B Category SetI

for an arbitrary set I• 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)

10Category of Indexed Sets
B Category SetI

for an arbitrary set I• 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)
B Important functors: given a function h : I → J,Σh%∑∗IJΣh (A)(j) =A(i)Set o h Set
9i∈IΠhj≡h(i)∏∗h (A)(j) = A(h(j))Πh (A)(j) =A(i)i∈Ij≡h(i)Lawvere’s quantiﬁers by adjointness [1969]

11

Dependent Polynomials [Gambino-Hyland’03]
B Def. A (dependent) polynomial P isa triple P = (d, p, c) of functions between sets
IodEp/Bc/J .

11

Dependent Polynomials [Gambino-Hyland’03]
B Def. A (dependent) polynomial P isa triple P = (d, p, c) of functions between sets
dIopEc/B/J .

B Then, one obtains a functorISetd∗ /ESet

Πp/

BSet

Σc /JSet

11

Dependent Polynomials [Gambino-Hyland’03]
B Def. A (dependent) polynomial P isa triple P = (d, p, c) of functions between sets
dIopEc/B/J .

B Then, one obtains a functor
ISetd∗ /ESet

Πp/

BSet

Σc /

JSet

B NB. the original version uses a lccc and slices

12

Dependent Polynomials [Gambino-Hyland’03]
B Def. The dependent polynomial functor FP
associated to a dependent polynomial P = (d, p, c) is
deﬁned byIJFP : Set → Set∗defFP (X) = Σc (Πp (d (X))).
B i.e.
FP (X)(j) =∑∏e∈Eb∈Bj≡c(b) b≡p(e)X(d(e))

13

Modelling Fin
data Fin : Nat -> Set where
Zero : {n : Nat} -> Fin (S n)Succ : {n : Nat} -> Fin n -> Fin (S n)
B Model constructors as polynomials
Zero =No!

Succ =

Noid∅!

/NS

/ N.

Nid

/NS

/ N.

13

Modelling Fin
data Fin : Nat -> Set where
Zero : {n : Nat} -> Fin (S n)Succ : {n : Nat} -> Fin n -> Fin (S n)
B Model constructors as polynomials
Zero =No!

Succ =Noid∅!

/NS/ N.

Nid/NS/ N.

B The sum of polynomials is again a polynomial
def

F in = Zero + Succ

14Modelling Fin
data Fin : Nat -> Set where
Zero : {n : Nat} -> Fin (S n)Succ : {n : Nat} -> Fin n -> Fin (S n)
B Sum of polynomials is again a polynomial
def

F in = Zero + Succ
B Dependent polynomial functor FF in : SetN → SetN
FF in (X)(n) = FZero+Succ (X)(n)= FZero (X)(n) + FSucc (X)(n)∗∗= ΣS Π! ! (X)(n) + ΣS Πid id (X)(n)∑(1 + X(a)))=a∈Nn≡S a

15Modelling Fin
B Dependent polynomial functor
FF in (X)(n) =∑(1 + X(a)))

a∈Nn≡S ais equivalent to the deﬁnition by pattern-matchingNN

FF in : Set → Set

FF in (X)(S a) = 1 + X(a)FF in (X)(Z) = ∅B Initial algebra is constructed by repeated applications of FF inThm. [Gambino-Hyland’03]
Every dependent polynomial functor has an initial algebra.

16Example: Fin(1) data Fin : Nat -> Set whereZero : {n : Nat} -> Fin (S n)Succ : {n : Nat} -> Fin n -> Fin (S n)(2) Polynomial
Zero =No!

∅!

/NS/ N.

Succ =NoidNid/NS/ N.

(3) Dependent polynomial functor FF in : SetN → SetN∑
FF in (X)(n) =(1 + X(a)))
a∈Nn≡S a

17

General Case: Simple Inductive Family
data D : I → Set whereK : (j : J) → D(d1 [j]) → · · · → D(dk [j]) → D(c[j])B Polynomial(functions di : J → I,
[d1 ,...,dk ]oIkJ∇k/Jc : J → I)c/I• “Co-diagonal” function ∇k = [idJ , . . . , idJ ] : kJ → J

B Dependent polynomial functor FD : SetI → SetI
∑FD X(m) =X(d1 (j)) × · · · × X(dk (j))
j∈Jm≡c(j)

18

More General: Basic Inductive Family(1)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])(2) PolynomialIo(d = [d1 , . . . , dk ])d{S1 + · · · + Sk }(3) Dependent
polynomialfunctor∑∏FD X(u) ∼=π/ {E}}X(d1 (j, e, s)) × · · · ×j∈J, e∈E(j) s∈S1 (j,e)
u≡c(j)∏cπ/IX(dk (j, e, s))s∈Sk (j,e)

19II. Application: Zippers

20Zippers
B G. Huet, Functional Pearl: The Zipper,
Journal of Functional Programming, 1997.
B A data structure for navigating a tree freely(not only decomposition)
B A zipper = current forcus & lists of depth-one contextsB Generic way to give the type of depth-one contexts

20Zippers
B G. Huet, Functional Pearl: The Zipper,
Journal of Functional Programming, 1997.
B A data structure for navigating a tree freely(not only decomposition)
B A zipper = current forcus & lists of depth-one contexts
B Generic way to give the type of depth-one contexts
B McBride’s ﬁnding• Binary trees F (X) = 1 + X × X• Depth-one contexts F 0 (X) = X + X– diﬀerentiation

B Only for ADTs and polynomial functors
B Extension to IFs and dependent polynomial functors

21Diﬀerentiation
B Dependent polynomial functor F : SetI → SetJ
∑ ∏F (X)(j) =X(d(e))
b∈B e∈Ebj≡c(b)21Diﬀerentiation
B Dependent polynomial functor F : SetI → SetJ
∑ ∏F (X)(j) =X(d(e))
b∈B e∈Ebj≡c(b)B Partial derivative of F with respect to i ∈ IIJ∂i F : Set → Set∑∂i F (X)(j) =e∈Ej≡c(b)∑∏X(d(e))`∈Eb e∈Eb \{`}i≡d(`)• Derived from diﬀerentiation of generalised species[Fiore FOSSACS’05, etc.]

21

Diﬀerentiation
B Dependent polynomial functor F : SetI → SetJ
∑ ∏F (X)(j) =X(d(e))
b∈B e∈Ebj≡c(b)B Partial derivative of F with respect to i ∈ IIJ∂i F : Set → Set∑∂i F (X)(j) =e∈Ej≡c(b)∑∏

X(d(e))`∈Eb e∈Eb \{`}i≡d(`)

cf.
0• (xn ) = nxn−1• (f (x) + g(x))0 = f 0 (x) + g 0 (x)22Zipper Datatype
B For dependent polynomial functor F for an IF,
defZipper(m) = µ F (m) × Ctx (m)∑Ctx (m) ∼∂m F (µ F )(n) × Ctx (n)= 1+n∈I

B Navigation operations are deﬁned accordingly

23Summary
B Polynomial representation of Inductive Families
B that automatically generates dependent polynomial functors
B Zippers for Inductive Families by diﬀerentiation
Reference
Hamana, Fiore. A Foundation for GADTs and Inductive
Families: Dependent Polynomial Functor Approach,
WGP’11, 2011-9-18.

24

Related Work
B Induction-recursion. Dybjer and A. Setzer[Ann. Pure Appl. Logic’03][J. Log. Algebr. Program.’06]• What are functors for inductive recursive deﬁnitions?
• Next step
B Indexed containers. Morris and Altenkirch [LICS’09]• Type theoretic characterisations• Mathematically equivalent25

Containers & Dependent Polynomials
Indexed containers [Morris and Altenkirch’09]• S ∈ SetJ
• P ∈I×∑j∈J Sj → Set(S / P ) ∈ Cont I J

25Containers & Dependent Polynomials
Indexed containers [Morris and Altenkirch’09]• S ∈ SetJ
• P ∈I×∑j∈J Sj → Set(S / P ) ∈ Cont I JCont → P olyπ1πoI∑i,a∈I×Pj∈J Sj

P (i, a) π 2 π /∑j∈JSjπ/J25Containers & Dependent Polynomials
Indexed containers [Morris and Altenkirch’09]• S ∈ SetJ
• P ∈I×∑j∈J Sj → Set(S / P ) ∈ Cont I J
P oly → ContIodpE/Bc/J• c−1 ∈ SetJ
• hd, pi : E → I × B(c−1−1hd, pi/ hd, pi−1: SetI×B) ∈ Cont I J

26Containers & Dependent Polynomials
Both generate the same dependent polynomial functor∗∼=Σc (Πp (d (X)))∑ ∏X(de)“dependent polynomial functor”b∈Bj e∈Eb∼=∏∑b∈Bj e∈∼=X(πe)Pi∈I Ei ,b∑ ∏ ∏X(i)b∈Bj i∈I e∈Ei ,b∼=∑ ∏Ei,b ⇒ X(i)b∈Bj i∈I∼=[[(c−1/ hd, pi−1)]](X)“extension of container”

27

Containers & Dependent Polynomials
B Indexed vs. ﬁbrational−1p: I → Set

⇔p:

∑−1p

(i) → Ii∈I

B Cont → P oly
π1πoI“ﬁbrational”∑i,a∈I×

P (i, a) π 2 π /Pj∈J Sj∑Sjπj∈JB P oly → ContIo(c−1d/ hd, piE−1p/B) ∈ Cont I Jc/J

“indexed”/J