From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p1P9lcio016818 for ; Fri, 25 Feb 2011 10:47:38 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjYCAGIJZ03RVdW2kGdsb2JhbACXd4Y2AYgECBUBAQEBCQkMBxEEIYg7mg6KH4IdhHgviFoBAQMFhVsEgWuKMohOOg X-IronPort-AV: E=Sophos;i="4.62,224,1297033200"; d="scan'208";a="100686445" Received: from mail-yx0-f182.google.com ([209.85.213.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Feb 2011 10:47:32 +0100 Received: by yxl31 with SMTP id 31so954540yxl.27 for ; Fri, 25 Feb 2011 01:47:31 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc:content-type; bh=4AKJf+5ds7YwPi0YxW79Dz7BIrEm/NCmGGCZ0u7wNAg=; b=Ky2FYu5Cjj5HYzuF+w6ZEuAUbpjWifMjjsKRE3587/jzWnHTr/Rzklk6/L+EaHXCQz i1FcaFPYkK/8iNnYtOFBxnnc82E1yWI/P+e5HoHctIRRyW7dzVXfo7bozUu89RTqA5Nd p8Y8kGr3HhE9cgNEgyMXnh7T207THvRroxtpU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=jVfw6y2ALr/sfJIYx/MO0dlaZOPIIzH6cErAIjRpyvUwiLgI0igZjg660zyyRVgNNR Bw2+mUCel0IcsDpxhmjJO7s/2XbuKHkEPP7nnpwGwL32Fv1N67upMWYsLeioI6uFyPFa 7+cKQ0SNaVL9NeBwd28Gr1ditA1d4LClNJ5GI= Received: by 10.100.114.13 with SMTP id m13mr935736anc.201.1298627251254; Fri, 25 Feb 2011 01:47:31 -0800 (PST) MIME-Version: 1.0 Received: by 10.100.225.8 with HTTP; Fri, 25 Feb 2011 01:47:11 -0800 (PST) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 25 Feb 2011 10:47:11 +0100 Message-ID: To: Damien.Pous@inria.fr Cc: Damien Pous , caml-list@inria.fr Content-Type: multipart/alternative; boundary=0016e6434ad801b7e9049d183898 Subject: Re: [Caml-list] type constructor polymorphism --0016e6434ad801b7e9049d183898 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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=3Dmarkup= &revision=3D174&root=3Damthing On Fri, Feb 25, 2011 at 10:26 AM, Damien Pous wro= te: > 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) :=3D > map (fun i =3D> i, float_of_nat i). > > Definition map_one A B (f: A -> B) x :=3D f x. > Definition map_two A B (f: A -> B) (x,y) :=3D (f x, f y). > Definition map_many :=3D List.map. > > Definition o :=3D k _ map_one 1. > Definition t :=3D k _ map_two (1,2). > Definition l :=3D 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) =3D > struct let k =3D C.map (fun i -> i, float_of_int i) end > > module One =3D struct type 'a t =3D 'a let map f x =3D f x end > module Two =3D struct type 'a t =3D 'a*'a let map f (x,y) =3D f x, f y end > module Many =3D struct type 'a t =3D 'a list let map =3D List.map end > > let _ =3D let module M =3D Make(One) in M.k 1 > let _ =3D let module M =3D Make(Two) in M.k (1,2) > let _ =3D let module M =3D Make(Many) in M.k [1;2;3] > > > * I remembered this (fabulous) message by Daniel B=FCnzli : > > http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/52732867110697f556= 50778d883ae5e9.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 =3D { map: 'b. ('a -> 'b) -> 'b container } > let rec one a =3D { map =3D fun f -> Obj.magic one (f a) } > let rec two a b =3D { map =3D fun f -> Obj.magic two (f a) (f b) } > let rec list l =3D { map =3D 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 > > --0016e6434ad801b7e9049d183898 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable As you use type-level computation (application of the type operator T to ty= pe 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 sy= ntactic sugar to make module manipulations lighter. Jacques Guarrigue has r= ecently mentioned such syntactic facilities in relation with the amthing pr= oject.
=A0 https://forge.ocamlc= ore.org/scm/viewvc.php/trunk/p4/pa_fcm.ml?view=3Dmarkup&revision=3D174&= amp;root=3Damthing

On Fri, Feb 25, 2011 at 10:26 AM, Damien Pou= s <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)
=A0(map: forall A B, (A -> B) -> T A -> T B) : T nat -> T (nat= *float) :=3D
=A0map (fun i =3D> i, float_of_nat i).

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

Definition o :=3D k _ map_one 1.
Definition t :=3D k _ map_two (1,2).
Definition l :=3D 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) =3D
struct let k =3D C.map (fun i -> i, float_of_int i) end

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

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


* I remembered this (fabulous) message by Daniel B=FCnzli :
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 =3D { map: 'b. ('a -> 'b) -> 'b= container }
let rec one a =A0 =3D { map =3D fun f -> Obj.magic one (f a) }
let rec two a b =3D { map =3D fun f -> Obj.magic two (f a) (f b) }
let rec list l =A0 =3D { map =3D 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. =A0Subscription 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


--0016e6434ad801b7e9049d183898--