Including module, coercing

Question

I'm writing a blog entry about how to use OCaml's module system instead of Java's OO-system (a fun perspective). I've come across something I don't understand about coercing. Below is a base module and two modules that includes it:

module M = struct
  type t = int
  let make () = 1
end   
module A = struct
  include M
end
module B = struct
  include M
end

Now A.t and B.t is the same type! Why? It's evidient if you do

let a = A.make();;
let b = B.make();;
[a;b] --> A.t list (* ? *)

I know it's possible to prevent this with private type abbreviations, and then use coercing if you want to put them in the same list. My question is: Why isn't this already done? How can the compiler know that A.t and B.t comes from the same base type?

Regards
Olle

Answer 1

There are a lot of cases where you would want those two modules to be compatible. A simpler use case is the following:

module Hashtbl = struct ... (* definition in the stdlib *) end

module ExtHashtbl = struct ... (* my own layer on top of it *) end

I want ExtHashtbl.t to be compatible with Hashtbl.t, so that I can functions of ExtHashtbl in the middle of code using Hashtbl.t, or to operate on values that have been built by someone else that only knows about the Hashtbl library, and not my own stuff.

In the theory of ML modules there is an operation called "strengthening" that enriches a module definition with as much equations as possible, exposing them in the signature. The idea is that if you want to have more abstraction (less equations), you can always use a type signature to restrict that, so it's strictly more general to have the equations.

The situation is a bit different in the case of functors. Consider that instead of defining A and B as simple modules, you had made them functors on the empty signature:

module A (U : sig end) = struct include M end
module B (U : sig end) = struct include M end

There are then two distinct notions of functors in the ML module systems, the ones that are called "generative" (each invocation of the functor generates "fresh" types that are incompatible with other invocations), and the ones called "applicative" (all invocations of the functor on equal arguments have compatible types). The OCaml system behaves in an applicative way if you instantiate it with a module argument that is named (more generally a path), and in a generative way if you instantiate it with a module argument that is unnamed.

You can learn much more than you ever wanted to know about the OCaml module systems in Xavier Leroy's 2000 paper A Modular Module System (PDF) (from the webpage A few papers on Caml). You will also find below code examples for all the situations I've described above.

Recent work on ML module systems, notably by Anreas Rossberg, Derek Dreyer and Claudio Russo, have a tendency to bring a different viewpoint to the classic distinction between "applicative" and "generative" functors. They claim that they should correspond to "pure" and "impure" functors: functors whose application perform side-effects should always be generative, while functors that only bring pure terms should be applicative by default (with some sealing construct to force incompatibility, hereby providing abstraction).

module type S = sig
  type t
  val x : t
end;;

module M : S = struct
  type t = int
  let x = 1
end;;

(* definitions below are compatible, the test type-checks *)
module A1 = M;;
module B1 = M;;
let _ = (A1.x = B1.x);;

(* definitions below are each independently sealed with an abstract
   signature, so incompatible; the test doesn't type-check *)
module A2 : S = M;;
module B2 : S = M;;
let _ = (A2.x = B2.x);;
(*This expression has type B2.t but an expression was expected of type A2.t*)


(* note: if you don't seal Make with the S module type, all functor
   applications will be transparently equal to M, and all examples below
   then have compatible types. *)
module Make (U : sig end) : S = M;;

(* same functor applied to same argument:
   compatible (applicative behavior) *)
module U = struct end;;
module A3 = Make(U);;
module B3 = Make(U);;
let _ = (A3.x = B3.x);;

(* same functor applied to different argument:
   incompatible (applicative behavior) *)
module V = struct end;;
module A4 = Make(U);;
module B4 = Make(V);;
let _ = (A4.x = B4.x);;
(* This expression has type B4.t = Make(V).t
   but an expression was expected of type A4.t = Make(U).t *)

(* same functor applied to non-path (~unnamed) arguments:
   incompatible (generative behavior) *)
module A5 = Make(struct end);;
module B5 = Make(struct end);;
let _ = (A5.x = B5.x);;
(* This expression has type B5.t but an expression was expected
   of type A5.t *)

Answer 2

I don't understand what is not already done, but:

• Include in ocaml is more like an #include in C, if you want to use classes and inheritance, then, there is that feature: http://caml.inria.fr/pub/docs/manual-ocaml/manual005.html .
• Type inheritance let's ocaml guess that make () is unit -> t. If you don't want ocaml to guess the type, you can define the function signature: http://caml.inria.fr/pub/docs/manual-ocaml/manual004.html#toc14 .