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 180FF7FBCE for ; Mon, 12 Jan 2015 15:28:29 +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.15.14; 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.15.14 as permitted sender) identity=mailfrom; client-ip=212.227.15.14; 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.15.14; 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: AqgAAFDZs1TU4w8OnGdsb2JhbABb0CICgQ9DAQEBAQERAQEBAQEGDQkJFC6EDQEFJxNPCxgJJQ8FKIhLARQEyDcfhBIBCwEfjytVFoMAgRMFl0mGDAyLYYQRgzEBAQE X-IPAS-Result: AqgAAFDZs1TU4w8OnGdsb2JhbABb0CICgQ9DAQEBAQERAQEBAQEGDQkJFC6EDQEFJxNPCxgJJQ8FKIhLARQEyDcfhBIBCwEfjytVFoMAgRMFl0mGDAyLYYQRgzEBAQE X-IronPort-AV: E=Sophos;i="5.07,744,1413237600"; d="scan'208";a="116648781" Received: from mout.web.de ([212.227.15.14]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 12 Jan 2015 15:28:28 +0100 Received: from frosties.localnet ([134.3.241.185]) by smtp.web.de (mrweb001) with ESMTPSA (Nemesis) id 0LfzgJ-1XPWbI1WTz-00pewl for ; Mon, 12 Jan 2015 15:28:27 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.82) (envelope-from ) id 1YAfyk-0001W1-72 for caml-list@inria.fr; Mon, 12 Jan 2015 15:28:26 +0100 Date: Mon, 12 Jan 2015 15:28:26 +0100 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20150112142825.GA4820@frosties> References: <20150107135012.GA17784@frosties> <20150108152157.GA4890@frosties> <86k30xutma.fsf@cam.ac.uk> <20150110175201.GA32757@frosties> <86mw5q4gjo.fsf@cam.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <86mw5q4gjo.fsf@cam.ac.uk> User-Agent: Mutt/1.5.23 (2014-03-12) X-Provags-ID: V03:K0:Svwal2PBSCJvkCx5m2PTl2js3ecdGoFt/qbJuMANi2SqhpappZ1 60Srmr3pAPJfWYKoadAwtHDAQNoUwDrpANKKFIzv/MiVJlbyP7BovY1IFSKxfHWotNwjmy4 XwYR7BddTBs+LLz25Mb8cMhsEN/TKHl2NvOiWe7qgO3QUCxqRPEZGjKVtMAgtPucVN3oHr6 heipSbASrkPH3dicl1aOQ== X-UI-Out-Filterresults: notjunk:1; Subject: Re: [Caml-list] Problem with universal functions in a module On Sat, Jan 10, 2015 at 06:49:31PM +0000, Leo White wrote: > > 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. > > 'a. 'a -> 'a cannot unify with int -> int. If it did then 'a. 'a -> 'a > wouldn't be polymorphic: it could not be used as both int -> int and > float -> float. Instead 'a. 'a -> 'a must be instantiated to 'b -> 'b > which can then be unified with int -> int. It is the descision whether > or not to perform this instantiation that needs to be infered. > > To understand the full range of issues associated with higher-rank and > impredicative polymorphism I suggest reading the relevant literature > (e.g. "MLF: raising ML to the power of system F", "Semi-explicit > first-class polymorphism for ML", "Flexible types: robust type inference > for first-class polymorphism", "Boxy types: inference for higher-rank > types and impredicativity", ...). > > Regards, > > Leo I acknowledge that I'm weak on the theory here but from the example the rules seems to be pretty simple: When trying to unify a universal function with a polymorphic or monomorphic function first instantiate. As said I don't expect ocaml to infer what functions are universal. That can be annotated. So the question isn't if we can infer from the mono case wether the function is universal or monomorphic. The function must already be annotated as universal. Dropping the universality to allow unification with other types seems to be straight forward though. In laymans terms: A function 'a . 'a -> 'a can always be used where 'b -> 'b (or in this case int -> int) is expected. That doesn't change the type of the function itself though. MfG Goswin