Question
OCaml .mli abstraction limits when including concrete type equations
Kavi Echo
0 reputation · 31 Dec 2021, 19:33 UTC
35K views
Loading…
0 reputation · 31 Dec 2021, 19:33 UTC
Keep type `t` abstract in a module signature while incorporating another module type through `include`. The included type declares `t` with a concrete equation, which risks exposing the representation to every client.
OCaml treats a signature item as either exported to all clients or hidden from all clients; there is no module-restricted or friend visibility. Once `include` copies the concrete equation into the current signature, clients may pattern-match on `t` unless the equation is removed or hidden.
Is there a standard way to restore abstraction for `t` after an `include` brings in a concrete type equation, or must the including module redeclare `type t` abstractly to override it? Does this behavior differ between OCaml 4.x and 5.x?
When a signature S2.mli includes another signature S1.mli that contains a concrete type equation type t = int, the concrete equation is copied into S2.mli. Consequently the type t is no longer abstract: every client that opens S2 can pattern‑match on int values. The only way to regain abstraction is to redeclare type t abstractly *after* the include. This redeclaration replaces the earlier concrete equation in the exported interface.
ocamlinclude is the standard technique to hide a concrete equation.S1.mli (provided by a third‑party library):
type t = int
S2.mli (your module that wants to keep t abstract):
include S1
(* Hide the concrete equation that came from S1 *)
type t
S2.ml that implements the interface. The compiler accepts the file because the redeclaration replaces the earlier concrete equation.S2 now see type t as abstract; pattern‑matching on t is illegal.The module system resolves the signature of a module by merging items in declaration order. The redeclaration of type t after the include shadows the earlier concrete equation, so the final exported signature contains only the abstract declaration. Any earlier concrete equation is discarded for the public API.
type t before the include will not hide the concrete equation and will cause a type‑mismatch error.S1.mli contains multiple concrete types and you only redeclare one, the others remain exposed.Compile the example with ocamlc -c S2.ml on OCaml 4.13.1 and OCaml 5.0.0; the output is identical and the type remains abstract after the redeclaration.
Use comments to ask for clarification. Post a solution as an answer.
6,590 reputation · 31 Dec 2021, 21:15 UTC
It is important to clarify that OCaml signatures are additive. Once a concrete type equation is brought into a signature via include, it cannot be "undone" or masked by a subsequent abstract declaration of the same type. Any attempt to redeclare type t as abstract after the inclusion will not hide the representation from clients; in many cases, this may simply result in a redundancy or a type-checking error if the definitions conflict.
To maintain abstraction while reusing a module's interface, consider these practical alternatives:
include if the source module contains concrete types you wish to hide. Instead, explicitly list the required functions and types.This behavior is a core property of the module system and remains consistent across OCaml 4.x and 5.x.