From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 01944BC57 for ; Fri, 24 Sep 2010 03:32:51 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aj4CADKcm0zRVdW0kWdsb2JhbACiMAgVAQECCQsKBxEDH60Ii1GGW4kDAQEDBYU9BIRMhWyDXoICgyM X-IronPort-AV: E=Sophos;i="4.57,226,1283724000"; d="scan'208";a="64750609" Received: from mail-yx0-f180.google.com ([209.85.213.180]) by mail2-smtp-roc.national.inria.fr with ESMTP; 24 Sep 2010 03:32:50 +0200 Received: by yxi11 with SMTP id 11so1060965yxi.39 for ; Thu, 23 Sep 2010 18:32:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:sender:subject:mime-version :content-type:from:in-reply-to:date:cc:reply-to :content-transfer-encoding:message-id:references:to:x-mailer; bh=PHfvwtR3iI3r4mU/Xgfm8YEjwpRYpXmAd/BF6J6jp5Y=; b=XbuDvg14nIZZGb1aa924e+0SCZbhPwM9oZQnRHXu95U1lDfCI4IcHKNEiLQcPkylx4 GO0OKjzBro+lryQBRs07zPc7vjjBMNWYmeJrY0uLlGymRhVg0denSD77x/YhPdB3fgY4 2aB4xH/pJdEDAJdLldp0UVq+ZBmbbiNgaF7ts= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :reply-to:content-transfer-encoding:message-id:references:to :x-mailer; b=S4TSz/l+oeF0uekjQqsHBGZ1eFGWw1WDyLLpYB58ZGhI/+FVOpkRZ5UBHP6KdMaRz6 i6j1nJkoLGyxDnxGLgC/mBrQt1iqAhrV071J6/bvvwGMGz67NnpcByKDQUzXdUroamJG 4/Rep+v3s17cAE2HDNxnRqu1Fjp2YOFqSccg0= Received: by 10.100.225.4 with SMTP id x4mr3015745ang.119.1285291969544; Thu, 23 Sep 2010 18:32:49 -0700 (PDT) Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mx.google.com with ESMTPS id d4sm2282459and.39.2010.09.23.18.32.47 (version=TLSv1/SSLv3 cipher=RC4-MD5); Thu, 23 Sep 2010 18:32:49 -0700 (PDT) Sender: Jacques Garrigue Subject: Re: [Caml-list] Optional arguments "between" non-optional ones Mime-Version: 1.0 (Apple Message framework v1081) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Fri, 24 Sep 2010 10:32:44 +0900 Cc: bluestorm , Caml Mailing List Reply-To: garrigue@math.nagoya-u.ac.jp Content-Transfer-Encoding: 7bit Message-Id: <00FF2AA5-C0EF-4835-BCB4-326DA78B8665@gmail.com> References: To: Adrien X-Mailer: Apple Mail (2.1081) X-Spam: no; 0.00; ocaml:01 semantics:01 semantics:01 discrepancy:01 wrote:01 wrote:01 defines:01 caml-list:01 functions:01 functions:01 argument:02 argument:02 inferred:02 coerce:02 parameter:02 On 2010/09/24, at 0:05, Adrien wrote: > On 23/09/2010, bluestorm wrote: >> (sorry for any double-posting) >> >> The problem is that in your declaration of h, the inferred type for f >> is of the form (unit -> unit -> ...), and you use it with the >> different type (unit -> ?a:'a -> unit -> ...). >> >> Changing ?a to be the first parameter of f change f's type to (?a:'a >> -> unit -> unit -> ...). OCaml knows that it can implicitly coerce >> functions when the optional parameters appear in the first position. > > I actually expected types (?a:'a -> unit -> unit -> ...) and (unit -> > ?a:'a -> unit -> ...) to work alike. I'm wondering why the arguments > are "dropped" from the first case but not the second. The answer is that this way of coercing functions by applying optional arguments when they are passed is a kind of hack. The formal semantics defines optional argument discarding as happening only when a function is applied. However, one often wants this discarding to occur when the function is passed as argument, to avoid manual eta-expansion. This is actually done through an eta-expansion (i.e., (fun x -> f x) gets passed to the function instead of f, to be sure that side-effects happen at the right time). Since only cases with a single eta-expansion are considered, optional arguments should come first. Of course we are very careful of not breaking the formal semantics (where there is no eta-expansion, and discarding will only occur when the function is applied). Whenever the eta-expansion approach might introduce a discrepancy, you will get a type error. Jacques Garrigue