0.0

Generic Programming with Adjunctions Ralf Hinze Computing Laboratory, University of Oxford Wolfson Building, Parks Road, Oxford, OX1 3QD, England [email protected] http://www.comlab.ox.ac.uk/ralf.hinze/

March 2010

University of Oxford — Ralf Hinze

1-172

Generic Programming with Adjunctions

1.0

Part 1

Prologue

University of Oxford — Ralf Hinze

2-172

Generic Programming with Adjunctions

1.0

1.0

Outline

1. What? 2. Why? 3. Where? 4. Overview

University of Oxford — Ralf Hinze

3-172

Generic Programming with Adjunctions

1.1

What?

1.1

What?

Haskell programmers have embraced • functors, • natural transformations, • initial algebras, • final coalgebras, • monads, • ...

It is time to turn our attention to adjunctions.

University of Oxford — Ralf Hinze

4-172

Generic Programming with Adjunctions

1.2

Why?

1.2

Catamorphism

f = Lb M

⇐⇒

University of Oxford — Ralf Hinze

f · in = b · F f

5-172

Generic Programming with Adjunctions

1.2

Why?

1.2

Banana-split law

LhM Lk M

= L h · F outl k · F outr M

University of Oxford — Ralf Hinze

6-172

Generic Programming with Adjunctions

1.2

Why?

1.2

Proof of banana-split law

=

=

=

=

=

(L h M L k M ) · in

{ split-fusion }

L h M · in L k M · in

{ fold-computation }

h · F LhM k · F Lk M

{ split-computation }

h · F (outl · (L h M L k M )) k · F (outr · (L h M L k M )) { F functor }

h · F outl · F (L h M L k M ) k · F outr · F (L h M L k M ) { split-fusion }

(h · F outl k · F outr) · F (L h M L k M ) University of Oxford — Ralf Hinze

7-172

Generic Programming with Adjunctions

1.2

Why?

1.2

Example: total

data Stack = Empty | Push (Nat, Stack) total : Stack → Nat total (Empty) =0 total (Push (n, s)) = n + total s

University of Oxford — Ralf Hinze

8-172

Generic Programming with Adjunctions

1.2

Why?

1.2

Two-level types

Abstracting away from the recursive call. data Stack stack = Empty | Push (Nat, stack) instance Functor Stack where fmap f (Empty) = Empty fmap f (Push (n, s)) = Push (n, f s) Tying the recursive knot. newtype µf = In {in◦ : f (µf )} type Stack = µStack

University of Oxford — Ralf Hinze

9-172

Generic Programming with Adjunctions

1.2

Why?

1.2

Two-level functions

Structure. total : Stack Nat → Nat total (Empty) =0 total (Push (n, s)) = n + s Tying the recursive knot. total : µStack → Nat total (In s) = total (fmap total s)

University of Oxford — Ralf Hinze

10-172

Generic Programming with Adjunctions

1.2

Why?

1.2

Counterexample: stack

stack : (Stack, Stack) → Stack stack (Empty, bs) = bs stack (Push (a, as), bs) = Push (a, stack (as, bs))

University of Oxford — Ralf Hinze

11-172

Generic Programming with Adjunctions

1.2

Why?

1.2

Counterexamples: fac and fib

data Nat = Z | S Nat fac : Nat → Nat fac (Z)