From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA21773; Sat, 17 Feb 2001 21:07:57 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA21776 for ; Sat, 17 Feb 2001 21:07:56 +0100 (MET) Received: from fledge.watson.org (fledge.watson.org [204.156.12.50]) by nez-perce.inria.fr (8.11.1/8.10.0) with ESMTP id f1HK7tD17486; Sat, 17 Feb 2001 21:07:55 +0100 (MET) Received: from localhost (patrick@localhost) by fledge.watson.org (8.11.1/8.11.1) with SMTP id f1HK7sP75315; Sat, 17 Feb 2001 15:07:54 -0500 (EST) (envelope-from patrick@watson.org) Date: Sat, 17 Feb 2001 15:07:54 -0500 (EST) From: Patrick M Doane To: Pierre Weis cc: caml-list@inria.fr Subject: Re: [Caml-list] Typing of default arguments In-Reply-To: <200102170715.IAA11563@pauillac.inria.fr> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Thank you very much for the explanation. I feel silly now for not seeing that derivation initially. Any thoughts about the restriction of polymorphism that can happen when using default arguments? It is still annoying that d' fails to type-check. I would assume that the function could be type-checked as if the default argument did not exist, and then type-check the default value against the signature of the function for consistency. This strategy would then give f and f' these types: val f : g:('a -> 'b) -> 'a -> 'b val f' : ?g:('a -> 'b) -> 'a -> 'b Patrick On Sat, 17 Feb 2001, Pierre Weis wrote: > > I am having difficulty understanding the typing rules for default > > arguments. Here are some test cases: > > > > (* No default arguments: all of these work *) > > let f ~g x = g x > > > > let a = f (fun x -> x) () > > let b = f (fun x -> (x,x)) () > > > > let c = f ~g:(fun x -> x) () > > let d = f ~g:(fun x -> (x,x)) () > > > > (* Default argument: last one fails to type-check *) > > let f' ?(g = (fun x -> x)) x = g x > > > > let a' = f' (fun x -> x) () > > let b' = f' (fun x -> (x,x)) () > > > > let c' = f' ~g:(fun x -> x) () > > let d' = f' ~g:(fun x -> (x,x)) () > > > > If I remove the offending case at the end, I notice that the difference > > between f and f' is: > > > > val f : g:('a -> 'b) -> 'a -> 'b > > val f' : ?g:('a -> 'a) -> 'a -> 'a > > > > So why does the definition for b' typecheck properly? The type of the > > first argument is not 'a -> 'a but rather 'a -> 'a * 'a. > > > > It's unfortunate that supplying a default argument restricts the > > polymorphism and reuse of the function. I would like someway to provide > > the default without losing that polymorphic capability. I think this > > example shows that is should at least be legal to do (from the declaration > > of b'). > > > > Any ideas? > > > > Thanks, > > Patrick Doane > > If f' (fun x -> (x,x)) () can typecheck it is not for a strange magic, > but just because of polymorphism and of the regular default value > treatment. > > Let's see the evaluation process: > > - the expression f' (fun x -> (x,x)) does not provide any argument > labelled g, hence g gets it default value (fun x -> x), hence it > returns the expression (fun x -> g x) with g being (fun x -> x ), > hence it returns (fun x -> x), which is applied in turn to > (fun x -> (x,x)); this application returns (fun x -> (x,x)), which is > the final result. > > - now the expression f' (fun x -> (x,x)) () naturally returns the result > of (f' (fun x -> (x,x))) applied to (), hence (fun x -> (x,x)) applied > to (), hence ((), ()), as observed. > > Now the typing process: > > f' : ?g:('a -> 'a) -> 'a -> 'a = > > f' (fun x -> (x,x)) () : (f' : 'a -> 'a) (fun x -> (x,x)) () > (default value rule) > : (f' : 'a -> 'a) > (fun x -> (x,x) : 'b -> 'b * 'b) () > : (f' : ('b -> 'b * 'b) -> ('b -> 'b * 'b)) > (fun x -> (x,x) : 'b -> 'b * 'b) () > : (f' (fun x -> (x,x)) : ('b -> 'b * 'b)) () > : (f' (fun x -> (x,x)) : unit -> unit * unit) (():unit) > : (f' (fun x -> (x,x)) ()) : (unit * unit) > > This is regular typing, just an amazing side effect of automatic > curryfication and polymorphism. > > Hope this helps, > > Pierre Weis > > INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/ > > > ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr