related-work-other-future-directions

Related Work: Other aspects and future directions 写作建议

本文档只给写作建议和可粘贴草稿，没有修改 sections/related-work.tex 或其他 LaTeX 源文件。

0. Bottom line

我建议把 \subsection{Other aspects and future directions} 写成 4—5 个 topic paragraphs，而不是继续沿着 “R1ML / MixML / Iso-recursive types” 三个空标题罗列。更好的组织是：

1. \paragraph{A practical source system.} 讨论 ZipML。把它接在 Double vision 小节末尾也可以，但更自然的是放在 Other aspects 第一段：Mω/F-ing 风格给了 semantic/internal representation；ZipML 是面向 OCaml typechecker 的 path-based/source-level 系统。我们的工作未来可以把 recursive modules 的 double vision / cyclic type elaboration 接到 ZipML 上，从而给当前 source-to-source encoding 和 practical retrofitting 一个更好的形式化落点。

2. \paragraph{Recursive linking and mixin composition.} 讨论 MixML 和 Clément thesis Chapter 6 对 composition design space 的分类：recursive modules 是 immediate recursive composition；mixin modules 是 delayed recursive composition / recursive linking，更适合 separate compilation。我们的工作仍然是 OCaml module rec 式的同组递归，不解决跨 compilation unit 的 recursive linking，也不试图用 mixins 取代 functors。

3. \paragraph{First-class recursive modules.} 讨论 R1ML。它不是 “Haskell-style recursion” 这么简单，而是 1ML 风格的 first-class modules + recursive modules，elaborates to System Fc/local coercion axioms to address double vision。它与我们 orthogonal：它统一 core/modules 并做 first-class recursive modules；我们形式化 OCaml-like second-class modules with applicative/generative functors and recursive module signatures。R1ML 自己也把 recursive linking 留作 future work。

4. \paragraph{Initialization safety.} 保留，但建议改得更谨慎。当前写法 “we inherit it from target fixpoint and OCaml runtime module-creation check” 容易混淆 formal type soundness 和 OCaml runtime initialization failure。更安全：本文关注 static typing/type abstraction/cyclic type equations；well-founded initialization 是 orthogonal。OCaml uses a static approximation plus runtime checks; RMC/Traviata study static well-foundedness; Mω target fixpoints give type safety but do not by themselves solve source-level initialization checking.

5. \paragraph{Iso-recursive datatypes and higher-kinded cycles.} 可以作为最后的 future direction，承接 cyclic types 小节：我们的 target calculus sound at arbitrary kinds，但 algorithm 目前 restricted；未来可以通过 source-level iso-recursive datatype/constructor discipline 把某些 higher-kinded cycles 隐藏在 fold/unfold 或 abstract boundaries 后面，避免把所有递归都暴露为 transparent higher-kinded equi-recursive equality。

如果篇幅非常紧，建议保留 1/2/4/5，把 R1ML 压缩到 recursive linking paragraph 或 footnote；但如果 Related Work 需要显得覆盖全面，R1ML 值得单独一段。

1. Evidence notes from the PDFs

Mω / Fulfilling OCaml Modules with Transparency

Checked source: Recursive Modules/files/2131/Clement 等 - 2024 - Fulfilling OCaml Modules with Transparency.pdf and Clément Blaudeau thesis Recursive Modules/files/2335/...Retrofitting...pdf.

Useful factual points:

• Mω covers a large subset of OCaml modules, including both applicative and generative functors, plus transparent ascription.
• It follows the F-ing lineage: modules are specified/elaborated through Fω-style core types/terms.
• It introduces transparent existential types to simplify sealing inside applicative functors.
• It includes a source-to-source encoding of aliasing/identity tags, so OCaml-style module identity can be represented using type abstraction.
• It provides an anchoring/reverse translation from Mω signatures back to path-based source signatures, but signature avoidance remains a central issue.
• In “omitted features / future work”, recursive modules are explicitly not covered: recursive modules raise double vision; a similar solution should apply after adding recursion at term and type levels; a more ambitious solution would be mixin modules; compilation/initialization remains separate.

Recommended role in our paper:

• Cite Mω/Fulfilling not only in the main comparison but also in Other aspects: our work is naturally “Mω + recursive modules + explicit μ-types”.
• Do not present Mω as competing recursive-module work; it is the immediate non-recursive predecessor whose future-work item we address.

ZipML

Checked source: Recursive Modules/files/1999/Blaudeau et al. - 2025 - Avoiding Signature Avoidance in ML Modules with Zippers.pdf.

Useful factual points:

• ZipML is a source/path-based type system for ML modules using zipper signatures / floating fields to delay and resolve signature avoidance.
• It is designed as a practical improvement that could be retrofitted into OCaml.
• Its soundness is by elaboration into Mω, not directly into Fω.
• Its conclusion says recursive modules raise double vision; OCaml requires full annotations and runtime-initialization semantics; these solutions are compatible with ZipML and left to future work.
• Implementation and mechanization are explicitly future work.

Recommended role in our paper:

• Put ZipML in Other aspects as a practical future direction, not in the main recursive-module feature table unless the table gets a row for “source/typechecker representation”.
• Strong point for the user’s suggested sentence: ZipML can provide a formal source-level account for the source-to-source encoding/identity-tag idea and a practical route to OCaml retrofitting.

Clément thesis Chapter 6: composition design space

Checked source: Retrofitting and strengthening the ML module system, Chapter 6 and conclusion.

Useful factual points:

• The thesis distinguishes immediate vs delayed composition, sequential vs recursive composition, and hierarchical vs flat composition.
• OCaml recursive modules are immediate recursive composition: useful when mutual dependencies cross module boundaries but require explicit signatures and must address double vision / type cycles / initialization.
• MixML/mixin modules are delayed recursive composition: they are motivated by recursive linking and separate compilation.
• Thesis conclusion: Mω and ZipML leave recursive composition and modular implicits out; recursive composition is a key difficult feature; future research is needed to understand interaction with applicative functors, especially sealing inside applicative functors.

Recommended role:

• Use this as the organizing bridge. It justifies a paragraph that says our work addresses one branch of recursive composition (OCaml module rec) but not recursive linking/separate compilation/mixins.

MixML

Checked source: Recursive Modules/files/3090/Dreyer and Rossberg - Mixin’ Up the ML Module System.pdf.

Useful factual points:

• MixML combines ML-style type abstraction/translucent signatures with mixin-style recursive linking.
• It is motivated by separate compilation: existing recursive-module proposals address type-system issues but not general separate compilation of mutually recursive components.
• It treats many ML module constructs through mixin composition/linking.

Recommended role:

• Compare on composition/linking, not on double vision/cyclic type details. Say MixML is broader in recursive linking/separate compilation; our work is closer to OCaml module rec and focuses on double vision plus cyclic type equations in an elaboration semantics.

R1ML

Checked source: Recursive Modules/files/3354/Jaakkola - A TYPE SYSTEM FOR FIRST-CLASS RECURSIVE ML MODULES.pdf.

Useful factual points:

• R1ML develops recursive first-class modules in the style of 1ML.
• It targets a System Fc variant with type equality coercions/local axioms to avoid double vision.
• It proves soundness and decidability but is incomplete in tolerated ways.
• It explicitly says there was no time/space to consider recursive linking.
• Its future-work chapter distinguishes well-founded recursion and recursive linking; dynamic initialization checks as in OCaml recover soundness but are unsatisfactory from a static-analysis/effect-tracking perspective.

Recommended correction:

• Replace “pursues Haskell-style recursion” with “uses GHC’s System Fc/coercion-equality machinery as an elaboration target for 1ML-style first-class recursive modules”. Haskell/GHC is the target-calculus inspiration, not the main source-language motivation.

2. Fact-check comments on the current draft lines 232—257

Current text:

\paragraph{Safe initialization.}
Initialization safety is not a focus of this work: we inherit it from the
target fixpoint and from \OCaml's runtime module-creation check.
\RTG and \Traviata provide static guarantees; \OCaml and \MoscowML rely on
runtime checks.

Suggested correction:

• “inherit it from the target fixpoint” is too strong. A target fixpoint can preserve type safety of the elaborated calculus, but source-level safe initialization is a separate property: it rules out premature forcing/access to uninitialized recursive components.
• “OCaml runtime module-creation check” is fine as an operational fact, but pair it with “static approximation + runtime check” if you want to be precise.
• Keep the paragraph, but call it orthogonal rather than inherited.

Current text:

\paragraph{R1ML}
\RoneML~\cite{jaakkola2020type} is another approach to recursive modules,
elaborating to GHC's System~$F_c$ with local axioms for double vision; it
pursues Haskell-style recursion rather than a formalization of \OCaml modules,
and we leave a detailed comparison for future work.

Suggested correction:

• The first half is directionally correct.
• “Haskell-style recursion” is misleading. R1ML is about 1ML-style first-class recursive ML modules; System Fc is the elaboration target because coercion axioms can express type equalities.
• Better contrast: first-class/core-module unification vs OCaml-like second-class module system; R1ML omits recursive linking; our work handles applicative/generative functors and source recursive signatures.

Current text:

\paragraph{MixML}

Suggested content:

• Use MixML to discuss recursive linking/separate compilation, not just as another recursive-module calculus.
• It also gives a natural place to mention Clément thesis’s “immediate vs delayed recursive composition” taxonomy.

Current text:

\paragraph{Iso-recursive types.}
Separately, although \Fomegarec is sound at arbitrary kinds, our algorithmic
checker currently restricts cyclic signatures to base kind for decidability.
...

Suggested correction:

• Good topic and good final future direction.
• Avoid sounding as if iso-recursive treatment “subsumes” equi-recursive transparent cycles generally. Safer: it may recover some programming patterns by making fold/unfold explicit or hiding recursion behind abstract boundaries, but it is a different source-level discipline.

3. Recommended organization with paragraph intent

Paragraph 1: Practical source system / ZipML

Purpose:

• Transition from semantic elaboration to practical source/typechecker representation.
• Connect the user’s point: ZipML as future work, especially for formalizing the source-to-source encoding.

Key contrast:

• Mω/Fωμ: semantic/internal elaboration target.
• ZipML: path-based source-level system designed for OCaml retrofitting; could make the source-to-source encoding and zipper-based avoidance story precise for recursive modules.

Paragraph 2: Recursive linking / MixML

Purpose:

• Cover “more related work” beyond double vision/cyclic types.
• Explain why MixML is not just missing from the table; it addresses a different axis.

Key contrast:

• Our module rec: immediate recursive composition within an explicit group.
• MixML: delayed recursive composition / recursive linking / separate compilation.

Paragraph 3: First-class recursive modules / R1ML

Purpose:

• Cover Jaakkola without derailing the OCaml narrative.
• Good paragraph if you want more breadth.

Key contrast:

• R1ML: first-class recursive modules; System Fc local axioms; recursive linking not covered.
• Our work: OCaml-like module layer, applicative/generative functors, recursive signatures and μ-types.

Paragraph 4: Initialization safety

Purpose:

• Acknowledge runtime/well-foundedness issue as out of scope.
• Prevent reviewers from thinking target μ-types solve initialization.

Key contrast:

• Static typing / double vision / cyclic type equations vs dynamic initialization.

Paragraph 5: Iso-recursive datatypes / higher-kinded cycles

Purpose:

• End with a genuine technical future direction from your work.
• Links back to cyclic-type subsection and algorithmic limitation.

Key contrast:

• Transparent equi-recursive equality at higher kinds is hard.
• Iso-recursive source disciplines might recover useful programs while preserving decidable equivalence.

4. Pasteable draft LaTeX

Below is a moderately long version. It is intended to replace the current subsection body, but I am not applying it automatically.

\subsection{Other aspects and future directions}
\label{sec:rw-other}
 
\paragraph{Toward a practical source type system.}
Our presentation follows the \Fing tradition of giving modules a semantics by
elaboration into a small typed core calculus, and is closest to \Momega, which
models a large OCaml-like module fragment with applicative and generative
functors, transparent ascription, and transparent existential types
\cite{\PaperMomega,\PaperFing}.  The same line of work also proposes a
source-to-source encoding of module identities by explicit identity tags, and an
anchoring translation from \Momega signatures back to path-based source
signatures.  A complementary direction is \ZipML
\cite{\PaperZipml}, a path-based source type system with zipper signatures and
floating fields, designed to avoid signature avoidance while remaining close to
OCaml's implementation.  Recursive modules are explicitly left as future work in
\ZipML: they raise double vision, require full recursive signatures in OCaml,
and interact with initialization.  Combining our recursive-module elaboration
with \ZipML would be valuable both practically---as a route to an OCaml-like
implementation---and conceptually, because it could give a source-level
formalization of the identity-tag/source-to-source encoding used to control
module identity and applicativity.
 
\paragraph{Recursive linking and mixin composition.}
Recursive modules are only one point in a broader design space of module
composition.  Cl\'ement Blaudeau's thesis distinguishes immediate vs. delayed
composition, sequential vs. recursive composition, and hierarchical vs. flat
composition.  OCaml's \ocaml{module rec}, and hence our calculus, is an
immediate recursive composition mechanism: a mutually recursive group is checked
against explicit external signatures.  MixML instead treats recursive linking as
a central operation, combining ML-style abstraction and translucent signatures
with mixin-style delayed composition and separate compilation
\cite{rossberg_mixinup_2013}.  This addresses a different axis from ours.  Our
focus is the type-theoretic account of OCaml-style recursive signatures,
including double vision and cyclic type equations; we do not provide a general
separate-compilation or recursive-linking discipline.  Understanding how our
applicative sealing and explicit $\mu$-types interact with mixin-style linking is
a natural next step.
 
\paragraph{First-class recursive modules.}
\RoneML~\cite{jaakkola2020type} explores a different extension point: it adds
recursive first-class modules to the 1ML programme of unifying core language and
modules.  Its elaboration target is a variant of GHC's System~$F_c$, using type
equality coercions and local axioms to express the equalities needed to avoid
double vision.  This makes \RoneML orthogonal to our goal of modeling the
second-class OCaml module layer with applicative and generative functors.
Moreover, \RoneML leaves recursive linking outside its scope, whereas our work
leaves first-class recursive modules outside its scope.  A detailed comparison
would therefore have to separate two axes: first-class module values and
recursive linking on the one hand, and OCaml-style recursive signatures with
transparent/applicative type equalities on the other.
 
\paragraph{Initialization safety.}
Safe initialization is orthogonal to the static issues studied here.  Our
elaboration explains how recursive modules may be typed, how abstract types are
refined to avoid double vision, and how transparent cyclic type equations become
explicit $\mu$-types.  It does not by itself replace the source-level analysis
needed to rule out premature access to uninitialized recursive components.
Existing systems make different choices: RMC and Traviata include static
well-foundedness disciplines, whereas OCaml uses a conservative static check
together with a runtime check that may fail during module initialization; Moscow
ML also relies on runtime checks in its implementation
\cite{\PaperRTG,nakata_recursive_nodate,leroy2003proposal,10.1145/507669.507644}.
Integrating a more precise initialization analysis with our elaboration is left
for future work.
 
\paragraph{Iso-recursive source disciplines.}
Finally, our target calculus is type sound with recursive types at arbitrary
kinds, but our algorithmic checker currently restricts transparent cyclic
signatures to base kind in order to keep equivalence checking decidable.  A
promising way to recover more source programs without exposing arbitrary
higher-kinded equi-recursive equality is to treat some datatype recursion
iso-recursively at the source level.  Explicit or abstract \ocaml{fold}/\ocaml{unfold}
coercions could hide higher-kinded recursion behind datatype or module
abstraction boundaries, so that equivalence checking need not unfold recursive
constructors transparently.  This would not subsume transparent equirecursion in
general, but it may capture common recursive-datatype patterns while preserving
a practical decidable type equivalence.

5. Shorter pasteable version

If the section must be shorter, use this compressed version:

\subsection{Other aspects and future directions}
\label{sec:rw-other}
 
\paragraph{Toward a practical source type system.}
Our semantics follows the \Fing/\Momega line of elaborating modules into a typed
core calculus \cite{\PaperFing,\PaperMomega}.  A complementary direction is
\ZipML~\cite{\PaperZipml}, a path-based source type system with zipper
signatures and floating fields, designed to avoid signature avoidance while
remaining close to OCaml's implementation.  Recursive modules are left as future
work in \ZipML because they raise double vision and interact with OCaml's
annotation and initialization discipline.  Combining our recursive-module
elaboration with \ZipML would provide a practical route to OCaml and a clearer
source-level formalization of the identity-tag/source-to-source encoding used to
control module identity and applicativity.
 
\paragraph{Recursive linking and mixins.}
OCaml's \ocaml{module rec} is an immediate recursive-composition mechanism:
mutually recursive modules are checked as one annotated group.  MixML addresses
a different axis, namely delayed recursive linking and separate compilation,
while retaining ML-style abstraction and translucent signatures
\cite{rossberg_mixinup_2013}.  Our work explains OCaml-style recursive
signatures, double vision, and cyclic type equations; it does not provide a
general recursive-linking discipline.  Understanding the interaction between our
applicative sealing, explicit $\mu$-types, and mixin-style linking remains future
work.
 
\paragraph{First-class recursive modules.}
\RoneML~\cite{jaakkola2020type} adds recursive first-class modules to the 1ML
programme, elaborating to a System~$F_c$ variant with local equality axioms for
double vision.  This is orthogonal to our focus on the second-class OCaml module
layer with applicative and generative functors: \RoneML leaves recursive linking
outside its scope, while we leave first-class recursive modules outside ours.
 
\paragraph{Initialization and iso-recursive source disciplines.}
Safe initialization is orthogonal to the static issues studied here.  RMC and
Traviata provide static well-foundedness disciplines, whereas OCaml uses a
conservative static check plus a runtime initialization check that may fail
\cite{\PaperRTG,nakata_recursive_nodate,leroy2003proposal}.  Another orthogonal
future direction is to recover more higher-kinded recursive patterns through
source-level iso-recursive datatypes: explicit or abstract \ocaml{fold}/\ocaml{unfold}
coercions could hide recursion behind datatype/module abstraction boundaries,
avoiding arbitrary transparent higher-kinded equi-recursive equality while
keeping type equivalence practical.

6. Citation-key issues to resolve before pasting

Current source uses these keys/macros:

• \PaperMomega expands in zipml.tex to Blaudeau-Remy-Radane/fulfilling@oopsla24, but I did not find that BibTeX entry in modules.bib. The PDF exists locally. Add/restore the OOPSLA 2024 entry if you cite it.
• \PaperZipml expands to Blaudeau-Remy-Radane!zipml@popl25, and this key exists in modules.bib.
• \PaperFing expands to Rossberg-Russo-Dreyer/Fing@jfp2014, and this key exists.
• rossberg_mixinup_2013 exists.
• jaakkola2020type is used in sections/related-work.tex, but I did not find it in modules.bib. The PDF exists locally; add a thesis BibTeX entry if you keep the R1ML paragraph.
• leroy2003proposal, 10.1145/507669.507644, and nakata_recursive_nodate exist or are already used in the draft.
• \PaperRTG expands to Dreyer/RTG@icfp2007; previous evidence suggests the local modules.bib may instead contain another key for RTG/RMC or may be missing the exact RMC paper. Verify before final compile.

7. How to place ZipML relative to the Double Vision section

Your instinct is right: ZipML can be mentioned at the end of Double vision, because the source-to-source identity-tag encoding is conceptually part of controlling module identity/applicativity. However, I would avoid inserting a long ZipML paragraph inside Double vision, because ZipML itself does not solve recursive-module double vision yet; it explicitly leaves recursive modules to future work.

Suggested compromise:

• At the end of Double vision, add one sentence: “The source-to-source identity-tag view also suggests a future source-level account in the style of ZipML, whose zipper signatures are designed to keep path-based signatures practical while elaborating to Mω.”
• Then in Other aspects, use the longer ZipML paragraph above.

8. One possible final narrative arc

The full Related Work chapter can now read as:

1. Foundations and feature matrix: CHP, Moscow ML, OCaml, RTG/RMC, Traviata, Im et al., Mω.
2. Double vision: RTG/RMC solution; our Mω substitution/fixpoint solution; source-to-source identity tags; ZipML as future source formalization.
3. Cyclic types: CHP higher-kinded equirecursive issue; later systems avoid/approximate; our explicit μ-types and contractiveness.
4. Other/future directions:
   • practical source/typechecker system: ZipML;
   • recursive linking/separate compilation: MixML;
   • first-class recursive modules: R1ML;
   • initialization safety;
   • iso-recursive source disciplines.

This keeps Double Vision and Cyclic Types as the technical core, while making the section look complete to readers who expect to see Mω, ZipML, MixML, first-class modules, and initialization mentioned.