[Caml-list] type constructor polymorphism

[Damien Pous <Damien.Pous@inrialpes.fr>]

Hi,

I have not been on this list for a long time, I come back for a naive
question on polymorphism :
How would you translate the following (pseudo)Coq code ?

Definition k (T: Type -> Type)
  (map: forall A B, (A -> B) -> T A -> T B) : T nat -> T (nat*float) :=
  map (fun i => i, float_of_nat i).

Definition map_one A B (f: A -> B) x := f x.
Definition map_two A B (f: A -> B) (x,y) := (f x, f y).
Definition map_many := List.map.

Definition o := k _ map_one 1.
Definition t := k _ map_two (1,2).
Definition l := k _ map_list [1;2;3].


* I have the following obvious solution, using modules, but I find it
pretty ugly :

module Make(C: sig type 'a t val map: ('a -> 'b) -> 'a t -> 'b t end) =
struct let k = C.map (fun i -> i, float_of_int i) end

module One = struct type 'a t = 'a let map f x = f x end
module Two = struct type 'a t = 'a*'a let map f (x,y) = f x, f y end
module Many = struct type 'a t = 'a list let map = List.map end

let _ = let module M = Make(One) in M.k 1
let _ = let module M = Make(Two) in M.k (1,2)
let _ = let module M = Make(Many) in M.k [1;2;3]


* I remembered this (fabulous) message by Daniel Bünzli :
http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/52732867110697f55650778d883ae5e9.en.html
but I couldn't manage to do a similar thing (since I am not trying to
encode existential types, this trick might be completely unrelated).


* I also tried things with objects, or polymorphic records like:

type 'a container = { map: 'b. ('a -> 'b) -> 'b container }
let rec one a   = { map = fun f -> Obj.magic one (f a) }
let rec two a b = { map = fun f -> Obj.magic two (f a) (f b) }
let rec list l   = { map = fun f -> Obj.magic list (List.map f l) }

without more success (note that Obj.magic is used both to allow
polymorphic recursion, and to make some people angry on the list!)



Do some of you have a nice trick for this pattern?
Or modules and functors are just the right way to do this in OCaml,
and I'll have to accept it...

Regards,
Damien Pous