As you use type-level computation (application of the type operator T to
type variables A and B), you are at the Fomega level, and to my knowledge
the module system is the only part of OCaml which can express Fomega. So I
don't think you will be able to do without it.

I you really find that too heavy, maybe you should start looking for
syntactic sugar to make module manipulations lighter. Jacques Guarrigue has
recently mentioned such syntactic facilities in relation with the amthing
project.

https://forge.ocamlcore.org/scm/viewvc.php/trunk/p4/pa_fcm.ml?view=markup&revision=174&root=amthing

On Fri, Feb 25, 2011 at 10:26 AM, Damien Pous <Damien.Pous@inrialpes.fr>wrote:

> 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
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>