[Caml-list] Typing of default arguments

[Caml-list] Typing of default arguments

[Patrick M Doane]

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

-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

Re: [Caml-list] Typing of default arguments

[Pierre Weis]

> 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

Re: [Caml-list] Typing of default arguments

[Patrick M Doane]

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

Re: [Caml-list] Typing of default arguments

[Jacques Garrigue]

From: Patrick M Doane <patrick@watson.org>

> 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

Since the default value for g is (fun x -> x), when g is omitted 'a =
'b should be enforced.
Otherwise, (fun x -> f' x) would be of the magic type ('a -> 'b),
which is certainly not what you are asking for.
Enforcing such a conditional equation is possible, but this would
means yet another extension to the type system:

    val f' : ?g:('a -> 'b ?= 'c -> 'c) -> 'a -> 'b

meaning that the default value for g has type 'c -> 'c.
Two problems: is it really worth it (you are not the first one to ask
for that, but would this improve a lot programming style?), and what
are the consequences. In particular it would probably mean more
polymorphic types at places where you do not really need them,
requiring more type annotations to make them readable.

    Jacques
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr