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 DA6417FBC5 for ; Sat, 10 Jan 2015 18:52:04 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of goswin-v-b@web.de designates 212.227.17.12 as permitted sender) identity=mailfrom; client-ip=212.227.17.12; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.17.12; receiver=mail2-smtp-roc.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: ArIAACFmsVTU4xEMnGdsb2JhbABbDtAdAoEJQwEBAQEBEQEBAQEBBg0JCRQuhAwBAQEDAScTPwULCw4KCSUPBSghiCoBDAgExSEfhBIBAQEBBgEBAQEBHY95B4MWgRMFl0aGCwyLYYNTPoMxAQEB X-IPAS-Result: ArIAACFmsVTU4xEMnGdsb2JhbABbDtAdAoEJQwEBAQEBEQEBAQEBBg0JCRQuhAwBAQEDAScTPwULCw4KCSUPBSghiCoBDAgExSEfhBIBAQEBBgEBAQEBHY95B4MWgRMFl0aGCwyLYYNTPoMxAQEB X-IronPort-AV: E=Sophos;i="5.07,737,1413237600"; d="scan'208";a="116465240" Received: from mout.web.de ([212.227.17.12]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 10 Jan 2015 18:52:04 +0100 Received: from frosties.localnet ([134.3.241.185]) by smtp.web.de (mrweb101) with ESMTPSA (Nemesis) id 0Mfq6i-1YOFGw1XO8-00N7YW; Sat, 10 Jan 2015 18:52:02 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.82) (envelope-from ) id 1YA0Cf-00008b-Bq; Sat, 10 Jan 2015 18:52:01 +0100 Date: Sat, 10 Jan 2015 18:52:01 +0100 From: Goswin von Brederlow To: Leo White Cc: caml-list@inria.fr Message-ID: <20150110175201.GA32757@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: <86k30xutma.fsf@cam.ac.uk> User-Agent: Mutt/1.5.23 (2014-03-12) X-Provags-ID: V03:K0:z1eqcGCu+uDhTRmyscCmxNOF7CzX2ciKw+BVnJpcYc4tHJxQnNd dvWahR8Y5emWDcmn8hFoO1SzQQyQpSbLdk/JJ6fda4O4Dil1ZQpdIHiB+hYdsnmnb1EngYk i/u33FuorSbI8f8PwYQGq8rgo0+s9afdy4AwWyLOwt9B9ij89iJi5OLbsF4Ko82TgvlfnOO oUs4mdW8mxDcIpOpgi+kg== X-UI-Out-Filterresults: notjunk:1; Subject: Re: [Caml-list] Problem with universal functions in a module On Thu, Jan 08, 2015 at 04:25:49PM +0000, 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. For example, compare this > example using polymorphic methods: > > let f (x : < m: 'a. 'a -> 'a >) = > let poly = > if true then x > else object method m : 'a. 'a -> 'a = id end > in > let mono = > if true then x#m ^^^ 'a . 'a -> 'a > else (fun x -> x + 1) ^^^^^^^^^^^^^^ int -> int > in > (poly, mono) > > with this example using proper higher-rank types: > > let f (x : 'a. 'a -> 'a) = > let poly = > if true then x > else id > in > let mono = > if true then x ^ 'a . 'a -> 'a > else (fun x -> x + 1) ^^^^^^^^^^^^^^ int -> int > in > (poly, mono) > Using objects with polymorphic methods we can trivially see that the > first use of `x` is not instantiated whilst the second use of `x` is > instantiated because the first uses the object itself whilst the second > uses the method `m`. > > With higher-rank polymorphism, we must infer this information. I don't > think this can be done in a principal way, without adding complexity to > the type langauge (see MLF), so there would need to be some additional > type annotations. I don't see anything to infere there. Only thing I see is that in the case of mono the universal function has to be unified with a single type function. But 'a . 'a -> 'a should unify with int -> int resulting in int -> int without problems. I see no difference between the record and the plain case. The record only adds a boxing around the type. It doesn't make the type any easier to infer or unify for me. MfG Goswin