1A Foundation for GADTs
and Inductive Families
Dependent Polynomial Functor Approach

Makoto Hamana
Gunma University, Japan

Joint work with
Marcelo Fiore, University of Cambridge

WGP’11, 18 September, 2011.

2This WorkB Dependent polynomial functor representation ofGADTs and Inductive Families, uniformly
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.
GADTs/IFs in these papers
Aim I Recipes for dependent polynomials for GADTs/IFs.
“mathematical codes”

3

Related Work
Johann and Ghani,
Foundations for structured programming with GADTs,POPL’08.

Our dependent polynomial functor approach
B Reﬁnes thisB Uniﬁed framework to deal with GADTs and IFs

4ADTs and Programming Techniques
ADTs have a solid foundation: ordinary polynomial functors
It is the basis of 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5This Talk
To extend this story to GADTs[I] Polynomial representation of GADTs
that generates dependent polynomial functors[II] Zippers for GADTs (and IFs)

ADTs

/ GADTspolynomial ft.s

dependent polynomials & ft.s

zippers, etc.

6

Review: Meaning of Algebraic Datatypes
data List = Nil| Cons Int List
B Assumption: set-theoretic models
B Semantics = the initial F -algebra α : F A∼=-AF : Set → Set
F (X) = 1 + Z × X
B Point: polynomial functor F characterises List
B How can we extend this to GADTs?

7

I. How to Model GADTs

8GADTs with Type-level Data
B Bounded natural numbers
data Z
data S adata Fin :: * -> * where
Zero :: Fin (S a)Succ :: Fin a -> Fin (S a)9Modelling Fin
data Fin :: * -> * where
Zero :: Fin (S a)Succ :: Fin a -> Fin (S a)
B What is the polynomial functor for Fin?
UU
B Answer: F:Set
→Set
F in

FF in (X)(S a) = 1 + X(a)FF in (X)(a) = ∅otherwiseU[[Fin]] = the initial FF in -algebra Fin ∈ Set
B How to derive? What are “polynomials”?
B Dependent polynomials10The Universe of DiscourseADTs

Set

GADTs
ÃSetU

the category of sets

the category of U -indexed setspolynomial ft.

dependent polynomial ft.

11Category of Indexed Sets
B Category SetU

for an arbitrary set U• Objects: A : U → Set
i.e. U -indexed sets {A(i) | i ∈ U }• Arrows: U -indexed functions f : A → B,
i.e. a family of functions (f (i) : A(i) → B(i) | i ∈ U )B Important functors: given a function h : I → J,∑ΣhΣh (A)(j) = i∈I A(i)⊥∗JSet ¾ hSet
⊥ ΠhI

j≡h(i)h∗ (A)(j) = A(h(j))∏Πh (A)(j) = i∈I A(i)Lawvere’s quantiﬁers by adjointness [1969]j≡h(i)

12

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

B NB. the original version uses a lccc and slices

13

Dependent Polynomials [Gambino-Hyland’03]
B Def. The dependent polynomial functor FP
associated to a dependent polynomial P = (d, p, c) is
deﬁned byIJ

FP : Set → Set∗

def

FP (X) = Σc (Πp (d (X))).
B i.e.
FP (X)(j) =∑∏e∈Eb∈Bj≡c(b) b≡p(e)X(d(e))

14

Modelling Findata Fin :: * -> * where
Zero :: Fin (S a)Succ :: Fin a -> Fin (S a)
B Model constructors as polynomials
Zero =Uo!

Succ =Uoid∅U!

/U

S/Uid

/U

S/U

15

Modelling Fin
data Fin :: * -> * where
Zero :: Fin (S n)Succ :: Fin n -> Fin (S n)
B Sum of polynomials is again a polynomial
def

F in = Zero + Succ
B Dependent polynomial functor FF in : SetU → SetU
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∈Un≡S a

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

a∈Un≡S ais equivalent to the deﬁnition by pattern-matching
UFF in : Set

U→ Set

FF in (X)(S a) = 1 + X(a)FF in (X)(a) = ∅otherwise

B Initial algebra is constructed by repeated applications of FF inThm. [Gambino-Hyland’03]
Every dependent polynomial functor has an initial algebra.

17Example: Fin(1)data Fin :: * -> * where
Zero :: Fin (S n)Succ :: Fin n -> Fin (S n)(2) Polynomial
Zero =Uo!

Succ =Uoid∅U!

/US/ U.

id/US/ U.

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

18

General Case: Simple GADTn

data D : ∗ → ∗ wherelm

K : ∀α , ² . D(d1 [α, ²]) → · · · → D(dk [α, ²]) → D(c[α])B Polynomial(functions di : U l+m → U n ,Un o [d1 ,...,dk ]kUl+mc : U l → U n)∇k/

Ul+mcπ l/ Un• “Co-diagonal” ∇k = [idU , . . . , idU ] : kU → UUnUnB Dependent polynomial functor FD : Set→ Set∑FD X(m) =X(d1 (j)) × · · · × X(dk (j))
j∈Um≡c(j)

19

II. Application: Zippers

20Zippers
B G. Huet, Functional Pearl: The Zipper,
Journal of Functional Programming, 1997.
B A data structure for navigating a tree freely
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 GADTs/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)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.]

22Zipper Datatype
B For dependent polynomial functor F for an GADT/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 GADTs
B that automatically generates dependent polynomial functors
B Zippers for GADTs by diﬀerentiation

Reference
Comanion slides at AIM-DTP’11 Shonan Workshop
are available from my homepage
I More on inductive families

24

Related Work
1. Initial algebras for GADTs. Johann and Ghani [POPL’08]
B Use Left Kan extension for representing the codomains
Lanh a (− ◦ h) a Ranh
Ours: Dependent polynomial functors
B Use all constructs, i.e. more structured
Σh a h∗a Πh2. Indexed containers. Altenkirch and Morris [LICS’09]
B Type theoretic characterisations
B Mathematically equivalent
3. Indexed functors. Löh, Magalhães [WGP’11]

25

Relationships¾(1)'Cont(I, J )@@@@interpretation @C[[−]] @@@@R

(3)

I-P oly(I, J )(2)¡¡¡¡¡ poly. funct.
¡ F( )¡¡ª¡J[Set , Set ](1) Indexed containers, Altenkirch and Morris(2) Dependent polynomials, Gambino, Hyland; Hamana, Fiore(3) Indexed functors, Löh, MagalhãesProblem I Indexed functor may not have an initial algebra