map and fold

skaller
 Florian Hars
 Andrej Bauer
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Andrej Bauer <Andrej.Bauer@f...> 
Subject:  Re: [Camllist] 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 propositionsastypes) to obtain a type. The foldliek 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 foldlike 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 categorytheoretic 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