related-work-factcheck

Related Work fact check and expansion plan

Date: 2026-05-18 Scope: manual.tex, sections/related-work.tex, ocamod.sty, modules.bib, and the Zotero export/PDF folder /Users/ltzhou/Downloads/Recursive Modules. I did not inspect figures/legacy/* and did not modify any TeX source.

0. Executive summary

The current Related Work draft has the right two technical anchors:

1. double vision: RTG/RMC and path-substitution approaches are the most direct comparisons;
2. cyclic types/contractiveness: CHP/Russo/RMC/Traviata/Im et al./Cai et al. are exactly the relevant line.

However, it is currently too compressed and contains several fact-risky claims. The most important corrections are:

• Separate RTG from RMC. RTG is Dreyer’s System-F-style core account of recursive type generativity; RMC is the ML-style recursive module calculus that scales RTG ideas to modules. Your macro \PaperRTG currently points to a key name that does not exist in modules.bib, and the available dreyer_2007 entry is for “Recursive type generativity”, not necessarily the RMC paper “A Type System for Recursive Modules”.
• Do not say Im et al. 2011 supports applicative functors. Their syntactic type system explicitly says it does not support OCaml-style applicative functors and supports only generative functors. This is especially important because the TODO in manual.tex currently says “Add Im et al. 2011 … first order applicative functors”; the paper is more accurately: nested modules, first-order module paths, higher-order functors, weak-bisimulation-inspired type equality, but generative functors only.
• Treat Traviata carefully: it supports applicative functors and signature inference, but path resolution for nested recursive modules is subtle/undecidable in the general setting. Garrigue–Nakata 2011 is the right paper for this nuance.
• Avoid phrasing “Traviata and OCaml work because they do not solve double vision”. Traviata does discuss double vision and uses type coercions/manual adjustment; OCaml has a pragmatic, partial implementation. Better: “they avoid some problematic exposed cycles by relying on opacity/opaque cuts, and their double-vision support is not a full RTG-style internal-view refinement.”
• The “safe initialization” paragraph is too strong. RTG is a core type-generativity calculus, not primarily a recursive-module initialization discipline. RMC has a soundness story via elaboration to RTG, Traviata has call-by-value soundness, and OCaml/Russo/Moscow ML use runtime checks/safe dummy values. Keep initialization as a short orthogonal paragraph.
• The table is useful but dangerous: many entries need footnotes or “partial” labels. In Related Work, prose is safer than a wide feature matrix unless you define every feature precisely.

I recommend restructuring the final Related Work into five subsections:

1. recursive modules in ML: proposals and implementations;
2. double vision and abstraction in recursive modules;
3. cyclic type definitions, contractiveness, and path resolution;
4. applicative/generative/higher-order functors and the F-ing/Momega lineage;
5. orthogonal directions: mixin modules, first-class recursive modules/R1ML, signature avoidance, and initialization safety.

This makes Double Vision and Cyclic Types central, but lets you relate the broader module-system literature without diluting the paper.

1. Fact check of preceding material in manual.tex

1.1 Intro motivation: mostly correct, but polish wording

Relevant lines: manual.tex 176–193, 404–440.

Current claim:

• ML modules balance abstraction boundaries with transparency/sharing.
• Recursive modules introduce unresolved challenges, especially double vision.
• Your work extends Momega with recursive modules, preserving generative/applicative functors, and then adds a top-level double-vision solution.

Fact check:

• Correct at the high level.
• It is good to emphasize that prior recursive-module accounts usually choose only a subset of: abstraction, recursive modules, applicative functors, higher-order functors, signature inference, and practical decidability.
• “OCaml and SML established a hierarchical module system” is fine, but SML does not have recursive modules in the Definition. Phrase as “ML-family languages such as Standard ML and OCaml established hierarchical modules; extensions such as OCaml’s module rec and Moscow ML’s recursive structures add recursion.”

Writing fixes:

• composability and efficiency and requires should be composability and efficiency require.
• tranparency should be transparency.
• doule vision in a comment should be double vision.
• When saying “challenges that have not yet been resolved,” avoid sounding as if no prior work solves them. Better: “have not been resolved simultaneously in an OCaml-like setting with applicative and generative functors.”

Suggested rewrite of the motivation sentence:

Recursive modules make this tension sharper: the type system must expose enough static information inside a recursive group to type-check mutually dependent components, while still preserving abstraction at the boundary of the group.

1.2 Double-vision example: conceptually right, but there are code/text typos

Relevant lines: manual.tex 196–361.

Core fact:

• The example with module rec Simple : SIMPLE = struct type t = int ... end not type-checking in OCaml is a valid illustration of OCaml’s limited treatment of double vision.
• The explanation that the recursive body should identify external Simple.t with the internal concrete t = int is right.
• The Tree/Forest example is also a good motivating example: the call through Forest.head returns an abstract external view of Tree.t, which must be related back to Tree’s internal view in Tree’s body.

Cautions:

• Calling this simply “a deficiency of OCaml” is acceptable in a draft, but in the paper I would phrase more neutrally: “OCaml implements a pragmatic approximation of double vision, which succeeds for some datatype definitions but fails for aliases and other equivalent presentations.”
• The sentence “OCaml does not allow the direct definition of recursive signatures” should be clarified. OCaml has recursive module declarations, including in interfaces, but not a standalone mutually recursive module type facility of the form one would want for TREE/FOREST aliases before the modules exist. Suggested phrasing: “OCaml does not provide standalone recursive module-type definitions that would let TREE and FOREST refer to each other directly; programmers usually express the sharing through with type constraints at the recursive module definition site.”

Concrete typos:

• In the variant workaround example: ket Int y = x should be let Int y = x or better let (Int y) = x in Int (y + 1).
• This just another illustration → This is just another illustration.
• work around in figure caption → workaround.
• A case of deep double vision that we not support → that we do not support.
• In the line “The outer abstract type …, created by the signature ascription” consider “signature ascription of the recursive binding” to distinguish it from the inner body.

1.3 The top-level/deep double-vision limitation: accurate, but should be framed as a design point

Relevant lines: manual.tex 430–475 and sections/related-work.tex 129–138.

Current claim:

• Your system strengthens only top-level components of a recursive group; RTG/RMC handles deeper sealed modules.

Fact check:

• This matches the literature: RMC’s aim is a full formal solution to double vision at the module-calculus level; your approach intentionally restricts the refinement to top-level recursive components.
• The paper should explain why this is acceptable not just “for simplicity”, but because your goal is an OCaml-oriented elaboration into Momega/Fomega-mu with transparent existentials. This makes the restriction a trade-off: simpler elaboration and better compatibility with applicative functors, at the cost of not refining arbitrary nested sealed abstract types.

Suggested framing:

Unlike RMC, our refinement is shallow: it relates the external and internal views of the components bound by the recursive group, but does not recursively inspect every nested sealing in the body. This loses some expressiveness but keeps the transformation local and aligns with the OCaml programming pattern where recursive dependencies are declared at the group boundary.

1.4 Recursive module checking as fixpoint: good, but be careful with “straightforward”

Relevant lines: manual.tex 1017–1034.

Current claim:

• Single-recursive-module case without double vision is enough; mutual recursion is encoded; generalization is straightforward.

Fact check:

• For the single-vision/no-double-vision case, this is plausible.
• For double vision, “straightforward” can be risky because the static pass, strengthening, and contractiveness conditions become mutually dependent. The draft already says it only illustrates two mutually recursive modules; keep “straightforward” only if the general rule is actually defined later.

Suggested phrase:

We present the binary case for readability; the n-ary rule follows the same componentwise construction, with the same contractiveness condition on the vector of synthesized recursive witnesses.

This is stronger and more precise than “straightforward”.

2. Fact check of sections/related-work.tex

2.1 The comparison table: useful but needs footnotes or simplification

Relevant lines: sections/related-work.tex 9–49.

The table is a nice map, but current cells flatten important distinctions. Specific points:

• Moscow ML / Russo:

  • The Russo paper formalizes Mini-SML with recursive structures and is implemented in Moscow ML.
  • It explicitly says a full type-soundness proof is not attempted, though it expects one via Tofte/Elsman-style techniques. So “Formal soundness” blank is okay, but prose should say “formal static/dynamic semantics without a completed type-soundness proof,” not merely “implemented”.
  • The table’s functor cells need care: Moscow ML has higher-order functors; the Russo paper notes examples relying on pattern matching and higher-order/applicative functors not formalized in Mini-SML. If the row is about the formal calculus, leave applicative blank and mark higher-order as implementation-level/partial. If about Moscow ML the implementation, add a footnote.

• Traviata:

  • “Applicative functors” yes.
  • “Higher-order functors” blank is probably okay if you mean full higher-order functor support; Traviata’s central design emphasizes applicative functors and path resolution, and Garrigue–Nakata 2011 shows serious issues even without higher-order functors.
  • “External signature: Inferred” should be “Inferred; optional opaque signatures.” Its abstract says opaque signatures can also be given explicitly.
  • “Double vision: Manual” is too vague. Better: “coercion/manual adjustment” or “partial/manual”.

• RMC:

  • “Generative functors” yes.
  • “Applicative functors” no; Dreyer explicitly says RMC supports generative functors because they are simpler to account for with universal/existential quantification, while OCaml uses applicative functors.
  • “Higher-order functors” in the early CHP/RMC paper is not fully supported; the CHP paper says generalizing to higher-order functors should not be fundamentally difficult but is left to future work. Check whether the RMC paper you cite supports it before putting a checkmark. If in doubt, use “partial / not central” rather than a check.

• lambda^rec_abs / Im et al. 2011:

  • It does not support applicative functors. The PDF explicitly says: “Unlike OCaml, we do not support applicative functors … we support only generative functors as in SML.”
  • It does support higher-order functors according to its examples/claims, but the path language excludes functor application paths.
  • It solves double vision with a syntactic/source-level system and weak-bisimulation-inspired type equivalence.

• Momega:

  • “Double vision: Top-Level” is fair for your system, but call it “shallow/top-level” and explain in prose.
  • “Cyclic types: checkmark” should be qualified: your target supports equirecursive types, but your algorithmic checker currently restricts cyclic signatures to base kind for decidability (as you say later). So table cell should be “base-kind / contractive μ”.

• OCaml:

  • “Double vision: Fragile” is accurate informally; in paper prose say “partial/pragmatic”.
  • “Cyclic types: checkmark” should be qualified. OCaml has recursive modules and structural recursive types (objects/polymorphic variants), but not arbitrary higher-kinded equirecursive types. For module-recursive aliases, acceptance depends on opacity, path resolution, and implementation checks.

Recommendation: either replace the table with a prose “feature map”, or keep it with footnotes and cells like “partial”, “implementation”, “formal core”, “no”. Otherwise reviewers may attack one ambiguous checkmark.

2.2 Recursive modules and formal foundations section

Relevant lines: sections/related-work.tex 51–115.

Mostly correct:

• CHP/Dreyer et al. are a foundational starting point and identify double-vision/trouble-with-opacity style issues.
• Russo/Moscow ML is an early practical extension.
• Traviata supports signature inference and applicative functors.
• RMC and Im et al. are generative/SML-like rather than OCaml-applicative.
• F-ing/Momega lineage is the right frame for your elaboration target.

Corrections:

1. “The first foundational account of recursive modules is due to CHP” — OK, but the citation key 10.1145/301631.301641 is not in modules.bib. Add it from the RDF/PDF list. The local PDF title is “Toward a Practical Type Theory for Recursive Modules”.

2. “CHP advocated fully transparent external signatures as the remedy” — This needs nuance. CHP discuss severe restrictions/forward declaration signatures and the interaction of data abstraction and recursion; “fully transparent” may describe one workaround, but do not imply their whole proposal is simply transparent signatures. Better: “early accounts often avoided the hardest opacity interactions by restricting how abstraction may appear in recursive definitions.”

3. “MoscowML … requiring forward-declared signatures whose type components are either transparent or implemented by datatype definitions.” This is close but should be grounded in Russo’s wording: forward signatures are enriched by the body under a contractive realization; datatype replication can identify body datatypes with opaque forward declarations. I would rewrite:

Russo’s recursive structures, implemented in Moscow ML, require a forward signature and check that the body enriches it under a contractive realization of the forward type components; in practice, opaque forward declarations are tied to datatype definitions/replication.

4. “To our knowledge, Momega is the first formalization that simultaneously supports generative, applicative, and higher-order functors inside module rec while aiming to model OCaml.” This is the main novelty claim and seems plausible from the PDFs, but be precise:

… the first elaboration-based formalization of OCaml-style recursive modules that combines shallow double vision with both generative and applicative higher-order functors.

This avoids overclaiming against systems like OCaml itself (implementation), 1ML/R1ML (different goals), and MixML (different module abstraction model).

5. “RMC solves double vision … using primitives provided by RTG” — correct in spirit. Add “RMC’s type soundness is obtained by elaboration to RTG.”

6. “MoscowML’s recursive modules … lack a formal soundness proof” — correct, and you can cite Russo’s own statement that he does not attempt the proof.

2.3 Double vision section

Relevant lines: sections/related-work.tex 118–148.

Mostly correct:

• Dreyer/RMC gives the first full formal module-level solution.
• Your approach adapts the two-pass/static-refinement idea but implements it in an Momega elaboration setting.
• Im et al. 2011 and path-substitution work are relevant.
• Traviata’s handling is less automatic/metatheoretically central than RMC/Im.

Corrections and improvements:

1. “The first full formal solution” should be tied to RMC, not just RTG. RTG solves the core type-generativity problem; RMC scales it to recursive modules.

2. “strengthening by type substitution in the elaborated term” — good, but maybe explain the conceptual difference:

• RMC: creates/forward-declares abstract type names and later defines them in a destination-passing style.
• Momega: computes internal-view witnesses and repackages/compacks transparent existentials; no imperative type cells in the target calculus.

3. Deep double vision paragraph is good. Avoid saying programmers “seldom intend” without evidence. Better:

In the OCaml idioms we target, recursive dependencies are normally expressed at the recursive-group boundary; nested sealings can be refactored outward when double vision is required.

4. Im et al. 2011 should be represented as more than “path substitution”. Their main contribution is a syntactic type system that solves double vision while rejecting only transparent cycles for practical decidability, with a weak-bisimulation-based declarative account. Path substitution/path resolution is more specifically Garrigue–Nakata 2011 and their earlier system.

2.4 Cyclic types and contractiveness section

Relevant lines: sections/related-work.tex 154–210.

This is the highest-risk part. The direction is right, but several claims need softer phrasing.

2.4.1 “Avoiding equi-recursive types” paragraph

Current:

CHP proposed transparent external signatures with higher-kinded equi-recursive constructors, but decidability at higher kinds is not known.

Safer:

CHP-style phase-splitting exposes the danger that recursive module signatures can induce static-on-static cycles. Supporting such cycles transparently would amount to higher-kinded equirecursive type constructors, for which practical/decidable equivalence is not available in the generality needed by ML modules.

Current:

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

Nuance:

• Dreyer thesis describes the dynamic-on-static restriction in early foundational accounts.
• RMC/RTG instead provides a different generativity account and conservative restrictions to avoid transparent cycles.
• Russo uses contractive realizations.

Suggested rewrite:

A common way to avoid this problem is to forbid or conservatively restrict static-on-static cycles, allowing only dynamic components to depend on forward-declared static components. Russo phrases the check in terms of contractive realizations; RMC rejects definitions that would create transparent type cycles.

2.4.2 “RMC rejects all unguarded cycles and mandates every cycle pass through a datatype”

Likely directionally right, but too absolute. In RMC/Dreyer, the relevant restriction is that internal definitions of abstract types in a sealed module cannot depend on undefined abstract variables except those known to be datatypes. Better:

RMC’s static checking prevents transparent type cycles by allowing dependencies through datatype-like components but rejecting problematic abbreviations/aliases that would define abstract types in terms of still-undefined abstract names.

This is more defensible.

2.4.3 “undefined check is order-sensitive”

This may be true in a specific exercise/example, but reviewers will want exact citation. If you keep it, explain in a footnote or avoid it. Suggested:

Its conservative undefined/type-cycle check can reject programs accepted by systems that treat guarded or opaque cycles more liberally.

2.4.4 “Traviata and OCaml permit cyclic definitions only when opaque sealing intercepts the cycle”

This is plausible for the examples, but too broad. Traviata also supports structural recursive types and weak bisimulation in the declarative account; OCaml has objects/polymorphic variants and practical path expansion. Safer:

Traviata and OCaml accept many module-induced 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, although opacity and semantic contractiveness are conceptually distinct.

2.4.5 Im et al. 2013

Current:

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

Fact check:

• Im et al. 2013 “Contractive Signatures…” focuses on interaction of recursive types, type parameters, and abstract types; key idea is semantic contractiveness for recursive types with abstract types.
• They discuss iso- vs equi-recursive types, syntactic contractiveness, non-regular recursive types, and practical type equivalence.

Suggested:

Im et al. 2013 study contractiveness in signatures with recursive types, type parameters, and abstract types, making explicit that opacity/abstractness and contractiveness are separate concerns. Their account is useful background for our decision to express recursive module cycles as explicit μ-types and discharge contractiveness structurally in the target.

2.4.6 “non-contractive exported cycle degenerates to bottom”

This is a strong technical claim about your system. Keep only if proven earlier. Otherwise mark as “in our target encoding, non-contractive cycles are rejected/approximated according to the well-formedness condition.” If the system really maps them to ⊥, point to the exact section/lemma.

2.4.7 Example classifications

The three examples at lines 193–205 are useful. Fact-check risk:

• The third example “datatype-guarded and contractive in Fomega-mu” uses list and *; if your target treats list/products as type constructors that guard recursion, yes.
• “RTG still rejects” should be “RMC/RTG-style system rejects under its conservative cycle policy” unless you specifically cite RTG’s undefined check. RTG as a core calculus is not exactly a source recursive-module checker.

2.5 Safe initialization paragraph

Relevant lines: sections/related-work.tex 217–221.

Current:

Initialization safety is not a focus … inherit it from target fixpoint and OCaml runtime module-creation check. RTG and Traviata provide static guarantees; OCaml and MoscowML rely on runtime checks.

Problems:

• RTG is about type generativity and has type soundness, not necessarily source-level safe module initialization.
• RMC elaborates to RTG, but term initialization of recursive modules is not the same topic as type-name generation.
• OCaml and Moscow ML indeed rely on runtime checks/safe dummy values for unsafe recursive module access.

Suggested rewrite:

We do not study the separate problem of initialization safety for recursive values. OCaml’s module rec and Russo’s recursive structures use runtime checks/dummy values to prevent unsafe early access. Other work studies static well-foundedness conditions for recursive modules. Our focus is instead static type identity: when recursive references are safe to type-check, which type equalities should be available inside the recursive group.

If you want citations here, include Leroy’s OCaml proposal, Russo 2001, and possibly Boudol/Hirschowitz–Leroy if you add those entries.

2.6 R1ML and MixML stubs

Relevant lines: sections/related-work.tex 224–231.

R1ML:

• The statement is plausible but too vague. Jaakkola’s thesis is about first-class recursive ML modules and discusses double vision/recursive linking. If you cite it, say why it is not the same problem: first-class recursive modules and recursive linking, Haskell/GHC-style elaboration/local axioms, not an OCaml module rec formalization into Momega.

MixML:

• You should not leave an empty paragraph in the final paper. Either remove it or add 3–5 sentences.
• MixML is related because it supports recursive linking of separately compiled components and hierarchical composability with type abstraction. It is less direct because it changes the module model to mixin units and, in the paper, does not model OCaml applicative functors.

Suggested text:

MixML synthesizes ML modules and mixin modules, providing recursive linking of separately compiled components while retaining hierarchical structure and type abstraction. It is complementary to our work: MixML changes the source module abstraction to support recursive linking as a first-class composition mechanism, whereas we keep OCaml-style module rec and study the static type equalities needed for recursive groups. MixML’s unit instantiation is closer to generative functor application and the paper leaves OCaml-style applicative behavior to future work.

3. Bibliography/key problems

modules.bib is incomplete for this Related Work. It appears to be from the earlier Momega project, as you said. The Related Work currently cites several keys that are missing.

Missing or suspicious keys I found:

• 10.1145/301631.301641 — likely CHP / “Toward a Practical Type Theory for Recursive Modules”. Add exact BibTeX from RDF/ACM.
• 10.1145/507669.507644 — Russo, “Recursive structures for Standard ML”. Add exact BibTeX.
• 10.1145/2076021.2048141 — Im et al. 2011, “A Syntactic Type System for Recursive Modules”. Add exact BibTeX.
• im2013contractive — Im, Nakata, Park, “Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types”. Add exact BibTeX.
• nakata2005type — likely “Type inference for recursive modules” or related. Check RDF and add exact entry.
• jaakkola2020type — Jaakkola thesis. Add exact entry if kept.
• \PaperRTG expands to Dreyer/RTG@icfp2007, but modules.bib only has dreyer_2007 for “Recursive type generativity”. Either change the macro or add the intended RMC entry.
• \PaperMomega, \PaperZipml, \PaperFing macro keys do not appear literally in modules.bib; there are related but differently named entries. This may be intentional if the current bib is stale, but it will not compile as-is.

Recommendation: create a new project-specific recursive-modules.bib or update modules.bib from Recursive Modules.rdf, then normalize keys. Do this before finalizing Related Work text, because the distinction between RTG/RMC/CHP/Im2011 depends on exact citations.

4. Additional related work to include and how to organize it

4.1 Recursive modules: proposals and implementations

Works to include:

• Crary/Harper/Puri / Dreyer et al., “Toward a Practical Type Theory for Recursive Modules” (CHP).
• Russo, “Recursive Structures for Standard ML” / Moscow ML.
• Leroy and Rocquencourt, “A proposal for recursive modules in Objective Caml”.
• Nakata and Garrigue, “Recursive Modules for Programming” / Traviata.
• Dreyer, “Recursive Type Generativity” and “A Type System for Recursive Modules” / RTG and RMC.
• Im et al. 2011, “A Syntactic Type System for Recursive Modules”.

What to say:

• These works introduce recursive modules as a way to avoid merging conceptually separate components.
• The design space has several axes: required vs inferred signatures; generative vs applicative functors; shallow vs deep/nested modules; source-level vs elaboration-based semantics; static vs runtime initialization; treatment of cycles.
• Your paper’s position: OCaml-oriented, elaboration-based, preserves Momega’s applicative/generative higher-order functor story, and gives a shallow double-vision transformation.

Possible paragraph skeleton:

Recursive modules have been studied both as practical language extensions and as type-theoretic calculi. CHP and Russo introduced early accounts based on forward declarations; OCaml adopted a pragmatic module rec design with explicit signatures and runtime checks. Traviata explored the opposite usability trade-off by inferring recursive signatures and supporting applicative functors. RMC and Im et al. give more systematic treatments of double vision in SML-like/generative settings. Our work differs by keeping the OCaml/Momega account of applicative and generative functors and explaining recursive modules by elaboration into an Fomega-mu target.

4.2 Double vision and abstraction

Works to include:

• CHP / “trouble with opacity” or early double-vision examples.
• Dreyer thesis, RTG, RMC.
• Garrigue–Nakata / Traviata’s type coercions and path resolution.
• Im et al. 2011 syntactic type system.
• OCaml behavior as motivating implementation.

Main comparison axes:

• Full deep refinement vs shallow/top-level refinement.
• Destination-passing/backpatching abstract type names vs source-level path substitution vs elaborated witness substitution/compack.
• Generative-only vs OCaml-style applicative paths.

Suggested message:

Our double-vision solution follows RMC in spirit—first compute the internal type information, then check the body under a refined view—but differs operationally: it is expressed as an elaboration/transformation using Momega transparent existentials, rather than extending the core with imperative type-name cells or relying on a source-level path-substitution judgment.

4.3 Cyclic types, contractiveness, and path resolution

Works to include:

• CHP and Dreyer thesis on dynamic-on-static/static-on-static cycles.
• Russo’s contractive realizations.
• RMC/RTG’s conservative prevention of transparent cycles.
• Traviata and OCaml’s opacity/path-expansion treatment.
• Garrigue–Nakata 2011 “Path resolution for nested recursive modules” for undecidability/termination of path resolution.
• Im et al. 2013 for contractive signatures with recursive/abstract types.
• Cai–Giarrusso–Ostermann 2016 for System F-omega with equirecursive types.

Important distinction to emphasize:

• “Cyclic types from recursive modules” are not just ordinary iso-recursive datatypes.
• The hard case is exposed transparent equality between higher-kinded constructors or path-dependent module components.
• Opaque sealing can cut a cycle operationally, but semantic contractiveness is a separate concept.
• Your elaboration makes the implicit cycles explicit as target μ-types and then delegates well-formedness/contractiveness to Fomega-mu.

Suggested message:

Earlier systems often avoid higher-kinded equirecursion by rejecting static-on-static cycles or by letting opacity hide them. We instead make the cycle explicit in the target type and check contractiveness there. This does not solve general higher-kinded equirecursive equivalence, but it clarifies which source cycles are accepted and why.

4.4 Applicative/generative functors and F-ing/Momega foundations

Works to include:

• Leroy 1995, applicative functors and fully transparent higher-order modules.
• F-ing modules (Rossberg, Russo, Dreyer 2014).
• Momega / “Fulfilling OCaml Modules with Transparency”.
• ZipML / signature avoidance with zippers, if relevant to transparent existentials/signature avoidance.
• 1ML if you want a broader unification-of-core-and-modules comparison.

Main point:

• This is where your work differs from RMC and Im2011. They are generative/SML-like; your baseline is Momega, so applicative paths and transparent existentials are first-class concerns.
• Do not overdo this section; it should justify the target calculus and functor story, not become a general history of modules.

Suggested message:

The F-ing line shows that much of ML modules can be understood as an elaboration into System Fomega. Momega extends this line with transparent existentials for OCaml-style applicative functors. Our contribution is to show that recursive modules and shallow double vision can be added without abandoning this elaboration discipline, provided the target is extended with suitable recursive types and repackaging operations.

4.5 Mixins, units, recursive linking, and first-class recursive modules

Works to mention briefly:

• MixML (Dreyer and Rossberg).
• Units / recursive linking literature if already in RDF or if space allows.
• R1ML / Jaakkola thesis.
• Possibly first-class modules / Montagu only if you discuss first-class recursive modules; otherwise omit.

What to say:

• These systems address module-level recursion and linking in broader ways, often making recursive linking a composition mechanism rather than focusing on OCaml’s module rec.
• They are orthogonal to your main concern: static equalities between internal and external views of abstract types in recursive groups.

Suggested compact paragraph:

Mixin modules and recursive linking systems attack a related modularity problem—assembling separately developed components with cyclic dependencies. MixML, for example, combines ML-style hierarchy and type abstraction with mixin-style recursive linking, but its unit model and generative instantiation differ from OCaml’s module rec and applicative functor paths. R1ML and related first-class recursive module systems likewise explore a different point in the design space, emphasizing first-class packaging and linking rather than an elaboration of OCaml recursive modules into Momega.

4.6 Initialization safety

Keep it short and orthogonal.

Works:

• OCaml proposal/reference manual.
• Russo/Moscow ML.
• Traviata’s call-by-value soundness.
• Static well-foundedness works if you decide to include Boudol/Hirschowitz–Leroy.

Message:

Initialization safety concerns whether recursive value components are evaluated before being available. It is orthogonal to double vision, which concerns static type equalities. We focus on the latter and rely on the target fixpoint/runtime discipline for the former.

5. Proposed final structure for the Related Work section

I would avoid the current table-first structure unless you are ready to defend every cell. A prose-first section is safer:

5.1 Recursive modules in ML

One paragraph on CHP/Russo/OCaml/Traviata/RMC/Im2011.

Purpose: establish design space.

5.2 Double vision

Two paragraphs:

1. CHP/RMC/RTG/Im2011/Traviata/OCaml.
2. Your shallow solution vs RMC deep solution; applicative/generative distinction.

Purpose: direct comparison to your first main line.

5.3 Cycles, contractiveness, and path resolution

Two paragraphs:

1. static-on-static cycles, dynamic-on-static restrictions, opaque cuts, weak bisimulation/path resolution.
2. Fomega-mu/Cai and your explicit μ-type elaboration; limitation at higher kinds/algorithmic decidability.

Purpose: direct comparison to your second main line.

5.4 Functor semantics and elaboration foundations

One paragraph on Leroy applicative functors, F-ing, Momega, ZipML.

Purpose: explain why supporting applicative + generative + higher-order functors in recursive modules is new/important.

5.5 Orthogonal module-recursion mechanisms

One short paragraph on MixML/R1ML/recursive linking/initialization.

Purpose: show broad awareness without overcommitting.

6. Concrete replacement outline for the current text

You can rewrite the current Related Work roughly as follows:

1. Open with a map:

Recursive modules sit at the intersection of three issues: abstraction in recursive groups, recursive type equalities induced by module paths, and functor semantics. Prior work typically solves two of these at the cost of restricting the third.

2. Recursive modules paragraph:

CHP and Russo/Moscow ML introduce forward declarations; OCaml implements explicit module rec; Traviata infers signatures and supports applicative functors; RMC and Im2011 give formal double-vision solutions in generative settings.

3. Double vision paragraph:

RMC is the closest ancestor. We follow the internal/external view refinement idea, but use Momega transparent existentials and explicit witness substitution rather than RTG primitives. Our solution is shallow; RMC is deeper.

4. Cyclic types paragraph:

Recursive modules can generate type cycles. Higher-kinded transparent cycles are problematic. Prior work avoids them via dynamic-on-static restrictions, contractive realizations, opacity cuts, or weak bisimilarity/path resolution. We make the cycles explicit as μ-types in Fomega-mu and check contractiveness there.

5. Functor/elaboration paragraph:

F-ing and Momega provide the elaboration foundation for higher-order/applicative/generative modules; previous recursive-module accounts do not simultaneously preserve these OCaml features.

6. Orthogonal work paragraph:

MixML/R1ML/recursive linking/initialization safety address related but different dimensions.

7. High-confidence citations from the PDF folder

These are definitely relevant and should be in the final bibliography if cited:

• Dreyer et al., “Toward a Practical Type Theory for Recursive Modules” — early double vision/trouble with opacity and repetitive stress.
• Russo, “Recursive Structures for Standard ML” — Moscow ML, forward declarations, runtime checks, contractive realization.
• Leroy and Rocquencourt, “A proposal for recursive modules in Objective Caml” — OCaml design, explicit signatures, safe modules/runtime Undefined_recursive_module, Okasaki bootstrapped heaps example.
• Nakata and Garrigue, “Recursive Modules for Programming” — Traviata, signature inference, opaque signatures, applicative functors, expression problem, type coercions.
• Garrigue and Nakata, “Path resolution for nested recursive modules” — path resolution, undecidability even without higher-order functors, decidable restrictions.
• Dreyer, “Recursive Type Generativity” — RTG, destination-passing/backpatching type generativity, core soundness.
• Dreyer, “A Type System for Recursive Modules” — RMC, module-level scaling of RTG, double vision solution, generative functors.
• Im et al., “A Syntactic Type System for Recursive Modules” — syntactic/source-level double vision, weak bisimulation, generative-only, no applicative functors.
• Im, Nakata, Park, “Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types” — contractiveness with abstract types.
• Cai, Giarrusso, Ostermann, “System F-omega with Equirecursive Types for Datatype-Generic Programming” — target calculus background for Fomega-mu/equirecursive types.
• Rossberg, Russo, Dreyer, “F-ing Modules” — elaboration of ML modules to Fomega; excludes recursive modules.
• Blaudeau/Rémy/Radanne, “Fulfilling OCaml Modules with Transparency” — Momega/transparent existentials baseline.
• Blaudeau et al., “Avoiding Signature Avoidance in ML Modules with Zippers” — if you discuss signature avoidance/ZipML.
• Dreyer and Rossberg, “Mixin’ Up the ML Module System” — recursive linking/mixins, orthogonal.
• Jaakkola, “A Type System for First-Class Recursive ML Modules” — optional orthogonal comparison.

8. Bottom-line recommendation

Do not expand Related Work by just adding a long list of systems. Make the structure argumentative:

• “Double vision” explains why recursive modules need internal/external type views.
• “Cyclic types” explains why those views can induce hard recursive equality problems.
• “Functor semantics” explains why your setting is harder than RMC/Im2011: OCaml applicative functors and Momega transparent existentials must be preserved.
• “Elaboration” explains why the result is conceptually clean: recursive modules are not a bespoke module calculus but compile into Fomega-mu.

This framing makes the current two main lines look like the center of the design space rather than an incomplete Related Work section.