Can't understand the syntax in ocaml code

Question

I have the following code:

module Make_Set (Elt : EQ) : SET with type elt = Elt.t = struct
  type elt = Elt.t
  type t = elt list

  let empty = []

  let rec is_element i set =
    match set with [] -> false | x :: xs -> Elt.eq x i || is_element i xs

  let add i set = if is_element i set then set else i :: set
end

I can't understand the SET with type elt = Elt.t, nor I can find it in the official documentation.

Answer 1

It surely can be found in the official documentation, but more beginner friendly is the corresponding chapter 11 of "Real World OCaml". There is a new edition of this book from 2022.

It can be read here: https://dev.realworldocaml.org/toc.html

Answer 2

The with constraints for module types (as described in the tutorial part of manual and in the reference part) provides a way to refine module types by adding equalities on types, modules or module types.

In your case, the constraint SET with type elt = Elt.t reads: the module type SET refined by adding the information that the type elt is Elt.t.

This is particularly useful when building types derived from other type inside a functor. For instance, let's consider a small module type SHOWABLE

module type SHOWABLE = sig
  type t
  val show: t -> string
end

which specifies modules that provide both a type t and a function show function which convert this type to a string representation.

For instance, an implementation of this specification could be:

module Int_showable = struct
  type t = int
  let show = string_of_int
end

Then, if we have two modules that satisfies the SHOW specification, we can build a Pair module that build a SHOWABLE module from a pair of SHOWABLE module:

module PAIR(X:SHOWABLE)(Y:SHOWABLE) = struct
  type t = X.t * Y.t
  let show (x,y) = String.concat "" ["(";X.show x;", "; Y.show y; ")"]
end

But what is the type of the resulting module?

One might be tempted to answer SHOWABLE. But if we use this module type directly

module Pair(X:SHOWABLE)(Y:SHOWABLE): SHOWABLE = struct
  type t = X.t * Y.t
  let show (x,y) = String.concat "" ["("; X.show x; ", "; Y.show y; ")"]
end
module Int_Pair = Pair(Int_showable)(Int_showable)

we will encounter a type error as soon we try to use the Int_pair module:

let fail = Int_pair.show (1,2)

We get an error

Error: This expression has type 'a * 'b but an expression was expected of type
         Int_pair.t

because the constraint

module Pair(X:SHOWABLE)(Y:SHOWABLE): SHOWABLE 

has restricted the result of PAIR to be exactly a SHOWABLE. And in the module type SHOWABLE, the type t is abstract, in other all concrete information about this type has been erased, and we don't know anymore that Int_pair.t is in fact int * int.

Thus we need a way to describe module type which is SHOWABLE except that the type t should be a pair of X.t and Y.t.

Of course, we could write that directly as:

module Pair(X:SHOWABLE)(Y:SHOWABLE): sig
  type t = X.t * Y.t
  val show: t -> int
end = ...

but then a future read might not spot the fact the resulting module also satisfies the SHOWABLE specification.

The with type constraints are a solution to this issue by providing a way to patch a previous module type by rewriting a type definition:

module type SHOWABLE_INT = SHOWABLE with type t = int

can be read: SHOWABLE_INT is SHOWABLE except that type t = int. In other words, SHOWABLE_INT is

module type SHOWABLE_INT = sig
  type t = int
  val show: t -> int
end

This gives us an easy way to write down the type of the Pair functor:

module Pair(X:SHOWABLE)(Y:SHOWABLE): SHOWABLE with type t = X.t * Y.t = ...

And once, we have added back the right type equality, the previous error is gone:

module Int_Pair = Pair(Int_showable)(Int_showable)
let ok = Int_pair.show (1,2)

and ok is bound to "(1, 2)".