map and fold

map and fold

[skaller]

What is the relationship between map and fold?

It seems like if you have a X.fold plus an constructor
which adds an element to an existing container Y.t
you can define a kind of map which copies elements of
'a X.t into 'b T.t given an element map f: 'a -> 'b.

In STL the algorithm accumulate can do this, given
a start and end iterator for the input container,
and an insert iterator for the output container.

Anyhow it 'feels' like the fold is a container destructor,
and the constructor is a kind of 'dual' of fold. Map is then
just a combination of the fold with a special case of
the constructor function.. hmm. Any hint what the formal
symmetry is here?


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] map and fold

[Florian Hars]

skaller wrote:
> Any hint what the formal symmetry is here?

Isn't this what the bananas-paper is about?
http://citeseer.ist.psu.edu/meijer91functional.html

Yours, Florian.

Re: [Caml-list] map and fold

[Andrej Bauer]

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

Re: [Caml-list] map and fold

[skaller]

On Sun, 2006-12-24 at 00:54 +0100, Andrej Bauer wrote:

[]

> I am not quite sure how skaller intended map to work 

Neither am I. My aim here is roughly: in Felix 
I have overloading, typeclasses and I also have tuples.

Overloading provides 'generic' operations on primitive types
in an ad hoc manner.

Typeclasses provide 'generic' operations on primitive types
in a uniform manner.

Tuples are heterogenous lists with statically known types,
more generally we'd have algebraic types but tuples will
do for a start.

There are many things I'd like to do with tuples.
Too many. The operations are generic (polyadic) not merely
polymorphic as for lists.

In fact there is a correspondence: the Ocaml representation
of a tuple is a list of terms, so run time generic operations
are Ocaml time list polymorphic: so in the compiler,
implementing generic operations is easy -- but end users
can't do it, and 'easy' isn't the same as wanting to
provide hundreds of compiler supported intrinsics.

What I need to do is find some primitive, compiler supported
operations, which can be *combined* in user library code
to provide the others.

Well, I obviously need things like

	fold
	zip (compose)
	split
	map

and a host of other generic operations. In fact so far I
have implemented

	memcount e         // counts members
	_tuple_fold f i c  // fold generic f 
        _tuple_trans e     // transpose tuple of tuples
                           // subsumes zip and split

but I have no idea 

(a) whether this set of operations is sufficient
(b) how to combine them 
(c) how to generalise to all algebraic types

so I'm trying to get a more theoretical picture of
how these things relate.

I have a picture that if you have fold, map comes for free,
but just folding over the appropriate constructor.

But really the question is deeper: I'm really asking
how to design a programming language that supports 
generic programming, or more precisely, how to make
practical progress towards that.

I can do slightly more to Felix than Ocaml, since
I can intervene in any part of the compiler. The tuple
fold depends on type information, so it couldn't be
implemented in Ocaml using camlp4.

The users have an immediate need: right now we have

	typeclass Eq[t] { virtual fun eq: t * t -> bool; }

	instance Eq[int] { .. }
	instance Eq[double] { .. }
	...

so we have generic equality for primitives. There should
be no need to manually instantiate the typeclass for
each tuple of interest though: one definition should
be enough to cover them all:

fun eqa[t with Eq[t]]: bool * (t * t) -> bool =
| ?result, (?a, ?b) => result and a == b;

val x1 = ((1,1),(2.0,2.0),("3","3"));
print$ _tuple_fold eqa true x1; endl;

actually works now. Throw in transpose function to get the
arguments in the right form, cover sum types as well,
and we have second class generic equality operator:
this is better than Ocaml's polymorphic equality in the
sense that it also works with abstract types, and weaker
in the sense it is only second class (compile time only,
no closures).

This is pretty hot stuff for a scripting language:
much safer than Python etc.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] map and fold

[skaller]

On Sun, 2006-12-24 at 00:54 +0100, Andrej Bauer wrote:
> skaller wrote:

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

However in Ocaml at least you cannot actually write a single
definition for map in terms of a single fold -- you have to
write out fold for each data type, and worse, even given that
you still need to write out map for each data type too,
following an idiomatic pattern.

How could Ocaml be extended to get rid of this unsafe
verbosity?

Even if the resulting generic operators weren't first class,
it would still be useful to define 'map' once and be done
with it.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] map and fold

[Tom]

[-- Attachment #1: Type: text/plain, Size: 807 bytes --]

>
>
> However in Ocaml at least you cannot actually write a single
> definition for map in terms of a single fold -- you have to
> write out fold for each data type, and worse, even given that
> you still need to write out map for each data type too,
> following an idiomatic pattern.
>
> How could Ocaml be extended to get rid of this unsafe
> verbosity?
>
> Even if the resulting generic operators weren't first class,
> it would still be useful to define 'map' once and be done
> with it.
>

Hm... maybe you have in mind something called "polytypic programming"

Example: pmap :: Regular d => (a->b) -> d a -> d b
    A generalisation to all regular datatypes of the normal map on lists .
Applies a function to all elements in a structure.

Take a look at http://www.cs.chalmers.se/~patrikj/poly/

- Tom

[-- Attachment #2: Type: text/html, Size: 1148 bytes --]