Difference between modules and existentials

Question

It's folk knowledge that OCaml modules are "just" existential types. That there's some kind of parity between

module X = struct type t val x : t end

and

data 'a spec = { x : 'a }
data x = X : 'a spec

and this isn't untrue exactly.

But as I just evidenced, OCaml has both modules and existential types. My question is:

• How do they differ?
• Is there anything which can be implemented in one but not the other?
• When would you use one over the other (in particular comparing first-class modules with existential types)?

Answer 1

Completing gsg's answer on your third point.

There are two kinds of way to use modules:

• As a structuring construct, when you declare toplevel modules. In that case you are not really manipulating existential variables. When encoding the module system in system-F, you would effectively represent the abstract types by existential variables, but morally, it is closer to a fresh singleton type.

• As a value, when using first class modules. In that case you are clearly manipulating existential types.

The other representations of existential types are through GADT's and with objects. (It is also possible to encode existential as the negation of universal with records, but its usage are completely replaced by first class modules).

Choosing between those 3 cases depend a bit in the context. If you want to provide a lot of functions for your type, you will prefer modules or objects. If only a few, you may find the syntax for modules or objects too heavywheight and prefer GADT. GADT's can also reveal a the structure of your type, for instance:

type _ ty =
  | List : ty -> ty list
  | Int : int list

type exist = E : 'a ty * 'a -> exist

If you are in that kind of case, you do not need to propagate the function working on that type, so you will end up with something a lot lighter with GADT's existentials. With modules this would look like

module type Exist = sig
  type t
  val t : t ty
end
module Int_list : Exist = struct
  type t = int list 
  let t = List Int
end
let int_list = (module Int_list:Exist)

And if you need sub-typing or late binding, go for the objects. This can often be encoded with modules but this tend to be tedious.