This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

map and fold
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2006-12-23 (23:54) From: Andrej Bauer Subject: Re: [Caml-list] map and fold
```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

```