[Caml-list] type constructor polymorphism

[Caml-list] type constructor polymorphism

[Damien Pous]

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

Re: [Caml-list] type constructor polymorphism

[Gabriel Scherer]

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

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

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

Re: [Caml-list] type constructor polymorphism

[Paolo Herms]

On Friday 25 February 2011 10:26:30 Damien Pous wrote:
> How would you translate the following (pseudo)Coq code ?
> [...]

using
Recursive Extraction map_one map_two map_many.

Seriously, why not have Coq extracted parts of your library? It may use some 
magic here and there but you can be sure it's what you wanted.
You just have to make sure you don't call functions like your k directly from 
caml code but through Coq extracted wrappers whose types are also in ml,
like your map functions.
-- 
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France