OCaml functors :: counter-intuitive behaviour

Question

I am experimenting with the module language of OCaml (3.12.1), defining functors and signatures for modules and so on, mostly following the examples from Chapter 2 of the OCaml manual and I've stumbled, by accident, on a situation where apparently my mental model of how functors and module signatures work is flawed. I tried to narrow the situation I encountered to the shortest amount of code possible so don't ask what I am trying to accomplish, this is a totally contrived example to demonstrate the OCaml feature in question.

So, we have a functor that simply provides an identity function f and is parametrized by a module supplying the type of that function's input parameter. Totally contrived example like I said.

module type SOMETYPE = sig type t end ;;
module Identity = functor (Type: SOMETYPE) -> struct let f (x: Type.t) = x end ;;

Given the above, we proceed to define a module to supply the int type:

module IntType = struct type t = int end ;;

.. and then we use the functor to generate a module for the int identity function:

module IdentityInt = Identity(IntType) ;;                     

Sure enough the generated module and its f function behave as expected:

#IdentityInt.f(3) + 10 ;;
- : int = 13

The mental model of functors being functions that take modules as inputs and return modules seems to be serving us right so far. The Identity functor expects as input parameter a module of signature (module type) SOMETYPE, and indeed the module we supplied (IntType) has the correct signature and so a valid output module is produced (IdentityInt) whose f function behaves as expected.

Now comes the un-intuitive part. What if we would like to make it explicit that the supplied module IntType is indeed a SOMETYPE type of module. As in:

module IntType : SOMETYPE = struct type t = int end ;;

and then generate the functor's output module the same way as before:

module IdentityInt = Identity(IntType) ;;

... let's try to use the f function of the newly generated module:

IdentityInt.f 0 ;;

Whereupon the REPL complains with:

"Error: This expression [the value 0] has type int but an expression was expected of type IntType.t."

How can providing redundant but correct type information break the code? Even in case A the functor module Identity had to treat the IntType module as SOMETYPE type. So how come explicitly declaring IntType to be SOMETYPE type yields a different outcome?

Answer 1

The : construct is different in the core language and in the module language. In the core language, it is an annotation construct. For example, ((3, x) : 'a * 'a list) constrains the expression to have some type that is an instance of 'a * 'a list; since the first element of the pair is an integer, let (a, b) = ((3, x) : 'a * 'a list) in a + 1 is well-typed. The : construct on modules does not mean this.

The construct M : S seals the module M to the signature S. This is an opaque seal: only the information given in the signature S remains available when typing uses of M : S. When you write module IntType : SOMETYPE = struct type t end, this is an alternate syntax for

module IntType = (struct type t end : SOMETYPE)

Since the type field t in SOMETYPE is left unspecified, IntType has an abstract type field t: the type IntType is a new type, generated by this definition.

By the way, you probably meant module IntType = (struct type t = int end : SOMETYPE); but either way, IntType.t is an abstract type.

If you want to specify that a module has a certain signature while leaving some types exposed, you need to add an explicit equality for these types. There's no construct to add all inferable equalities, because applying a signature to a module is usually meant for information hiding. In the interest of simplicity, the language only provides this one generative sealing construct. If you want to use the defined signature SOMETYPE and retain the transparency of the type t, add a constraint to the signature:

module IntType = (struct type t = int end : SOMETYPE with type t = int)

Answer 2

If you look at the inferred signature when you don't write something explicitly:

# module IntType = struct type t = int end ;;
module IntType : sig type t = int end

The signature exposes that t is an int. Your signature, on the contrary:

# module IntType : SOMETYPE = struct type t = int end ;;
module IntType : SOMETYPE

is really:

# module IntType : sig type t end = struct type t = int end ;;
module IntType : sig type t end

This seems to solve your problem:

# module IntType : (SOMETYPE with type t = int) = struct type t = int end ;;
module IntType : sig type t = int end
# module IdentityInt = Identity(IntType) ;;
module IdentityInt : sig val f : IntType.t -> IntType.t end
# IdentityInt.f 0 ;;
- : IntType.t = 0

(you don't need the parens, but they help mentally parse). Basically, you expose the fact that t is an int with your signature. So that OCaml knows the equality IntType.t = int.

For more details of the internals, I'll leave it to more knowledgeable people.

Answer 3

When you write:

module IntType : SOMETYPE = struct type t = int end ;;

You are constraining the signature of InType to be exactly SOMETYPE. This means, for instance, that the type t is now becoming an abstract type (whose implementation is unknown to the typer).

So IdentityInt.f type is still IntType.t -> IntType.t, but, by using a signature constraint, you've explicitly removed the equation IntType.t = int from the typer knowledge. The error message you get tells you exactly that.