[Caml-list]Warning 20: this argument will not be used by the function.

[Caml-list]Warning 20: this argument will not be used by the function.

[AUGER Cedric]

Hi all,
while playing with coq and extraction I did the following:

"
Fixpoint narity (n: nat) : Set :=
match n with
|  O  => nat
| S n => nat -> (narity n)
end.

Definition sum_aux : nat -> forall n, narity n :=
fix sum acc n :=
match n as n0 return narity n0 with
|  O  => acc
| S n => fun m => sum (m+acc) n
end.

Definition sum := sum_aux O.

Eval compute in sum 3 14 67 21.

Recursive Extraction sum.
"

I do not want to comment if this is or not meaningfull, but adapting
the code to caml ints (not doing so will do the same thing, but ints
are easier to play with), I got:

        Objective Caml version 3.12.0

# type __ = Obj.t
  ;;
type __ = Obj.t
# let rec sum_aux acc n = if n <= 0
  then Obj.magic acc
  else Obj.magic (fun m -> sum_aux (m+acc) (n-1));;
val sum_aux : int -> int -> 'a = <fun>
# let sum = sum_aux 0;;
val sum : int -> 'a = <fun>
# print_int (sum 3 14 67 21);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
102- : unit = ()

The result is correct, but the warning is quite unexpected!
(Changing the values of the arguments will of course change the result)

It is not important or armfull, but quite funny.

Re: [Caml-list]Warning 20: this argument will not be used by the function.

[John Carr]

> Warning 20: this argument will not be used by the function.

See also warning 21:

# let f () = assert false; 0;;
Warning 21: this statement never returns (or has an unsound type.)
val f : unit -> int = <fun>

Assert behaves like a function with type bool -> 'a.  The return type is
an unconstrained type, a type variable not mentioned on the left hand
side of the arrow.  Functions with such type never return or have
unsound type.  Your example used Obj.magic and has unsound type.

A more verbose version of warning 20 would explain

Warning 20: this argument will not be used by the function (or the function has an unsound type).


    --John Carr (jfc@mit.edu)

Re: [Caml-list]Warning 20: this argument will not be used by the function.

[Philippe Wang]

On Wed, Aug 31, 2011 at 12:31 AM, John Carr <jfc@mit.edu> wrote:
> # let f () = assert false; 0;;
> Warning 21: this statement never returns (or has an unsound type.)
> val f : unit -> int = <fun>

> Assert behaves like a function with type bool -> 'a.  The return type is
> an unconstrained type, a type variable not mentioned on the left hand
> side of the arrow.

Actually, assert is more like a function with type bool -> unit.
Indeed, (assert false) is a special case where it is "so obvious that
it'll raise an exception that it's made type 'a".

Notably, if you write
assert(1=2)
it's not "obvious enough" for the compiler to assume it will raise an
exception.
(Which is normal, by the way, because it's generally an undecidable
problem: in general, it's not possible to know that the evaluation of
assert's argument will return a value, especially when there is a
function application such as in "1=2".)

So,
in
let f () = assert false
f : unit -> 'a
let f () = assert (1=2)
f : unit -> unit

And while
let f () = assert false; 0;;
raises a warning,
let f () = assert (1=2); 0;;
won't raise any.

Somehow, the choice of discriminating (assert false) is not so perfect...

Cheers,

--
Philippe Wang


N.B. Sorry for double-replying.
I wonder if "reply-to: caml-list@inria.fr" field could be added
automatically to headers of all mails received by the list...

Re: [Caml-list]Warning 20: this argument will not be used by the function.

[Esther Baruk]

[-- Attachment #1: Type: text/plain, Size: 2034 bytes --]

In fact 'assert false' is explicitely replaced by 'raise
Assert_failure(...)' by the parser.
See the documentation about that in the "Language extensions" section.

With any other argument than false, assert is considered to have type bool
-> unit



Esther Baruk


On Wed, Aug 31, 2011 at 1:40 AM, Philippe Wang <mail@philippewang.info>wrote:

> On Wed, Aug 31, 2011 at 12:31 AM, John Carr <jfc@mit.edu> wrote:
> > # let f () = assert false; 0;;
> > Warning 21: this statement never returns (or has an unsound type.)
> > val f : unit -> int = <fun>
>
> > Assert behaves like a function with type bool -> 'a.  The return type is
> > an unconstrained type, a type variable not mentioned on the left hand
> > side of the arrow.
>
> Actually, assert is more like a function with type bool -> unit.
> Indeed, (assert false) is a special case where it is "so obvious that
> it'll raise an exception that it's made type 'a".
>
> Notably, if you write
> assert(1=2)
> it's not "obvious enough" for the compiler to assume it will raise an
> exception.
> (Which is normal, by the way, because it's generally an undecidable
> problem: in general, it's not possible to know that the evaluation of
> assert's argument will return a value, especially when there is a
> function application such as in "1=2".)
>
> So,
> in
> let f () = assert false
> f : unit -> 'a
> let f () = assert (1=2)
> f : unit -> unit
>
> And while
> let f () = assert false; 0;;
> raises a warning,
> let f () = assert (1=2); 0;;
> won't raise any.
>
> Somehow, the choice of discriminating (assert false) is not so perfect...
>
> Cheers,
>
> --
> Philippe Wang
>
>
> N.B. Sorry for double-replying.
> I wonder if "reply-to: caml-list@inria.fr" field could be added
> automatically to headers of all mails received by the list...
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

[-- Attachment #2: Type: text/html, Size: 3106 bytes --]