The magic words are “One, Two, Four, Eight: time to exponentiate!”. | |

I could give up laziness tomorrow... or maybe the day after, but I couldn't cope without abstraction at higher kinds. | |

The Functor class captures notions of instance Functor [] where The fixpoint construction builds recursive types (think trees) from functors by identifying superstructures with substructures: each node frames its children.
The iterator takes an For example, data ListB x xs = Nil | Cons x xsadmits instance Functor (ListB x) whereand you'll find that Fix (LIST x) behaves a lot like [a]. Except that Fix (LIST x) is not obviously functorial in x. unfold :: Functor f ⇒ (t → f t) → t → Fix f | |

You can get out of this pickle by considering superstructures
parametrized by We take a parametrized fixpoint, instantiating the second sort of substructure recursively, but remaining abstract in the first. We get an iterator (and a coiterator as before). The ‘P’ in ‘PFix’ is silent, and similarly for ‘PIn’, ‘pfold’, and ‘punfold’ — no unintended. The crucial point, though, is that we also get that the resultant parametrized recursive structure is an instance of the Functor class. There's a special place we put people who implement fmap for (PFix b) as a pfold: it's called Oxford. | |

The rest of us do it like this. | |

Here's the ListB example. Note that there's a Bifunctor kit which you can use to build lots of your favourite recursive containers. Jeremy Gibbons wrote some lovely notes about programming in this ‘origami’ style for the 2006 Spring School on Data-Generic Programming. | |

Haskell makes a fair enough start at expressing categorical concepts useful for programming, but sometimes the naming is a bit askew. By calling the class for things in *→* with fmap ‘Functor’, we implicitly lock ourselves into the category with objects in * and arrows from σ to τ in σ→τ. The Arrow abstraction begins to undo some of the damage, but we still haven't really broken out of it. | |

Categorists use the word ‘just’ the way lepidopterists use cyanide.
A bifunctor is What do you mean you don't have product categories? But we can turn this product into an exponential... ...if only we could find a kind that behaved enough like Bool. Let's just pretend that we do. A morphism s ⊆ t (in ascii, I write s :-> t) between s,t :: {ι}→* is an index-respecting map between indexed sets, or Curry-Howardly, an inclusion of predicates. This TorF thing is kind of ‘if..then..else..’ for types (with the condition shoogled to the end, ready to be left out in a partial application).
The index-respecting maps TorF u s ⊆ TorF v t are polymorphic
functions which can be specialized to (Sorry I wrote a blue ⊆ by mistake — I write defined things (e.g., type synonyms) in green.) | |

Just revisiting the slide for kinds to add the blue braces of upward mobility which turn types (inhabitants of kind *) into kinds. I'll tell you which expressions get to live at the type level and inhabit these kinds on the next slide, but you can bet we'll have {True}, {False} :: {Bool}. I've left out another thing I know I'll need: kinds polymorphic in type-level stuff. ∀x::κ. κNote that I don't get to abstract kinds themselves this way. I just
get to form kinds like this (list membership, or typed de Bruijn
indices from Altenkirch and Reus, CSL 1999)
data Has :: ∀x::*. {[x]}→{x}→* where | |

You get to put first-order constructor forms in type-level expressions. Don't worry about termination — they've already terminated. Also, the same unification which gets used for type inference, GADT pattern matching, etc, works just as well for these things. I've just yanked some tubes out of the middle of the machine and gaffer-taped them into the wrong holes, but the machine still works — even better, actually. It's like what dentists do to their cars, for a laugh. | |