type of high order functions

Question

if I specify the (I think) correct type for a high order function the OCaml compiler rejects the second usage of that function.

The code

let foo ():string  =
    let f: ('a -> string) -> 'a -> string = fun g v -> g v
    in let h = string_of_int
    in let i = string_of_float
    in let x = f h 23
    in let y = f i 23.0
    in x ^ y

leads to the following error message

File "test.ml", line 6, characters 14-15:
Error: This expression has type float -> string
       but an expression was expected of type int -> string

So the first usage of f seems to fix the type of its first parameter to int -> string. I could understand that. But what I don't get is that omitting the type restriction on f fixes the problem.

let foo ():string  =
    let f g v = g v
    in let h = string_of_int
    in let i = string_of_float
    in let x = f h 23
    in let y = f i 23.0
    in x ^ y

And moving f to global scope fixes the problem, too:

let f: ('a -> string) -> 'a -> string = fun g v -> g v

let foo ():string  =
  let h = string_of_int
  in let i = string_of_float
  in let x = f h 23
  in let y = f i 23.0
  in x ^ y

Why is it that the first example does not compile while the later ones do?

Answer 1

Let me use a simpler example that illustrates the issue.

# let cons0 (x : 'a) (y : 'a list) = x :: y;;
val cons0 : 'a -> 'a list -> 'a list = <fun>
# let cons1 (x : 'a) (y : 'a list) = x :: y in cons1 1 [];;
- : int list = [1]
# let cons2 (x : 'a) (y : 'a list) = x :: y in (cons2 1 [], cons2 true []);;
This expression has type bool but is here used with type int
# let cons3 x y = x :: y in (cons3 1 [], cons3 true []);;
- : int list * bool list = ([1], [true])

cons0 is a polymorphic function definition, defined at global scope. It's just a trivial wrapper to the :: operator. Unsurprisingly, the definition works. cons1 is almost the same as cons0, except that its scope is limited to the expression in the in body. The change of scope looks innocuous, and sure enough, it typechecks. cons3 is again the same function, with no type annotation, and we can use it polymorphically in the in body.

So what's wrong with cons2? The problem is the scope of 'a: it's the whole toplevel phrase. The semantics of the phrase that defines cons2 is

for some type 'a, (let cons2 (x : 'a) (y : 'a list) = ... in ...)

Since 'a must be compatible with int (due to cons3 1 []) and with bool (due to cons3 true [], there is no possible instantiation of 'a. Therefore the phrase is ill-typed.

If you like to think about ML typing in terms of its usual type inference algorithm, each explicit user variable introduces a set of constraints in the unification algorithm. Here the constraints are 'a = "type of the parameter x" and ' = "type of the parameter y". But the scope of 'a is the whole phrase, it's not generalized in any inner scope. So int and bool both end up unified to the non-generalized 'a.

Recent versions OCaml introduce scoped type variables (as in Niki Yoshiuchi's answer). The same effect could have been achieved with a local module in earlier versions (≥2.0):

let module M = struct
    let cons2 (x : 'a) (y : 'a list) = x :: y
  end in
(M.cons2 1 [], M.cons2 true []);;

(Standard MLers note: this is one place where OCaml and SML differ.)

Answer 2

This is a real head-scratcher and I wouldn't be surprised if it's a compiler bug. That said, you can do what you want by explicitly naming the type:

let f (type t) (g: t->string) (v: t) = g v in

From the manual: http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#htoc108

Edit:

This also works:

let f g v:string = g v in

which has the type signature you are looking for: ('a -> string) -> 'a -> string

Strange that it doesn't work when you annotate the type of the arguments.

EDIT:

Polymorphic type annotations have a special syntax:

let f: 'a. ('a -> string)-> 'a -> string = fun g v -> g v in

And the type is required to be polymorphic: http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc79