Section 5.1 of What is a recursive module?

Elaboration of Recursively Dependent Signatures

The authors of the paper are describing a problem and proposing a solution for it.

The Problem: A Clash Between Programmer Convenience and Compiler Rules

[cite_start]The core issue in Section 5.1 is a conflict between the external language (what a programmer writes) and the internal language (what the compiler formally requires)[cite: 437, 438].

[cite_start]The internal language has a strict rule: all recursively dependent signatures (rds’s) must be fully transparent and contractive[cite: 437]. This means every type within the signature must be completely defined. [cite_start]However, forcing a programmer to manually write out these exhaustive definitions every time is “burdensome” and impractical[cite: 438].

---

The Proposed Solution: Automatic Transformation by the Compiler

[cite_start]The authors propose a solution where the compiler’s elaborator (the part that processes the code) automatically transforms the programmer’s simpler, incomplete signatures into the fully transparent and contractive form that the internal language demands[cite: 439].

The solution works by “hoisting” abstract types. [cite_start]The elaborator identifies any types that are not fully defined within the recursive signature, creates definitions for them outside of the signature, and then rewrites the original signature to refer to these new, external definitions[cite: 443]. This makes the recursive part of the signature fully transparent, satisfying the compiler’s rule without burdening the programmer.

For example, a non-transparent signature like:

rec S: sig
  type t
  type u = S.u -> t
end

can be automatically transformed by the elaborator into a permissible one:

sig
  type t'
  structure rec S :
    sig
      type t = t'
      type u = S.u -> t
    end
end

[cite_start]In this transformed version, the inner rec S signature is now fully transparent because t is explicitly defined [cite: 448-457].

However, the authors note that this solution has limitations. [cite_start]It can fail when a signature involves unknown type constructors, because the elaborator cannot determine if a type is truly abstract and can be hoisted, or if its definition is simply hidden within the unknown constructor[cite: 468, 477].