Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

recursive modules fail to compile recursive compilation units #5286

Open
vicuna opened this Issue Jun 9, 2011 · 2 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Jun 9, 2011

Original bug ID: 5286
Reporter: @lefessan
Status: acknowledged (set by @gasche on 2012-01-22T22:32:00Z)
Resolution: open
Priority: normal
Severity: feature
Platform: all
OS: all
OS Version: all
Version: 3.12.0
Category: typing
Tags: patch
Monitored by: @jberdine @alainfrisch

Bug description

It is possible to write recursive compilation units, i.e. compilation units with recursivity in their types, and correctly compile and link them with ocaml. However, copying their sources into one "module rec" construct will fail for two reasons:

  • during the typing phase, the approximation of all the modules types is computed in the initial environment, while it would be useful to have, for each module, an environment that is already enriched with the approximation of the previous modules
  • during the linking phase, modules are reordered, based on an approximation of their shape, leading to a runtime error, even if a topological order exists and would not fail at runtime.

The following patch fixes the two issues:

  • in typemod.ml, it computes the approximations of the modules while enriching the environment with the previous approximations
  • in translmod.ml, it computes first a topological order of the dependencies between modules, and uses that topological order for the modules that can be completely initialized in that order, leaving the other modules being reordered as before.

File attachments

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 22, 2012

Comment author: @gasche

I believe recursive modules are the kind of topics where there is a tension between pragmatical usefulness and theoretical understanding of the implementation.

The current semantics is quite crude but also simple; it's unsatisfying yet easy to reason about for the programmer that would wonder which code is is accepted, may fail at runtime, or always succeed.

The change you propose may help in practice, but at the same time increase the overall complexity of the language semantics, and make it unclear what the behavior will be. In some cases, especially when we don't know yet what a clean solution is, being predictable wins over being convenient.

One interesting angle is the ordering robustness. I would be a bit wary of your suggestion to enrich the typing environment during typing, because it may result in the type system accepting modules if typed in some order, and rejecting them in some other order.

The suggestion of topological sort is robust wrt. ordering. The current semantics also specify some sort of dependency sorting (computation of "safe" modules dependencies). Maybe your criterion is thus relatively solid, and would in particular still stand in an hypothetical next version of recursive module semantics based on hypothetical better theoretical grounds. That requires to be careful, though.

To sum up, the questions are: "Is it worth trying to fiddle with recursive modules if we don't even have a reasonable semantics for them? Could such pragmatic changes complicate theoretically-motivated changes later on?". Given the lack of enthusiasm of caml-devs to tackle this bug so far, I'd be tempted to guess that their answer to the first question is not a clear "yes". But maybe Alain's proposal in implicit compilation unit recursion could bring more value to those borderline changes.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 23, 2012

Comment author: @xavierleroy

Let me record my thoughts about this proposal.

  • On the typechecking side: the typing algorithm is incomplete (and I doubt a complete algorithm exists), and, by experience, any change we make on the algorithm causes some existing program to break. It's like a bump on a rug: you can move it away but not flatten it. So, it is my policy not to change the typing of recursive modules except to fix an unsoundness issue.

  • On the compilation side: we have more liberty here, as it is possible to convince oneself that a change is backward-compatible. So, I'm not opposed but would like to see more motivations (other than "I took separately-compiled units that rely on the undocumented cross-unit type-level recursion trick and when I put them in a single file they don't compile").

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.