FUN with type CTORS
Presented by Felix Klock
Transcribed by Ryan Culpepper
Some examples to start out:
data List a = Nil
| Cons a (List a)
list_size Nil = 0
| (Cons x r) = 1 + list_size r
data Tree a = Leaf a
| Bin (Tree a) (Tree a)
tree_size (Leaf x) = 1
| (Bin t1 t2) = (tree_size t1)
+ (tree_size t2)
This follows HtDP, but seems redundant. It is not obvious how to pull out common code.
Functional Programming with Bananas, Envelops, Lenses, and Barbed Wire (The Bananas Paper)
Meijer, Fokkinga, Patterson '91
Claim: just as gotos all over the place leads to unreadable code, so do
arbitrary recursive calls all over the place obscure the intent of the
programmer. Recursive functions should follow certain structure, and
they should be build with combinators which reflect that structure.
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
Examples are <Listof, map>, <BF, bfmap>
- 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
Jay, Cockett '94
This paper is based heavily in category theory. This work came out of a
need for compiler optimization, with the idea that you should be able
to do shape processing at compile time, get runtime speedup (Matthias
explains how the idea came over from the Fortran community, where
people want to figure out the shape of processing on arrays and do
transformations to speed up that processing based on shape).
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!
Bananas in Space
Meijer, Hutton '95
"We forgot the 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.
Polytypic Pattern Matching
This paper is based around the grammer of functors described earlier.
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
flattenTree = cataTree flTree
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 flf flg.
You can think of instantiation of this polytypic function as involving
elaboration of this definition based on the (known) datatype. So:
= 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 -> 
flTree = flPar + (Rec X Rec) = either flPar flRec X Rec = ... = either (\x -> [x]) (\(x,y) -> x ++ y)
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 ...