Slicing It

Conor McBride

Utrecht, Portland, Nottingham, 2009

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 superstructure which frame arbitrary substructures in some way: fmap lifts functions on substructures to functions on superstructures — acting on the substructures, but preserving their framing. For example, lists are superstructures for their elements:

instance Functor [] where
  fmap f [] = []
  fmap f (x:xs) = f x : fmap f xs

The fixpoint construction builds recursive types (think trees) from functors by identifying superstructures with substructures: each node frames its children.

The iterator takes an algebra — a method of reducing a superstructure of values to a value — and uses it to reduce a whole tree to a value. The plan is: unpack the root substructure; turn its children into values by recursive iteration; feed result to algebra.

For example,

data ListB x xs = Nil | Cons x xs
instance Functor (ListB x) where
  fmap f Nil = Nil
  fmap f (Cons x xs) = Cons x (f xs)
and 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 two sorts of substructure — e.g., ‘elements’ and ‘subtrees’. These have Bifunctor structure.

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 just a functor from a product category.

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
TorF u s {True} → TorF v t {True} (that's u→v, up to iso), or to
TorF u s {False} → TorF v t {False} (that's s→t, up to iso). We've found the right notion of arrow to express bifunctors as a kind of functor (but not the *→* kind).

(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
  Top :: Has {x:xs} {x}
  Pop :: Has {xs} {y} → Has {x:xs} {y}

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.

Conor McBride 2009