Module, what does "with type" do?

Question

module type ORDER = sig 
  type t 
  val leq : t -> t -> bool
  val equal : t -> t -> bool
end 

module Int:ORDER with type t = int = struct
  type t = int
  let leq = (<=)
  let equal = (=)
end

Can someone explain to me this line :

    module Int:ORDER with type t = int = struct
    this --> with type t = int 

I've tried without it :

Int.equal 3 3
Line 1, characters 10-11:
Error: This expression has type int but an expression was expected of type
         Int.t

I can see what "It does", but I'm unable to explain it in words what it is happening, thank you

Answer 1

The colon operator in a module expression isn't just a signature constraint, it's also an abstraction construct. M : S requires the module M to have the signature S, and tells the compiler to forget everything about typing of M except for what is specified in S. This is where abstraction is born.

Given the definition module Int: S = struct … end (which is syntactic sugar for module S = (struct … end : S)), all the compiler knows about the types of elements of Int is what is recorded in S. If S is ORDER, its type t is abstract, and therefore Int.t is an abstract type: the fac that Int.t is actually an alias for int is hidden. Hiding the real implementation of a type is exactly what abstract types are about.

The signature that is actually desired for Int is

sig
  type t = int
  val leq : t -> t -> bool
  val equal : t -> t -> bool
end

This is almost exactly the signature called ORDER, but with the type t being an alias for int rather than abstract. The with type construct allows using the name ORDER to construct the module type expression above. Given the definition of ORDER, writing

module Int : ORDER with type t = int = struct … end

is equivalent to writing

module Int : sig
  type t = int
  val leq : t -> t -> bool
  val equal : t -> t -> bool
end = struct … end

Since the type Int.t is transparently equal to int, it can be used interchangeably with int.

A ORDER signature is mostly useful to pass the type to functors like Set and Map that build data structures that rely on an ordering relation for their elements. The data structure only depends on the abstract properties of the order relation, but the code that uses the data structure can still be aware of the type of the elements (thanks to another with type constraint, this one equating the type of data structure elements with the type of the functor argument). See “functors and type abstraction” in the language introduction.