Generic Programming with Adjunctions - Department of Computer ...

Generic Programming with Adjunctions. 0.0. Generic .... Part 4: Application: Type fusion ..... NB Type application and abstraction are invisible in Haskell.
544KB Sizes 10 Downloads 273 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)