From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 76E6CBBAF for ; Sat, 14 Mar 2009 15:46:12 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkMBAMtfu0lCbwQZkGdsb2JhbACVQQEBAQEJCQwHEQS6J4N/Bg X-IronPort-AV: E=Sophos;i="4.38,362,1233529200"; d="scan'208";a="24326712" Received: from out1.smtp.messagingengine.com ([66.111.4.25]) by mail3-smtp-sop.national.inria.fr with ESMTP; 14 Mar 2009 15:46:11 +0100 Received: from compute2.internal (compute2.internal [10.202.2.42]) by out1.messagingengine.com (Postfix) with ESMTP id A80472ECC97; Sat, 14 Mar 2009 10:46:10 -0400 (EDT) Received: from heartbeat2.messagingengine.com ([10.202.2.161]) by compute2.internal (MEProxy); Sat, 14 Mar 2009 10:46:10 -0400 X-Sasl-enc: pIfpwyCi0NWAlgxttSsho7zk8tHPreNRq8Kd/7vLv56E 1237041970 Received: from [192.168.1.10] (ALyon-157-1-34-213.w86-219.abo.wanadoo.fr [86.219.117.213]) by mail.messagingengine.com (Postfix) with ESMTPSA id 0FE12455DC; Sat, 14 Mar 2009 10:46:09 -0400 (EDT) Message-ID: <49BBC289.8080908@ens-lyon.org> Date: Sat, 14 Mar 2009 15:43:21 +0100 From: Martin Jambon User-Agent: Thunderbird 2.0.0.17 (X11/20081008) MIME-Version: 1.0 To: Philippe Veber Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Commuting labeled arguments References: <721f7f5a0903140314saf947b9n1531207146ba2e29@mail.gmail.com> In-Reply-To: <721f7f5a0903140314saf947b9n1531207146ba2e29@mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; ens-lyon:01 checker:01 val:01 val:01 runtime:01 compiler:01 checker:01 wrote:01 caml-list:01 int:01 int:01 jambon:01 jambon:01 behaviour:01 expression:02 Philippe Veber wrote: > Hi all, > > is this behaviour of the type checker expected ? > > Objective Caml version 3.11.0 > > # let f g x y = g ~x ~y;; > val f : (x:'a -> y:'b -> 'c) -> 'a -> 'b -> 'c = > # let g ~y ~x = x + y;; > val g : y:int -> x:int -> int = > # f g;; > Error: This expression has type y:int -> x:int -> int > but is here used with type x:'a -> y:'b -> 'c > > If so, I'm tempted to fill a report to mantis anyway, to get this said > in the manual (i've not seen anything for this case, but i might have > missed something). Imagine that any function has a unique runtime representation that only accepts one particular order for its arguments. Labeled arguments can only commute during function application when a particular order is expected. Reordering is done solely by the compiler based on the presence labels. If no particular order is expected (g ~x ~y in your definition of f), then the type checker assumes something reasonable but must make a choice. This is why the first argument of f is inferred to have type (x:'a -> y:'b -> 'c) although a type annotation could change this. I find this interesting: # let f g x y = g ~x ~y + g ~y ~x ;; Characters 26-27: g ~x ~y + g ~y ~x ^ This function is applied to arguments in an order different from other calls. This is only allowed when the real type is known. # let f (g : x:_ -> y:_ -> _) x y = g ~x ~y + g ~y ~x ;; val f : (x:'a -> y:'b -> int) -> 'a -> 'b -> int = Martin -- http://mjambon.com/