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>
(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

Shapely Types

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

Jeuring '95

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)
  = 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 -> []
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:

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 ...