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 B27BA7FBC5 for ; Thu, 8 Jan 2015 17:25:52 +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.140; 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.140; 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-40.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.140; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-40.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlcAAPGurlSDbwiMnGdsb2JhbABct3AGmC4CgRBDAQEBAQERAQEBAQEICwkJFC6EDQEEASdSBQsLISUPAQRJiDcIBMNMgngBAQgBAQEBHhiFbYl0B4QpBakohBCDMgEBAQ X-IPAS-Result: AlcAAPGurlSDbwiMnGdsb2JhbABct3AGmC4CgRBDAQEBAQERAQEBAQEICwkJFC6EDQEEASdSBQsLISUPAQRJiDcIBMNMgngBAQgBAQEBHhiFbYl0B4QpBakohBCDMgEBAQ X-IronPort-AV: E=Sophos;i="5.07,723,1413237600"; d="scan'208";a="116220522" Received: from ppsw-40.csi.cam.ac.uk ([131.111.8.140]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 08 Jan 2015 17:25:52 +0100 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from host86-182-254-133.range86-182.btcentralplus.com ([86.182.254.133]:48362 helo=netbook) by ppsw-40.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.156]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:AES128-GCM-SHA256:128) id 1Y9FuC-0001Md-ja (Exim 4.82_3-c0e5623) (return-path ); Thu, 08 Jan 2015 16:25:52 +0000 From: Leo White To: Goswin von Brederlow Cc: caml-list@inria.fr References: <20150107135012.GA17784@frosties> <20150108152157.GA4890@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: Thu, 08 Jan 2015 16:25:49 +0000 In-Reply-To: <20150108152157.GA4890@frosties> (Goswin von Brederlow's message of "Thu, 8 Jan 2015 16:21:57 +0100") Message-ID: <86k30xutma.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 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 else (fun x -> x + 1) 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 else (fun x -> x + 1) 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. Regards, Leo