From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 3E2DDBC0A for ; Sun, 24 Dec 2006 00:54:15 +0100 (CET) Received: from postar.fmf.uni-lj.si (vega.fmf.uni-lj.si [193.2.67.45]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id kBNNsEpN031207 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Sun, 24 Dec 2006 00:54:14 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id E955CF48BB; Sun, 24 Dec 2006 00:54:13 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id zSGLWMznvzbX; Sun, 24 Dec 2006 01:02:50 +0100 (CET) Received: from [192.168.1.100] (BSN-77-186-71.dsl.siol.net [193.77.186.71]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 51083F490F; Sun, 24 Dec 2006 00:54:12 +0100 (CET) Message-ID: <458DC1BC.5090802@fmf.uni-lj.si> Date: Sun, 24 Dec 2006 00:54:36 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 1.5.0.7 (X11/20060927) MIME-Version: 1.0 To: skaller , caml-list@yquem.inria.fr Subject: Re: [Caml-list] map and fold References: <1166786286.6549.24.camel@rosella.wigram> In-Reply-To: <1166786286.6549.24.camel@rosella.wigram> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 458DC1A6.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 datatype:01 constructors:01 datatype:01 nat:01 nat:01 forall:01 forall:01 recursion:01 parametrized:01 node:01 node:01 parametrized:01 functor:01 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