From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p1P9QFh9016170 for ; Fri, 25 Feb 2011 10:26:15 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoYCALMEZ03RVda2kGdsb2JhbACYKI4KCBUBAQEBCQkMBxEEIaJVjDyEeYkJAQEDBYVbBIwdiE46gRU X-IronPort-AV: E=Sophos;i="4.62,224,1297033200"; d="scan'208";a="88693728" Received: from mail-iw0-f182.google.com ([209.85.214.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Feb 2011 10:26:09 +0100 Received: by iwn33 with SMTP id 33so1437666iwn.27 for ; Fri, 25 Feb 2011 01:26:07 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:sender:reply-to:date :x-google-sender-auth:message-id:subject:from:to:content-type :content-transfer-encoding; bh=NBFeLka8Qz1+gGpt4sMI+nRekTwL9Ru9itUxe/BsHNE=; b=fiwzpttHX78nlAcVsKR14iAZ8xteQUR0sDXN8Gx5ojwgCsLI6R4pCqN96IaSjm7Fjd YFt6YQDXQp5st2lAmEk0lwuf7xSHCmsojP+oGvvEwZP3JxfLU4lMMla0SZqWg+EgGJfT YpGFfxVMwSR4f7IyW8KiAYkDloSUp19MzQIVw= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:reply-to:date:x-google-sender-auth:message-id :subject:from:to:content-type:content-transfer-encoding; b=qNVqJFcvlVImqENiB4v5jCpW9qALhBjrxbIpbePmp978RJxnAZYr7BUbWfs5zatg/2 M0b9R+9fhS4tJOP+Qq55J0mJ3Clh1k12O+iPVX21ObPAEQ2jqD1laN/UA4Fnu09BcTQ9 pacHwZxHbsHaT13rN2HUTdpqMlPlYvufZ0aOc= MIME-Version: 1.0 Received: by 10.231.35.136 with SMTP id p8mr2690376ibd.139.1298625966216; Fri, 25 Feb 2011 01:26:06 -0800 (PST) Sender: damien.pous@gmail.com Reply-To: Damien.Pous@inria.fr Received: by 10.231.170.77 with HTTP; Fri, 25 Feb 2011 01:26:06 -0800 (PST) Date: Fri, 25 Feb 2011 10:26:06 +0100 X-Google-Sender-Auth: grF4L0yEDf_ca-ZWBca97J6_TjM Message-ID: From: Damien Pous To: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p1P9QFh9016170 Subject: [Caml-list] type constructor polymorphism 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