A strange example of typing in Ocaml

Question

it is quite strange that this ocaml snippet is well typed by the toplevel. Look at the structure, if g is of type int->int as shown in the toplevel, the h x = g x part of the structure would not be able to get type-unified. So can any one clarify a bit?

module Mymodule : sig
  val h:int ->int
  val g: string-> string
end = struct
  let g x = x
  let h x = g x
end

This is the topelevel's response:

  module Mymodule : sig val h : int -> int val g : string -> string end

Answer 1

The important thing to understand here is that OCaml performs type inference in a compositional manner, i.e., it will first infer type of struct ... end and only then it will match the inferred types against sig ... end to verify that the structure really does implement the signature.

For example, if you write

module Monkey : sig val f : int -> int end =
struct
  let f x = x
end 

then OCaml will be happy, as it will see that f has a polymorphic type 'a -> 'a which can be specialized to the required type int -> int. Because the sig ... end makes Monkey opaque, i.e., the signature hides the implementation, it will tell you that f has type int -> int, even though the actual implementation has a polymorphic type.

In your particular case OCaml first infers that g has type 'a -> 'a, and then that the type of h is 'a -> 'a as well. So it concludes that the structure has the type

sig val g : 'a -> 'a val h : 'a -> 'a end

Next, the signature is matched against the given one. Because a function of type 'a -> 'a can be specialized to int -> int as well as string -> string OCaml concludes that all is well. Of course, the whole point of using sig ... end is to make the structure opaque (the implementation is hidden), which is why the toplevel does not expose the polymorphic type of g and h.

Here is another example which shows how OCaml works:

module Cow =
struct
  let f x = x
  let g x = f [x]
  let a = f "hi"
end

module Bull : sig
  val f : int -> int
  val g : 'b * 'c -> ('b * 'c) list
  val a : string
end = Cow

The response is

module Cow :
    sig 
      val f : 'a -> 'a
      val g : 'a -> 'a list
      val a : string
    end

module Bull :
    sig
      val f : int -> int
      val g : 'a * 'b -> ('a * 'b) list
      val a : string end
    end

Answer 2

I'd say that the string -> string typing isn't applied to g until it's exported from the module. Inside the module (since you don't give it a type) it has the type 'a -> 'a. (Disclaimer: I'm not a module expert, trying to learn though.)