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 988B27FBC5 for ; Sat, 10 Jan 2015 19:49:33 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-50.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-50.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArUAAP9ysVSDbwiWnGdsb2JhbABbt3MGmDECgQlDAQEBAQERAQEBAQEGDQkJFC6EDQEEASdSBQsLISUPAQRJiDcIBMYzgxUBAQEHAQEBAR4YhW2JJk4HhCkFqT6EEIMyAQEB X-IPAS-Result: ArUAAP9ysVSDbwiWnGdsb2JhbABbt3MGmDECgQlDAQEBAQERAQEBAQEGDQkJFC6EDQEEASdSBQsLISUPAQRJiDcIBMYzgxUBAQEHAQEBAR4YhW2JJk4HhCkFqT6EEIMyAQEB X-IronPort-AV: E=Sophos;i="5.07,737,1413237600"; d="scan'208";a="116468083" Received: from ppsw-50.csi.cam.ac.uk ([131.111.8.150]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 10 Jan 2015 19:49:33 +0100 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from host86-190-253-80.range86-190.btcentralplus.com ([86.190.253.80]:59114 helo=netbook) by ppsw-50.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.158]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:AES128-GCM-SHA256:128) id 1YA16K-0002V3-qe (Exim 4.82_3-c0e5623) (return-path ); Sat, 10 Jan 2015 18:49:32 +0000 From: Leo White To: Goswin von Brederlow Cc: caml-list@inria.fr References: <20150107135012.GA17784@frosties> <20150108152157.GA4890@frosties> <86k30xutma.fsf@cam.ac.uk> <20150110175201.GA32757@frosties> X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Sat, 10 Jan 2015 18:49:31 +0000 In-Reply-To: <20150110175201.GA32757@frosties> (Goswin von Brederlow's message of "Sat, 10 Jan 2015 18:52:01 +0100") Message-ID: <86mw5q4gjo.fsf@cam.ac.uk> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain Subject: Re: [Caml-list] Problem with universal functions in a module > 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