From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id E2AF17FBC5 for ; Sat, 10 Jan 2015 19:02:29 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.15.4; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of goswin-v-b@web.de designates 212.227.15.4 as permitted sender) identity=mailfrom; client-ip=212.227.15.4; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.15.4; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArIAAAZosVTU4w8EnGdsb2JhbABbDs1Ogk8CgQlDAQEBAQERAQEBAQEGDQkJFC6EDQEFJxM/EAsYCSUPBSghiCoBFATFHR+EEgEBAQEBAQQBAQEBAQEcj3kHgxaBEwWXRoYLDIthg1M+gzEBAQE X-IPAS-Result: ArIAAAZosVTU4w8EnGdsb2JhbABbDs1Ogk8CgQlDAQEBAQERAQEBAQEGDQkJFC6EDQEFJxM/EAsYCSUPBSghiCoBFATFHR+EEgEBAQEBAQQBAQEBAQEcj3kHgxaBEwWXRoYLDIthg1M+gzEBAQE X-IronPort-AV: E=Sophos;i="5.07,737,1413237600"; d="scan'208";a="95966570" Received: from mout.web.de ([212.227.15.4]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 10 Jan 2015 19:02:29 +0100 Received: from frosties.localnet ([134.3.241.185]) by smtp.web.de (mrweb002) with ESMTPSA (Nemesis) id 0MINI7-1YDZny0xsF-0049V9; Sat, 10 Jan 2015 19:02:25 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.82) (envelope-from ) id 1YA0Mi-0000CD-2Y; Sat, 10 Jan 2015 19:02:24 +0100 Date: Sat, 10 Jan 2015 19:02:24 +0100 From: Goswin von Brederlow To: Jacques Garrigue Cc: Leo P White , OCaml Mailing List Message-ID: <20150110180223.GB32757@frosties> References: <20150107135012.GA17784@frosties> <20150108152157.GA4890@frosties> <86k30xutma.fsf@cam.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-Provags-ID: V03:K0:s+ckUXpqM97qwOhuRcUhOFRHI8xB45ROeSAgYZcaFsokTf2N1YX 6qOwiD8Hpw0KW3+Fq5dqzeZWrVZlK9fil81QVKvSz85x26SnP2kOt+RzTpPCRfIdDH6PxlU bElXgm7sTjaUaO6DoKdK3/YFqU/aUhIdgd+j+n/S+dhNZ1utHB0W08rjyIAu85ovsUqtYlg 1aTAFDrfO3GDoVIgNStvw== X-UI-Out-Filterresults: notjunk:1; Subject: Re: [Caml-list] Problem with universal functions in a module On Fri, Jan 09, 2015 at 10:02:30AM +0900, Jacques Garrigue wrote: > On 2015/01/09 01:25, Leo White wrote: > > > >> I don't see how there can be much added complexity involved. The > >> higher-rank polymorphism is already allowed in records and objects so > >> the type system knows how to deal with them. At least when they are > >> annotated. I wouldn't need ocaml to infere those types. > > > > It is possible that higher-rank types would not add too much complexity > > to OCaml. > > > > However, there is an important difference between that and the > > higher-rank polymorphism provided by records and objects: whether to > > instantiate a type or not must be inferred. > > Actually the formal system for polymorphic methods use a notion of boxing/unboxing > of first-class polymorphic values. It would be trivial to add it to ocaml's type system. > There was not much demand originally, but with the introduction of GADTs it becomes > more interesting. > > let f (x : ['a. 'a -> 'a]) = > let poly = > if true then x > else (Poly (fun x -> x) : ['a. 'a -> 'a]) > in > let mono = > let Poly x = x in > if true then x > else (fun x -> x + 1) > in > (poly, mono) > > Note also that first-class modules already provide another flexible approach to first-class > polymorphism, and while you need to define a package type, equality of package > types is structural since 4.02. > > module type T = sig val f : 'a -> 'a end > > let f (module X : T) = > let poly : (module T) = > if true then (module X) > else (module struct let f x = x end) > in > let mono = > if true then X.f > else (fun x -> x + 1) > in > (poly, mono) > > As you can see here, the only slightly heavy part is the syntax for building modules. > > Jacques Garrigue Modules don't improve anything here. The problem is still that you can't hide the implementation of the boxing: # let make : ('a -> 'a) -> (module T) = function | fn -> (module struct let f = fn end);; Error: Signature mismatch: Modules do not match: sig val f : '_a -> '_a end is not included in T Values do not match: val f : '_a -> '_a is not included in val f : 'a -> 'a And you need different modules for different kind of types. Like 'a t, ('a, 'b) t, ... So I think modules are just as unflexible as objects and records here. MfG Goswin