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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id A319D7FBC5 for ; Fri, 9 Jan 2015 02:02:39 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkUFAOQnr1SFBoIFVmdsb2JhbABcDoQiy3YCgVcBAQEBAQYBFwkRFy6EDQEFJxMGAwE1AQEOCxgcEkMUBog+slaFWAKMDoMOAQEBAQEBAQMBAQEBAQEBARMBBo9GMweDFoETiWONXJFug1NMYIJDAQEB X-IPAS-Result: AkUFAOQnr1SFBoIFVmdsb2JhbABcDoQiy3YCgVcBAQEBAQYBFwkRFy6EDQEFJxMGAwE1AQEOCxgcEkMUBog+slaFWAKMDoMOAQEBAQEBAQMBAQEBAQEBARMBBo9GMweDFoETiWONXJFug1NMYIJDAQEB X-IronPort-AV: E=Sophos;i="5.07,726,1413237600"; d="scan'208";a="116260413" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 09 Jan 2015 02:02:37 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 6A2A665D8; Fri, 9 Jan 2015 10:02:34 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 765412500; Fri, 9 Jan 2015 10:02:33 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=RMv2VKFOhYzOcn8Miiicjx8VKWE=; b=px53s6loLuLjQG9sOY1MTA+b0e+k mY/CyBLQSud198OBj5N8HtKS1B0B5LaM6MrQtwazgDcjuaLMFrE6TGgfh4cbwBI2 KOx54oCRGdWUHvhfvsSUZBA6bSTpfvcdU/0Vfa1xL3QNkSKcS9qVDNH5p87SauSH 6F+oXEFbz1foyDg= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=2Huw6rO9lrGl9cmFfJ2IFl17QMG+ldQbhboxgv5cFWSWNGcCFxI7/k/3oZmd45jBi0RTffjYoAVoHRiyOkfjEB3XYWBOxE+7tm7RsI7KOIlelqqmSZ4fUH28T58VgcnfPya/mep6eGubV+XK/onxhdrTWYoFmoivcdef6Y2UIWE=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 3EBAA24FA; Fri, 9 Jan 2015 10:02:32 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 8.1 \(1993\)) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: <86k30xutma.fsf@cam.ac.uk> Date: Fri, 9 Jan 2015 10:02:30 +0900 Cc: Goswin von Brederlow , OCaml Mailing List Content-Transfer-Encoding: quoted-printable Message-Id: References: <20150107135012.GA17784@frosties> <20150108152157.GA4890@frosties> <86k30xutma.fsf@cam.ac.uk> To: Leo P White X-Mailer: Apple Mail (2.1993) Subject: Re: [Caml-list] Problem with universal functions in a module On 2015/01/09 01:25, Leo White wrote: >=20 >> 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. >=20 > It is possible that higher-rank types would not add too much complexity > to OCaml. >=20 > 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/u= nboxing 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]) =3D let poly =3D if true then x else (Poly (fun x -> x) : ['a. 'a -> 'a]) in let mono =3D let Poly x =3D x in if true then x else (fun x -> x + 1) in (poly, mono) Note also that first-class modules already provide another flexible approac= h to first-class polymorphism, and while you need to define a package type, equality of pack= age types is structural since 4.02. module type T =3D sig val f : 'a -> 'a end let f (module X : T) =3D let poly : (module T) =3D if true then (module X) else (module struct let f x =3D x end) in let mono =3D 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 buildin= g modules. Jacques Garrigue=