Tony's Wiki

Cyclic type definitions in OCaml with opaque sealing

3 min read

The example in this passage is related to A Type System for Recursive Modules’s comment:

Recursive modules provide a natural means of writing down cyclic type definitions that span module boundaries. However, existing recursive module proposals differ on what kinds of cyclic type definitions they consider permissible. … A more restrictive approach is the one taken by Leroy (2003) and Nakata and Garrigue (2006), who permit cycles between transparent type definitions, but only if they are intercepted by the use of opaque sealing. For instance, suppose we were to modify the example in Figure 1 so that internally A.t were defined to equal int * X.A.t. The resulting cyclic definition would be permissible in OCaml and Traviata because the type cycle is broken by the use of opaque sealing in the definition of module A.

The passage describes the mechanism OCaml (and similar systems like Traviata) uses to permit certain cyclic type definitions within recursive modules, specifically by using opaque sealing to “break” the cycle.

The OCaml example demonstrating this permissible cyclic definition is:

The OCaml Example

This example defines a recursive module X whose structure A contains a type t that is defined recursively in terms of itself, but the recursion is intercepted by the opaque sealing using the module type (SOME_SIG).

1. Define the Signature (SOME_SIG)

The signature requires that the type t be abstract, hiding its recursive definition.

OCaml

module type SOME_SIG = sig
  (* t is declared abstract/opaque *)
  type t 
  (* Other definitions, possibly using t *)
end

2. The Recursive Module Definition

The module X is defined recursively. The internal structure A_impl has the cyclic definition, but the public structure A is sealed with SOME_SIG, making A.t opaque to the outside world.

OCaml

module rec X : sig
  (* The recursive type environment requires X.A to be opaque *)
  module A : SOME_SIG
end = struct
  (* The internal structure contains the cyclic, transparent definition *)
  module A_impl = struct
    (* type t = int * X.A.t is the cyclic definition *)
    type t = int * X.A.t 
  end

  (* Opaque Sealing: This line breaks the transparent cycle.
     The public module A is constrained by SOME_SIG, hiding the definition
     A.t = int * X.A.t
  *)
  module A : SOME_SIG = A_impl
end

Explanation of Why This Works (Opaque Sealing)

  1. Transparent Cycle (Internal): The definition inside A_impl (type t = int * X.A.t) creates a transparent type cycle: A.t→⋯→X.A.t→A.t. If this module were not sealed, the type system would struggle with this unbounded expansion (t would be transparently equal to an infinite tuple).

  2. Opaque Sealing (External): By constraining the final module A with SOME_SIG (which declares type t), the definition is made abstract/opaque. The type system knows that A contains a type named t, but it only knows it as the abstract path X.A.t.

  3. The “Break”: Because X.A.t is treated as a simple abstract name for the purpose of the surrounding type environment, the internal expansion is contained. The cycle is “broken” by the abstraction boundary, allowing the OCaml type system to accept the definition as sound, even though it contains a recursive type. The actual type is essentially treated as a recursive type μt.(int×t), but its complex structure is concealed by the module boundary.

Graph View

Backlinks