Re: [Caml-list] Typing of default arguments

[Pierre Weis <Pierre.Weis@inria.fr>]

> 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 = <fun>

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