related-work-cyclic-types-rewrite-plan

Related Work: cyclic types / contractiveness rewrite plan and fact check

Date: 2026-05-18 23:00 CST

Scope: This note focuses on the proposed rewrite of \subsection{Cyclic types and contractiveness}. I did not modify any TeX source. I used the current draft files, modules.bib, and the Zotero-exported PDFs under /Users/ltzhou/Downloads/Recursive Modules; I did not inspect legacy material.

1. Bottom line

I agree with your proposed direction: do not foreground the terms “static-on-static” and “dynamic-on-static”. They are historically useful, but if they become the main narrative, the paragraph sounds as if our contribution is merely to re-enable a class of dependencies that later work intentionally forbade. The better story is:

1. CHP identifies the core difficulty: recursive module signatures can induce recursive equations among static components, especially transparent type components and higher-kinded type constructors.
2. CHP’s transparent account requires higher-kinded equirecursive constructors, but constructor equivalence at higher kinds, in the presence of singleton/share information, was not known to be decidable/practical.
3. Later recursive-module systems choose various approximations: forward declarations plus contractive realizations (Moscow ML/Russo), destination-passing/backpatching of abstract type names with conservative cycle checks (RTG/RMC), opacity/path-resolution based acceptance (OCaml/Traviata), weak-bisimilarity based declarative accounts plus algorithmic restrictions (Im et al. 2011), and semantic contractiveness for recursive types with abstract types (Im et al. 2013).
4. Our paper reopens the CHP design point by making the static cycles explicit in the target calculus: the static pass synthesizes \mu-types in \Fomegarec/\Momega rather than relying on implicit source-level path equality. This gives a grounded account of when cycles are contractive and avoids order-sensitive rejection of some programs.
5. The subtle correspondence with Dreyer is worth highlighting: RTG/RMC’s backpatching/destination-passing is a disciplined way to forward-declare abstract type names and fill them later. In our single-vision opaque/transparent modes, hiding secret types behind abstract types plays a functional analogue of that backpatching role. Separately, transparent signatures and applicative functors force genuine static recursive equations, which we solve by target \mu-types. This is a good conceptual bridge, but I would state it as an analogy, not by using the terms as the main organizing principle.

2. Fact check of the current paragraph

2.1 CHP

Current draft says:

CHP proposed transparent external signatures with higher-kinded equi-recursive constructors, but the problem of deciding equivalence at higher kinds is not known to be decidable.

Fact check:

• Directionally correct, but too compressed.
• CHP (“What is a recursive module?”) uses recursively dependent signatures and an external signature discipline that must be fully transparent in the phase-splitting account. The target type theory includes higher-kinded equirecursive constructors and singleton kinds.
• CHP’s exact claim is not “undecidable”; it is that constructor equality is made difficult by singleton kinds and equirecursive constructors, and at that time neither problem was known to be decidable. For equirecursive constructors, Amadio–Cardelli decide equality at kind type, but the algorithm does not extend to higher kinds; CHP mentions later work suggesting decidability at higher kinds but not by a practical algorithm.

Safer wording:

CHP showed that transparent recursive module signatures can induce recursive equations among type components and type constructors. Their type-theoretic account supports such equations using higher-kinded equirecursive constructors and singleton kinds, but equality for these constructors was not known to have a practical decidable algorithm in the generality required by ML modules.

2.2 “Subsequent work adopted dynamic-on-static restriction”

Current draft says:

Subsequent work adopted the dynamic-on-static restriction, forbidding static-on-static cycles.

I would not keep this as written.

What is correct:

• Dreyer’s thesis explicitly describes the “dynamic-on-static” restriction in the context of recursively dependent signatures: recursive references may occur from the dynamic part of a signature to the static part, but not in transparent type specifications that create static cycles.
• Dreyer also says this restriction avoids extending the core language with equirecursive types.

What is misleading:

• “Subsequent work” is too broad. Russo/Moscow ML, RMC, Traviata, OCaml, and Im et al. do not all implement exactly the same named restriction.
• RMC’s key story is not simply “dynamic-on-static”; it is RTG-style recursive type generativity plus static typechecking and conservative rejection of transparent type cycles.
• Im et al. 2011 explicitly address cyclic type definitions and try to reject only transparent cycles algorithmically.

Better wording:

Later systems avoided the full CHP equality problem in different ways. Some restrict recursive references so that forward-declared type names may be used by value components but not by transparent type equations. RMC instead combines RTG-style forward declaration of abstract type names with conservative checks that rule out transparent type cycles. OCaml and Traviata accept more cycles when opacity cuts the observable equality, while Im et al. give a weak-bisimilarity account and an algorithmic fragment that rejects transparent cycles.

This expresses the same idea without making the named taxonomy the main narrative.

2.3 Moscow ML / Russo

Current draft says:

MoscowML further requires opaque forward-declared types to be implemented by datatype replication, so opaque recursive types are barely expressible.

This is too strong and probably reviewer-risky.

What Russo/Moscow ML actually supports:

• Russo’s “Recursive structures for Standard ML” is explicitly designed to support cyclic dependencies between both types and terms defined in separate modules.
• It uses forward signatures and checks that the implementation enriches them under a contractive realization of forward type components.
• Mini-SML has datatype definitions and datatype replication; datatype replication is used to copy a datatype into another scope while preserving compatibility.
• It supports important mutually recursive datatype examples across structures.

What it does not support / limitations:

• It does not solve double vision in the RTG/RMC sense.
• It does not provide arbitrary transparent recursive type-constructor equality at higher kind.
• Opaque forward declarations are mainly tied to datatype-style generativity/replication, not general abstract cyclic aliases.
• Russo does not give a full type-soundness proof in the paper.

Safer statement:

Russo’s recursive structures, implemented in Moscow ML, support mutually recursive structures via forward signatures and contractive realizations, including cycles through datatypes and datatype replication. This is a practical and important early design, but it avoids the full CHP problem: it does not provide general higher-kinded transparent equirecursive type equality, and it does not solve double vision for abstract types in the later RTG/RMC sense.

So: do not say “Moscow ML does not support cyclic types.” It does support cyclic type/term dependencies, but in a restricted, datatype-oriented way.

2.4 RTG/RMC

Current draft says:

RMC solves double vision but then rejects all unguarded cycles and mandates that every cycle pass through a datatype; its “undefined” check is sound but order-sensitive and rejects safe generative functor fixpoints.

Fact check:

• “RMC solves double vision” is correct, but be precise: RTG solves the core recursive type-generativity problem; RMC scales the idea to an ML-style recursive module calculus and obtains type soundness by elaboration to RTG.
• RMC uses undefined abstract type variables in the context while typechecking recursive modules.
• RMC explicitly says it follows RTG in requiring all type cycles to go through at least one component defined by a datatype declaration; even after stripping opaque sealings, there must be no transparent type cycles.
• The restriction is conservative. Im et al. 2011 give the clearest citation for the order-sensitivity/functor-fixpoint issue: their Figure 7 Tree/Forest functor-fixpoint example is datatype-guarded, but RMC rejects it because the internal definition of Tree.t depends on Forest.f, which is marked undefined; reversing the order does not help because then Tree.t is undefined at the functor application Set(Tree).

Safer statement:

RMC gives the cleanest module-level solution to double vision by scaling RTG’s destination-passing account of type generativity to modules, but it deliberately avoids adding new equirecursive type equalities to ML. It therefore rejects transparent type cycles and permits cycles only when they pass through datatype-like definitions. This policy is sound and compatible with abstraction, but it is conservative: Im et al. show datatype-guarded functor-fixpoint examples that RMC rejects because the undefined-type check depends on the order in which the recursive components are checked.

2.5 Traviata / OCaml

Current draft says:

Traviata and the OCaml compiler permit cyclic definitions only when an opaque sealing intercepts the cycle. This conflates opacity with contractiveness and works largely because these systems do not solve double vision.

This needs softening.

What is correct:

• Nakata–Garrigue’s examples explicitly contrast Dreyer’s design with Traviata. Traviata accepts examples such as:
  • module M = (struct type t = N.t end : sig type t end) / module N = ... (opaque unguarded cycle)
  • module M = (struct type t = N.t list end : sig type t end) / module N = (struct type t = M.t * M.t end : sig type t end) (guarded cycle behind opacity) while Dreyer rejects both.
• Traviata uses path expansion/type expansion and termination checks; it raises errors for cyclic/dangling references it cannot prove safe.
• OCaml’s behavior is pragmatic and accepts many recursive-module programs when the problematic type equality is hidden behind abstraction; it rejects exposed/transparent cycles.

What is too strong:

• “only when an opaque sealing intercepts the cycle” is too broad: OCaml has recursive types through objects/polymorphic variants, datatypes, and -rectypes; Traviata also has datatype/structural cases and path expansion machinery.
• “works largely because these systems do not solve double vision” is not fair to Traviata. Traviata explicitly discusses double vision and has a source-level mechanism involving path/coercion/type adjustment, though it is not the same as RMC’s RTG-style internal-view refinement.

Better wording:

OCaml and Traviata take a more operational/path-based route. They accept many recursive-module cycles when the problematic equality is hidden behind an opaque boundary, and reject exposed transparent cycles. This makes opacity act as a practical cut in the cycle, even though opacity and semantic contractiveness are conceptually distinct. Traviata further supports signature inference and applicative functors, but its path-resolution/type-expansion machinery is an algorithmic discipline rather than an elaboration into an explicit recursive-type target.

2.6 Im et al. 2011 (“A syntactic type system for recursive modules” / your “Lambda-apps-rec” line)

This paper is important and should be included in this subsection. It is probably the best historical bridge between Traviata/OCaml and our target-calculus story.

Key facts:

• It identifies two challenges for practical recursive modules: double vision and cyclic type definitions.
• It says previous decidable systems solve double vision but fail to typecheck common patterns such as functor fixpoints.
• It gives a declarative type equivalence based on weak bisimilarity, which accommodates a broad range of cyclic type definitions but is not generally practical to implement.
• It then gives an algorithmic syntactic type system using type normalization, rejecting transparent type cycles to keep typechecking practical.
• It explicitly claims to reject only transparent type cycles in the algorithmic system, and to accept all opaque type cycles.
• It shows RMC rejects a datatype-guarded functor-fixpoint Tree/Forest example for order/undefined reasons.
• Important caveat: it does not support OCaml-style applicative functors; it supports generative functors.

Suggested role in our narrative:

Im et al. make the cyclic-type issue explicit: recursive modules can create type equations spanning module boundaries, and a practical system must choose between weak-bisimilarity-level expressiveness and an algorithmic fragment. Our work shares their goal of separating observable transparent cycles from harmless hidden cycles, but we take a target-calculus route: we synthesize explicit \mu-types in \Fomegarec, so contractiveness is checked structurally in the target rather than by a source-level weak-bisimilarity or normalization relation. Moreover, unlike their SML-like/generative setting, our source includes applicative functors, which themselves force static type equations.

2.7 Im et al. 2013 contractive signatures

Current draft says:

Im et al. decouple the issues using weak bisimilarity, but still reject transparent cycles algorithmically in practice.

This conflates Im et al. 2011 and Im et al. 2013.

• 2011: weak bisimilarity + syntactic/algorithmic recursive-module type system.
• 2013: contractive signatures with recursive types, type parameters, and abstract types. The main point is that syntactic contractiveness is difficult in the presence of abstract types and type parameters; they develop semantic contractiveness using mixed induction/coinduction. They show non-contractive types in signatures lead to unsoundness, though non-contractive types may be allowed in modules.

Suggested role:

Im et al. 2013 is the right citation for “opacity/abstractness and contractiveness are conceptually distinct”. It supports our claim that contractiveness should be a semantic/type-theoretic discipline, not merely whether an opaque boundary happens to cut a source-level cycle.

2.8 Fωμ / Cai–Giarrusso–Ostermann

Key facts:

• Fωμ extends System Fω with records, variants, and equirecursive types.
• It proves soundness.
• It shows typechecking for first-order recursive types is decidable with a practical algorithm.
• Type equality is defined by interpreting types as infinitary lambda terms, especially Berarducci trees; the algorithm beta-normalizes types and extends equivalence checking for ordinary equirecursive types.

How to compare:

• Compared with CHP, Fωμ gives a modern, explicit target calculus with a more grounded account of equirecursive type equality, at least in the decidable fragment it studies.
• Compared with Im et al. 2011, it is not a recursive-module system by itself; it is a target language for equirecursive types. Our contribution is using it as the target of module elaboration, so recursive-module cyclic equations are not an implicit source-language equality problem.
• Be careful not to claim “full arbitrary higher-kinded equirecursive equality is solved” unless your own calculus/proofs explicitly cover it. Better claim: “we restrict/synthesize cycles into the target fragment whose well-formedness/equality discipline we rely on.”

Suggested wording:

Cai et al.’s Fωμ provides the target-language ingredient missing from the early CHP story: an explicit equirecursive extension of Fω with soundness and a practical decidability result for first-order recursive types. We use this ingredient not for datatype-generic programming, but as an elaboration target for recursive-module signatures. Thus module-induced cycles become target \mu-types subject to a structural well-formedness/contractiveness check.

3. Recommended new organization for the subsection

I recommend replacing the current three paragraphs with four paragraphs:

1. Historical starting point: CHP and the higher-kinded equirecursive equality problem.
2. Avoidance strategies in recursive-module systems: Russo/Moscow ML, RTG/RMC, OCaml/Traviata.
3. Cyclic type definitions as an explicit problem: Im et al. 2011 and Im et al. 2013.
4. Our target-calculus approach: synthesize \mu-types in \Fomegarec; compare to Fωμ; explain order independence and applicative functors.

This organization makes the line from CHP to Fωμ clear without using “static-on-static” as the headline.

4. Suggested replacement text

This is deliberately a bit longer than a final POPL paragraph. You can compress after the surrounding Related Work stabilizes.

\subsection{Cyclic types and contractiveness}
\label{sec:rw-cycles}
 
\paragraph{From recursive signatures to recursive type equations.}
CHP~\citep{10.1145/301631.301641} already exposed the central difficulty:
transparent recursive module signatures can generate recursive equations among
static components, including higher-kinded type constructors.  Their account
supports such equations using singleton kinds and higher-kinded equirecursive
constructors, but constructor equality in that setting was not known to have a
practical decidable algorithm.  This observation shaped later work: most
recursive-module systems avoid making arbitrary transparent static cycles part of
the source-language equality theory.
 
\paragraph{Avoiding transparent cycles.}
Russo's recursive structures, implemented in \MoscowML, support cyclic
dependencies between structures through forward signatures and contractive
realizations, with datatype definitions and datatype replication providing the
main disciplined way to tie recursive type components~\citep{10.1145/507669.507644}.
RTG and RMC take a different route: they solve the double-vision problem by
forward-declaring abstract type names and later defining them in a
destination-passing style~\citep{dreyer_2007,dreyer_phdthesis}, but deliberately
avoid adding new transparent equirecursive equalities to ML.  RMC therefore
rejects transparent type cycles and permits cycles only when they pass through
datatype-like definitions.  This policy is sound and compatible with abstraction,
but conservative: Im et al. show datatype-guarded functor-fixpoint examples that
RMC rejects because the undefined-type check depends on the order in which the
recursive components are checked~\citep{10.1145/2076021.2048141}.
 
\paragraph{Opacity as a practical cut.}
OCaml and Traviata accept many module-induced cycles when the problematic
equality is hidden behind an opaque boundary, and reject exposed transparent
cycles~\citep{nakata_recursive_nodate,nakata2005type}.  In this sense, opacity
acts as a practical cut in the cycle, even though opacity and contractiveness are
conceptually distinct.  Im et al.'s syntactic type system makes this distinction
explicit: their declarative system uses weak bisimilarity to account for a broad
class of cyclic type definitions, while their algorithmic system remains practical
by rejecting transparent type cycles~\citep{10.1145/2076021.2048141}.  Their
later work on contractive signatures further shows that recursive types,
parameters, and abstract types require a semantic notion of contractiveness, not
just a syntactic occurrence check~\citep{im2013contractive}.
 
\paragraph{Explicit $\mu$-types in \Momega.}
Our elaboration follows the historical lesson of CHP but changes where the
recursive equality lives.  Opaque external signatures do not require a new
source-level equirecursive equality: as in RTG, the secret representation can be
hidden behind an abstract type, giving a functional analogue of type-name
backpatching.  Transparent signatures and applicative functors, however, create
genuine recursive equations among static components.  We make these equations
explicit by synthesizing $\mu$-types in the \Fomegarec target calculus, whose
well-formedness discipline gives the contractiveness check.  Thus guarded cycles
are accepted independently of the order in which the recursive modules are
checked, while unguarded transparent cycles are rejected or collapse according to
the target recursive-type semantics.  Compared with F$\omega_\mu$~\citep{cai2016system},
which studies equirecursive types for datatype-generic programming, our
contribution is to use such a target calculus as the semantic account of
OCaml-style recursive modules with abstraction and applicative functors.

Notes on the last sentence:

• If your system really maps non-contractive exported cycles to \bot, replace “rejected or collapse according to …” with the exact claim and cite your lemma/section.
• If your decidability theorem only covers a base-kind/first-order fragment, say “the target fragment we synthesize” rather than “the target calculus” in the strong sense.

5. How to express the static/dynamic correspondence without naming it too much

Your proposed observation is good, but it should be framed as an interpretation rather than a formal equivalence.

Recommended wording:

There are two different knots to tie. The first is the RTG/RMC knot: an abstract type name is forward-declared and its representation is supplied later. This is a form of type-name backpatching, and our opaque/single-vision elaboration has a functional analogue: the representation is kept secret behind an abstract package while the recursive group is checked. The second knot is a genuine static equation, arising when transparent signatures or applicative functors require the type component itself to be equal to an expression mentioning the recursive group. We do not simulate this second knot by backpatching; we elaborate it to an explicit \mu-type in the target.

This captures the “dynamic-on-static vs static-on-static” intuition without making those terms the main story. If you want a footnote, use:

In CHP's phase-distinction terminology, the first kind of dependency corresponds
roughly to using a forward-declared static component from dynamic specifications,
whereas the second creates recursive equations among static components themselves.
We avoid relying on this terminology in the main text because the later systems
implement the distinction in different ways.

6. Direct answers to the fact-check questions

Does Moscow ML support cyclic types?

Yes, but restricted. Russo/Moscow ML supports cyclic dependencies between types and terms across structures, especially mutually recursive datatypes and datatype replication under forward signatures. It does not support arbitrary transparent higher-kinded equirecursive type equality, and it does not solve double vision in the RTG/RMC sense. So do not write “Moscow ML does not support cyclic types”; write “supports datatype-oriented/contractive cycles but avoids arbitrary transparent cyclic type equations.”

Does RMC support cyclic types?

RMC supports cycles only under a conservative policy compatible with ML’s existing datatype recursion. It rejects transparent type cycles and requires cycles to pass through datatype-like components. It can therefore reject safe-looking guarded cycles, especially functor-fixpoint examples, because its undefined-type check is order-sensitive. So the current claim is basically right but should be softened and tied to Im et al. 2011’s example.

Does Traviata support cyclic types?

Yes. Traviata accepts opaque cycles that Dreyer rejects, including Nakata–Garrigue’s two small examples in your draft. It also has path/type expansion algorithms designed to keep type equality terminating. It is better to say “Traviata accepts many opaque or guarded cycles but rejects/path-errors on exposed problematic cycles” rather than “only opaque sealing intercepts cycles.”

Does Im et al. 2011 support cyclic types?

Yes, and this is exactly why it should be included. Declaratively it handles broad cyclic type definitions with weak bisimilarity; algorithmically it rejects transparent type cycles for practicality. It also solves double vision and accepts important functor-fixpoint examples. Caveat: it is not OCaml-applicative; it supports generative functors only.

Does Im et al. 2013 belong here?

Yes, but not as “the weak-bisimilarity recursive-module paper.” Use it for contractiveness with recursive types, type parameters, and abstract types, and for the claim that opacity/abstractness and contractiveness must be separated semantically.

Does Fωμ belong here?

Yes. It is the target-calculus/historical endpoint after the weak-bisimilarity/source-level line. Use it to explain why our paper can revisit CHP’s equirecursive idea in a more disciplined way. Be careful to state its decidability theorem accurately: practical decidability for first-order recursive types, not arbitrary higher-kinded equality in full generality.

7. Other related work to mention briefly

These do not all need to be in the cyclic-types subsection, but they are useful supporting references.

1. Leroy and Rocquencourt, “A proposal for recursive modules in Objective Caml”.

   • Good for OCaml’s practical module rec design and initialization/runtime-check context.

2. Garrigue and Nakata, “Path resolution for nested recursive modules” (2011).

   • Good if you discuss Traviata path expansion and nested recursive modules. It supports the claim that path resolution/type expansion is subtle and algorithmic.

3. Rossberg and Dreyer, “Mixin’ Up the ML Module System”.

   • Related but complementary: recursive linking/mixins rather than OCaml module rec; uses equirecursive types in the metatheory but not as a surface recursive-module equality story.

4. Montagu and Remy, “Modeling abstract types in modules with open existential types”.

   • Relevant for open existential types and abstract types; Im et al. 2011 compare against it and note limitations around functor fixpoints returning structures.

5. Jaakkola, “A Type System for First-Class Recursive ML Modules”.

   • Related if you include first-class recursive modules / R1ML-like directions; probably not central for the cyclic-types paragraph.

6. Solomon 1978 and Amadio–Cardelli.

   • Mention only if you want the deeper historical line for equirecursive equality. CHP already cites them: Amadio–Cardelli for equality at kind type; Solomon for parameterized type definitions / higher-kind hints.

8. Suggested final narrative in one paragraph

If space is tight, the whole subsection can be compressed to this:

CHP identified the fundamental tension: transparent recursive module signatures can induce recursive equations among type components and higher-kinded type constructors, but equality for higher-kinded equirecursive constructors with singleton/share information was not known to be practical. Later systems avoid this equality problem in different ways. Russo/Moscow ML supports recursive structures through forward signatures and contractive datatype-oriented realizations; RTG/RMC solves double vision by backpatching abstract type names but conservatively rejects transparent type cycles; OCaml and Traviata accept many cycles when opacity cuts the observable equality; Im et al. make the cyclic-type issue explicit using weak bisimilarity and an algorithmic fragment that rejects transparent cycles. Our elaboration follows a different route: opaque cycles are handled by abstract packaging, while transparent/applicative cycles are elaborated to explicit \mu-types in \Fomegarec. Contractiveness is therefore checked structurally in the target, not approximated by source-level ordering or path-expansion heuristics.

This paragraph keeps the historical line, avoids overusing the static/dynamic terminology, and highlights our advantage: target-calculus synthesis of recursive types, order independence, and compatibility with applicative functors.