What are abstract module types useful for?

Learning
,
1

abstract module types,

module type T (* specification omitted *)

what’s the use-case for them? What was the motivation to add them to the module language?

According to the manual:

An abstract module type specification module type modtype-name allows the name modtype-name to be implemented by any module type in a matching signature, but hides the implementation of the module type to all users of the signature.

This doesn’t tell much about how to use it or why it’s useful to have. I understand that the manual isn’t too pedagogical, although I wish it had more examples, but I’m just curious about the feature and there doesn’t seem to be much said about it.

My own observations were that ascribing a module to an abstract module type does not work, even if the module was completely empty struct (* --- *) end. using so it doesn’t seem useful inside the module, but perhaps it’s meant to interact with another less-used feature: recursive modules… no idea though.

2

Abstract module types are useful in exactly the same way as abstract types are: given a module of type T, the user will not be able to do anything with it, except pass it to functions or functors expecting such a module type as argument.

Cheers,
Nicolas

7 Likes
3

I think you need a rather complicated setup to see the need for abstract module types :slight_smile: ! I’m guessing you tried to write an .ml file with:

module type S
module Foo : S = struct end
(* Error: Signature mismatch:
     Modules do not match: sig end is not included in S *)

But since the signature S is abstract (not “empty”), this doesn’t typechecks just like it wouldn’t work with abstract types:

type t
let foo : t = ()
(* Error: This expression has type unit
     but an expression was expected of type t *)

So you actually need both an .ml file containing an actual definition, and an .mli that hides/abstracts it:

(* foo.ml *)                                   (* foo.mli *)
module type S = sig                            module type S
  type t
  val unsafe_operation : ... -> t -> ...
  (* etc *)
end

module Bar = struct                            module Bar : S
  type t = int
  let unsafe_operation = (* ... *)
  (* etc *)
end

I named the function unsafe_operation to highlight that the signature S contains dangerous stuff that mustn’t leak outside. This happens when you have complex invariants using internal procedures that you don’t want a user to access directly, as it could break your otherwise safe API. It’s the same motivation as hiding the definition of a type in your mli, since letting the user know it would allow them to do really bad stuff.

So at this point, a user of this module Foo can only know that there exists some module Foo.Bar that implement some signature Foo.S… but they can’t do anything with it: They don’t know that the function unsafe_operation exists, and they can’t implement a new module for this signature. In other words, this is rather useless! You are most likely going to add a functor that allow your user to transform the abstract signature S into a concrete one that they can use:

(* foo.ml *)                                   (* foo.mli *)
module Make (X : S) = struct                   module Make (X : S) : sig
  let safe =                                     val safe : ... -> ...
    (* ... *) X.unsafe_operation (* ... *)
  (* etc *)                                      (* etc *)
end                                            end

Note that we are still able to exploit the definition of the signature S and the existence of the function unsafe_operation from within the file foo.ml ! And now a user is able to write something useful:

module Ok = Foo.Make (Foo.Bar)
let _ = Ok.safe (* ... *)

But but, you could have saved them the trouble since you know that Foo.Make (Foo.Bar) is forced, they can’t ever do anything without first doing this! So your file foo.mli could be a lot simpler with no need for abstracts signatures or functors:

(* foo.ml *)                        (* foo.mli *)
(* ... same as before ... *)        (* remove everything *)

module Ok = Make (Bar)              module Ok : sig
                                      val safe : ... -> ...
                                      (* etc *)
                                    end

Which is why you need a much more complicated setup to really have a need for them… I couldn’t find simple examples in the wild (I’m curious if anyone has some to share?), so forgive me for paraphrasing my own code:

(* foo.mli *)
module type UNSAFE                 (* you don't wanna know what happens in there! *)
module Basic : UNSAFE              (* but here's a simple implementation *)
module Make (X : UNSAFE) : UNSAFE  (* and you can call [Make] multiple times over [Basic] *)
module Public (X : UNSAFE) : sig   (* before finally accessing the safe operations *)
  val safe : ...
  (* etc *)
end

(* this interface constrains the user to do variations on *)
module M = Public (Make (Make (... (Make (Basic)))))

The motivation for this interface is that the functor Make changes the algorithmic complexity of the public functions (so the user should be able to choose how many times they want to call it). But the signature UNSAFE is so terrible that no-one should ever try to re-implement it or use it outside of the module Make or Public: without an abstract signature, I would only be able to beg the user not to look at it!

You probably shouldn’t read the following if you were unfamiliar with the topic before, but the rabbit hole goes deep. The previous interface actually requires Basic to be parametrized by a type provided by the user:

module type UNSAFE
module Basic (Elt : sig type t end) : UNSAFE with type elt = Elt.t
module Make (X : UNSAFE) : UNSAFE with type elt = X.elt
module Public (X : UNSAFE) : sig
  type elt = X.elt
  (* ... *)
end

But this is illegal! Since UNSAFE is abstract, we don’t even know that it contains a type elt and can’t constrain it with type elt = ... The solution then is to wrap the abstract signature inside a functor:

module Private (Elt : sig type t end) : sig
  module type SECRET
end

module type UNSAFE = sig
  module E : sig type t end
  module S : Private(E).SECRET
end

module Basic (Elt : sig type t end) : UNSAFE with type E.t = Elt.t

module Make (X : UNSAFE) : UNSAFE with type E.t = X.E.t

module Public (X : UNSAFE) : sig
  type elt = X.E.t
  (* etc *)
end

Since SECRET is still abstract, when comparing modules of type Private(E).SECRET, the typechecker correctly checks that their E parameters are equal to decide if the resulting SECRET signatures are. This means that the user can’t exploit its knowledge of the signature UNSAFE to switch its module E for something else that wouldn’t be compatible with the type of elements used by the SECRET operations. In other words, you can also expose partially abstracted signatures :slight_smile: .

There’s another motivation for abstract module types: They make the module language incredibly (too) powerful!

let apply (f : 'a -> 'b) (x : 'a) : 'b = f x

(* Can we write this function in the module language? *)

module Apply (F : functor (X : ??) -> ??) (X : ??) : ?? = F (X)

(* Hmm but what should we put in place of the "??"
   as there are no 'a, 'b for modules? *)

module Apply (Forall : sig module type A module type B end)
             (F : functor (_ : Forall.A) -> Forall.B)
             (X : Forall.A)
             : Forall.B
    = F (X)

(* An example usage *)
module S = Apply (struct module type A = Set.OrderedType with type t = int
                         module type B = Set.S with type elt = int
                  end)
                 (Set.Make)
                 (Int)

(* Which gives the same result as *)
module S = Set.Make (Int)

It’s not clear that there are practical examples for this though (but you can definitively go crazy dependent and break the universe.)

10 Likes