Re: [Caml-list] Typing of default arguments

[Patrick M Doane <patrick@watson.org>]

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