Tony's Wiki

related-work-review-evidence-status

4 min read

Evidence status for related-work-factcheck.md

This note answers the user’s follow-up about evidentiary grounding.

What was reviewed

The generated review related-work-factcheck.md was based on:

  • manual.tex
  • sections/related-work.tex
  • ocamod.sty for macros
  • modules.bib
  • Zotero PDF folder /Users/ltzhou/Downloads/Recursive Modules

It was not based on figures/related-work-legacy.tex. That legacy file was not used as the review target. I only opened the beginning of it later to confirm that it is a separate legacy draft.

PDF-reading method

I did not read all 37 imported PDFs end-to-end. I used:

  • file discovery over /Users/ltzhou/Downloads/Recursive Modules;
  • pdftotext -layout to extract text from selected PDFs;
  • targeted keyword searches for terms such as double vision, applicative functor, generative functor, higher-order functor, contractive, opaque, path resolution, type inference, soundness, and initialization;
  • focused snippets from the selected PDFs to check claims.

Therefore the original review should be treated as an evidence-informed review, not as a fully quoted literature audit.

Claims that were directly grounded in PDF text snippets during the review

High confidence / directly checked against PDF text:

  1. Dreyer/RTG vs RMC distinction:

    • Checked in Dreyer - 2007 - Recursive type generativity.pdf and Dreyer - A type system for recursive modules.pdf.
    • The RMC paper says RTG solves double vision at the System-F-style core-calculus level and RMC scales RTG to recursive ML-style modules.

  2. Im et al. 2011 does not support applicative functors:

    • Checked in Im et al. - 2011 - A syntactic type system for recursive modules.pdf.
    • The paper explicitly says it does not support applicative functors and supports only generative functors as in SML.

  3. Garrigue–Nakata path resolution issue:

    • Checked in Garrigue and Nakata - 2011 - Path resolution for nested recursive modules.pdf.
    • The abstract/introduction states that path resolution termination is undecidable even without higher-order functors and motivates decidable restrictions.

  4. Russo/Moscow ML lack of completed soundness proof:

    • Checked in Russo - 2001 - Recursive structures for standard ML.pdf.
    • The paper says it does not attempt the type-soundness proof, though it expects one via known techniques.

  5. RMC generative/applicative distinction:

    • Checked in Dreyer - A type system for recursive modules.pdf.
    • The paper states RMC supports generative functors and contrasts this with OCaml’s applicative functor semantics.

  6. Traviata call-by-value soundness and initialization relevance:

    • Checked in Nakata and Garrigue - Recursive modules for programming.pdf.
    • The paper discusses recursive modules, initialization, and call-by-value soundness.

  7. MixML broad comparison:

    • Checked in Dreyer and Rossberg - Mixin’ Up the ML Module System.pdf.
    • The paper positions MixML as recursive linking/separately compiled components with ML-style abstraction and notes applicative behavior as future work.

  8. F-ing/Momega lineage:

    • Checked in Rossberg et al. - 2014 - F-ing modules.pdf, Rossberg - 1ML – Core and Modules United.pdf, and the local Momega/Blaudeau PDFs enough to verify the general module-elaboration line.

Claims that are synthesis / should be rechecked before putting in the paper

These are not necessarily wrong, but the previous review did not attach enough primary-source evidence to treat them as final paper claims:

  1. Exact feature-table cells, especially:

    • Moscow ML higher-order/applicative functor support in the formal calculus vs implementation;
    • RMC higher-order functor support;
    • Traviata first-order vs higher-order functor status;
    • OCaml cyclic-type status.

  2. The statement that “Traviata and OCaml work because they do not solve double vision.” The review already recommended weakening this, but any final wording needs direct textual support.

  3. The claim that RMC rejects all unguarded cycles or mandates every cycle pass through a datatype. This captures the intuition from the undefined/static check but should be phrased more conservatively unless tied to a precise source passage.

  4. The exact classification of the three cyclic examples in sections/related-work.tex as RTG/Traviata/Momega accept/reject. This should be verified case-by-case against the cited papers and the current formal rules.

  5. Broad novelty claims such as “first formalization that simultaneously supports X/Y/Z”. These require a careful, citation-backed comparison and probably should be phrased with “to our knowledge” plus precise scope.

Bottom line

The previous review is useful as a map and first-pass fact check, but it should not be treated as a fully evidence-certified review where every sentence is backed by quoted PDF passages. A stricter next version should include, for each claim, the exact PDF title and a short source quotation/snippet.

Graph View