Re: [Caml-list] First order compile time functorial polymorphism in Ocaml

[Michal Moskal <malekith@pld-linux.org>]

On Mon, Jun 23, 2003 at 04:25:18AM +1000, John Skaller wrote:
> In ML style functional programming languages like Ocaml,
> we have what is termed data polymorphism. This provides
> a kind of code reuse we're all familiar with.
> 
> However, there is another kind of polymophism
> which Ocaml does not provide. Two things to consider here:
> 
> 1. Every data structure has a map function.
> 2. User defined algebraic type require a hand written map function
> 
> It sure is inconvenient to have to remember the names
> of all those map functions, not to mention having to hand
> write them. Lets look at a map function:
> 
> type 'a mylist = Empty | Cons of 'a * 'a list
> 
> let rec map_mylist f a = match a with
> | Empty -> Empty
> | Cons (h,t) -> Cons (f h, map_mylist f t)
>
> It is clear from this example, that every inductive type
> can have a map function generated by a purely mechanical
> transformation on the type terms: that is, there
> is no reason to ever write map functions again.

First thing to consider: map function of this kind only exists for types,
where type variables occur only positively. Even then, for inductive
types it requires proof (it isn't as simple as it first seems).

For example consider:

type 'a t = Foo 'a -> unit

To map : 'a t -> 'b t here, you need f : 'b -> 'a.

[...]
> 7. Handling abstract types. In order to actually summon
> the above code generations, we posit a new binding construction:
> 
> 	let <new_name> = polymap <type> in
> 
> if the definition of <type> contains any opaque types,
> including any abstract type of a module, primitive
> not known in Pervasives, or, a class, then the client
> must supply the mapping function as follows:
> 
> 	let <new_name> = polymap <type> with polymap list = List.map in
> etc.

What about t1 -> t2? (this is the real problem).
 
> The same mechanism can be provided for folds, iterators,
> etc. Because this is a first order system, we have to hand
> write the functorial transformation each time.

Automatic definition of iterators and recursors for types also isn't
that simple, it requires good dose of theory.

I once wrote (in OCaml) interpreter for language with automatic
definitions of iterators and recursors, based on PhD thesis of Zdzislaw
Splawski. Unfortunately while I can provide source code, thesis is not
available online, and without it it will be hard to understand source
(i.e. the iterator/recursor generation part).

-- 
: Michal Moskal :: http://www.kernel.pl/~malekith : GCS {C,UL}++++$ a? !tv
: When in doubt, use brute force. -- Ken Thompson : {E-,w}-- {b++,e}>+++ h

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners