[Caml-list] Ocaml 3.01: bug or feature?

[Caml-list] Ocaml 3.01: bug or feature?

[Anton Moscal]

Hello!

When I try to compile the following program by Ocaml 3.01:

let f ?(a=1) b = a + b
let (+>) x f = f x
let _ = 1 +> f

I get following message:

File "bug.ml", line 3, characters 13-14: 
This expression has type ?a:int -> int -> int 
but is here used with type 'a ->'b

With Ocaml 3.00 all worked fine.

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

Re: [Caml-list] Ocaml 3.01: bug or feature?

[Jacques Garrigue]

> When I try to compile the following program by Ocaml 3.01:
> 
> let f ?(a=1) b = a + b
> let (+>) x f = f x
> let _ = 1 +> f
> 
> I get following message:
> 
> File "bug.ml", line 3, characters 13-14: 
> This expression has type ?a:int -> int -> int 
> but is here used with type 'a ->'b
> 
> With Ocaml 3.00 all worked fine.

You stumbled on a very interesting glitch :-(

If I remember correctly, this would work in 3.00 in classic mode, but
not in commuting label mode. 3.01 is a bit more conservative, so this
doesn't work in both.

The problem is that the type of the expected function ('a -> 'b) is
not precise enough to be sure whether this would be legal or not to
discard ?a:int. The notion of legality is with respect to a set of
untyped reduction rules, which you can find in my recent paper
"Labeled and optional arguments for Objective Caml" at
http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/.

You can make it work by explicitly giving a (non-polymorphic) type for
the return value of f:
  # let (+>) x f : int = f x;;
  val ( +> ) : 'a -> ('a -> int) -> int = <fun>
  # 1 +> f;;
  - : int = 2

Considering commuting label mode, here is an example which would
create semantical problems:
   # let f ?(a=1) b ~a:c = a + b + c;;
   val f : ?a:int -> int -> a:int -> int
   # let id (x : 'a -> 'b) = x;;
   val id : ('a -> 'b) -> 'a -> 'b
   # let g = id f;;
   val g : int -> a:int -> int
   # g ~a:2;;
   - : int -> int
According to the untyped semantics, this application on ~a is the
first argument (indiretcly) passed to f, so it should really replace
the first ?a, so that the type of the result should be "int -> a:int
-> int", and indirectly the type of g was wrong.
This is subtle, and this is a rather unusual style of coding, but this
would make the system unsound, so this is prohibited.

For classic mode, the situation is even worse, and in fact the current
version is not 100% sound. Here is a counter-example, that is accepted
by the compiler:
  # let f ?(a=1) b = print_int (a+b);;
  val f : ?a:int -> int -> unit = <fun>
  # let g ~f = f ~a:2;;                
  val g : f:(a:int -> 'a) -> 'a = <fun>
  # let h ~(f : int -> unit) ~g = ignore (g ~f);;
  val h : f:(int -> unit) -> g:(f:(int -> unit) -> 'a) -> unit = <fun>
  # h ~f ~g;;
  3- : unit = ()
According to the untyped semantics, we are really applying f on ~a:2, so
there should be no output.
Again, this is pretty far-fetched, but we will have to solve it
someday.

Cheers,

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