Re: [Caml-list] map and fold

[Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>]

skaller wrote:
> What is the relationship between map and fold?

I don't have much to say about map, but here's a mathematician's 
explanation of where fold comes from. Perhaps it will help.

With each inductive datatype, such as natural numbers, lists or trees, 
there is an associated induction principle, which roughly says:

   If a property P holds for the base cases (zero, empty list, empty
   tree), and if the property is preserved by all the constructors
   (successor, cons), then the property holds for all elements of the
   inductive datatype.

We can interpret the induction principle under the realizability 
interpretation (which is sort of like propositions-as-types) to obtain a 
type. The fold-liek operation corresponding to the inductive datatype 
has this type. Examples follow.


1) Natural numbers are defined inductively as

   type nat = Zero | Succ of nat

The induction principle is:

   P(Zero) ==> (forall n:nat)(P(n) ==> P(Succ(n))) ==>
   (forall n:nat)P(n)

The type corresponding to this is:

   'p -> (nat -> 'p -> 'p) -> nat -> 'p

An element of this type is:

let rec fold u f = function
   | Zero -> u
   | Succ n -> f n (fold u f n)

This is just primitive recursion.

2) Lists (parametrized by 'a) are defined inductively as

   type 'a list = Nil | Cons of 'a t * 'a list

The induction principle is

   P(Nil) ==> (forall x:'a)(forall l:'a list)(P(l) => P(Cons(x,l)) ==>
   (forall l:'a list)P(l)

which yields the type

   'p -> ('a -> 'a list -> 'p -> 'p) -> 'a list -> 'p

with the fold-like operation of this type:

let rec fold u f = function
   | Nil -> u
   | Cons (x,l) -> f x l (fold u f l)

(Note the difference between fold and List.fold_left: fold hands the 
tail to f, whereas List.fold_left does not.)

3) Trees of t's:

type 'a tree = Empty | Node of 'a * 'a tree * 'a tree

Induction principle:

   P(Empty) ==>
   (forall u:'a)(forall t1:'a tree)(forall t2:'a tree)(
     P(t1) ==> P(t2) ==> P (Node (u, t1, t2)
   ) ==>
   (forall t:'a tree)P(t)

The type:

   'p -> ('a -> 'a tree -> 'a tree -> 'p -> 'p -> 'p) -> 'p

Fold for trees:

let rec fold u f = function
   | Empty -> u
   | Tree (x,t1,t2) -> f x t1 t2 (fold u t1) (fold u t2)


Just like induction is a powerful and basic principle, fold is a 
powerful operation that allows us to construct many others.

I am not quite sure how skaller intended map to work (it seems like the 
"add one more element" operation is rather specialized). A simple way to 
view map is as follows.

Suppose we have a parametrized type

   type 'a t = ...

in which 'a appears _covariantly_. Then

   map : ('a -> 'b) -> 'a t -> 'b t

will be just the action of the type constructor t on morphisms (when we 
view things appropriately in a category-theoretic sense, with t being a 
functor). Example:

type 'a t = Foo of (int -> 'a * 'a * t) | Bar of 'a * t

let rec map f = function
   | Foo h -> Foo (fun n -> let u,v,x = h n in (f u, f v, map f x))
   | Bar (u,x) -> Bar (f u, map f x)

Furthermore if t is inductively defined, we can express map in terms of 
fold. Examples:

1) Lists:

type 'a list = Nil | Cons of 'a * 'a list

let map f = fold Nil (fun u _ x -> Cons (f u, x))

2) Trees:

type 'a tree = Empty | Node of 'a * 'a tree * 'a tree

let map f = fold Empty (fun u _ _ x y -> Node (f u, x, y))

Andrej