Type of high order functions

Question

if I set the correct type (I think) for a higher order function, the OCaml compiler rejects the use of this function second .

The code

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

results in 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 

Thus, the first use of f apparently fixes the type of its first parameter to int -> string . I could understand that. But I don’t understand that the exception of type restriction on f fixes the problem.

 let foo ():string = let fgv = gv in let h = string_of_int in let i = string_of_float in let x = fh 23 in let y = fi 23.0 in x ^ y 

And moving f to the global scope also fixes the problem:

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

Why is the first example not compiled, but later?

Answer 1

Let me use a simpler example to illustrate the problem.

 # 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 xy = x :: y in (cons3 1 [], cons3 true []);; - : int list * bool list = ([1], [true]) 

cons0 is a definition of a polymorphic function defined in the global domain. This is just a trivial wrapper for the :: operator. Not surprisingly, the definition works. cons1 almost matches cons0 , except that its scope is limited to the expression in body in . Changing the area looks harmless, and, of course, these are typechecks. cons3 again the same function without type annotation, and we can use it polymorphically in the in body.

And what happened to cons2 ? The problem is 'a : area: this is a whole top-level phrase. The semantics of the phrase that cons2 defines are

 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 [] , it is not possible to instantiate 'a . Therefore, the phrase is not typical.

If you like to think about what ML is typed in terms of a regular type determination algorithm, each explicit user variable introduces a set of constraints in the unification algorithm. Here the limitations are 'a = "type of the parameter x" and ' = "type of the parameter y" . But region 'a is the whole phrase, it does not generalize in any inner region. So int and bool both combine into non-generic 'a .

Recent versions of OCaml introduce type variables (as in Nicki Yoshiuchi's Answer ). The same effect could be achieved using the 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 thug, and I won’t be surprised if this is a compiler error. However, you can do what you want by explicitly specifying the type:

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

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

Edit:

This also works:

 let fgv:string = gv in 

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

It is strange that it does not work when you comment on the type of arguments.

EDIT:

Polymorphic annotations have a special syntax:

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

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

Answer 3

As a control point, the equivalent of F #

 let foo ():string = let f: ('a -> string) -> 'a -> string = fun gv -> gv let h = string let i = string let x = fh 23 let y = fi 23.0 x ^ y 

compiles.