[Camllist] Ocaml 3.01: bug or feature?

Anton Moscal
 Jacques Garrigue
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20010317 (10:58) 
From:  Jacques Garrigue <garrigue@k...> 
Subject:  Re: [Camllist] Ocaml 3.01: bug or feature? 
> 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 1314: > 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.kyotou.ac.jp/~garrigue/papers/. You can make it work by explicitly giving a (nonpolymorphic) 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 counterexample, 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 farfetched, but we will have to solve it someday. Cheers, Jacques  To unsubscribe, mail camllistrequest@inria.fr. Archives: http://caml.inria.fr