Applicative vs generative encoding — is the () barrier the only difference?
Status: waiting (needs collaborator confirmation)
The double-vision source encoding may need two mode-specific variants. The conjecture: the generative variant is identical to the applicative one modulo a () barrier that prevents path equality from leaking. Is that the only difference, or does generativity require more?
What would settle it
Either a proof that the ()-barrier variant is sufficient, or a counterexample where generativity needs additional structure. Flagged #waiting on collaborator input.
Related
Double-Vision Recursive Modules · Source-to-Source Encoding Correctness