Generic Programming with Adjunctions - Department of Computer ...

Overview 1.4. 1.4 Overview. • Part 0: Prologue. • Part 1: Category theory. • Part 2: Adjoint folds and unfolds. • Part 3: Adjunctions. • Part 4: Application: Type fusion.
544KB Sizes 7 Downloads 224 Views
Generic Programming with Adjunctions

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)