Presented by Felix Klock

Transcribed by Ryan Culpepper

Some examples to start out:

data List a = Nil |
list_size Nil = 0 |

data Tree a = Leaf a |
tree_size (Leaf x) = 1 |

This follows HtDP, but seems redundant. It is not obvious how to pull out common code.

A Functor has two parts: a type constructor and a mapping of functions to functions:

<F, fmap>, where F : * -> *, and fmap : (a -> b) -> (F a -> F b)

The mapping must satisfy laws such as

- fmap id = id
- fmap (f o g) = (fmap f) o (fmap g)

(BF is a bifunctor: BF : * -> * -> *

and bfmap : (a -> b) -> (c -> d) -> (BF a c -> BF b d)

Cartesian product is an example of a bifunctor:

<X, -X-> (note: Felix uses the convention of writing the mapping as the functor name between dashes)

For the purpose of this talk, the real contribution of this paper is the modelling of recursive datatypes as the fixed points of functors, particularly the fixed point of a partially applied bifunctor. Example:

data List a = Nil | Cons a (List a)

FList p r = 1 + (p X r)

If we also have a fixed-point operator mu : (* -> *) -> *

inn : FList a (Mu FList a) => Mu FList a

out : Mu FList a -> FList a (Mu FList a)

for FList to be a functor we also need its fmap:

bflistmap f g = id -+- (f -X- g)

The paper gives a way to get from the data definition and the bifunctor to the mapping. One last remark: think about instantiating (FList p r) where r is not the recursive link: then you get part of the type of the function argument of fold. Example:

FList String Int -> Int

Grammar for functors:

F = F + F | 1 | Const t | F X F | Par | Rec | D @ F

where Par is the type parameter (Int in (Listof Int)), Rec is the recursive argument (the backlink in a HtDP data definition or the result of the recursive call in a fold), and D@F is a datatype applied to a functor.

data Rose a = Fork a (List (Rose a))

FRose = Par X (List @ Rec)

Felix: What's missing from this grammar?

Peter: Function types!

How do you fold over function types? (Matthias elaborates: How do you take a function space apart?)

You do something like take 2 functions, one which is a combiner and one which is an inverse combiner...

Meijer says on his homepage: Now we've figured out how to do this, but we still don't know when we'd want to.

data Mu f a = In (f a (Mu f a))

flatten :: Regular d => d a -> [a]

(A datatype is regular if recursive uses of its type constructor are always applied to the same types as its definition's arguments. Eg: the datatype above defines Mu f a, and the only recursive use of Mu is an application Mu f a, so this is regular.)

flatten = cata fl

(where cata is one of Meijer's recursion combinators, and fl will be polytypic)

If used on a tree, this really means

flatten

Sam: Isn't cata just fold?

Felix: No, fold is for lists; cata is for anything.

polytypic fl :: f a [a] -> [a] (second arg is result now)Where the line above either fl fl really means either fl

= case f of

f + g -> either fl fl

f X g -> \(x,y) -> (fl x) ++ (fl y)

() -> \x -> []

Par -> \x -> [x]

Rec -> \x -> x

d @ g -> concat o flatten o pmap fl

Con t -> []

fl

It works! You've just got to figure out what to put in the slots of the case expression.

It's like magic, almost. It has some drawbacks, though. For example, consider the case of expression trees. There an addition tree and a multiplication tree will have the same shape, but you probably want to do different things with them. So they hacked in some extra arguments to let you know the order of the clauses, and ...