Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005286OCamltypingpublic2011-06-09 19:362017-03-03 15:50
Assigned To 
PlatformallOSallOS Versionall
Product Version3.12.0 
Target VersionFixed in Version 
Summary0005286: recursive modules fail to compile recursive compilation units
DescriptionIt 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, it computes the approximations of the modules while enriching the environment with the previous approximations
- in, 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.
Attached Filespatch file icon recmodules-2011-06-09.patch [^] (3,443 bytes) 2011-06-09 19:36 [Show Content]

- Relationships

-  Notes
gasche (administrator)
2012-01-22 23:32
edited on: 2012-01-22 23:33

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.

xleroy (administrator)
2012-01-23 11:44

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").

- Issue History
Date Modified Username Field Change
2011-06-09 19:36 lefessan New Issue
2011-06-09 19:36 lefessan Status new => assigned
2011-06-09 19:36 lefessan Assigned To => xleroy
2011-06-09 19:36 lefessan File Added: recmodules-2011-06-09.patch
2012-01-22 22:51 lefessan Assigned To xleroy =>
2012-01-22 22:52 lefessan Status assigned => new
2012-01-22 23:32 gasche Note Added: 0006767
2012-01-22 23:32 gasche Status new => acknowledged
2012-01-22 23:33 gasche Note Edited: 0006767 View Revisions
2012-01-22 23:33 gasche Note Edited: 0006767 View Revisions
2012-01-22 23:33 gasche Note Edited: 0006767 View Revisions
2012-01-23 11:44 xleroy Note Added: 0006769
2013-10-08 16:14 doligez Tag Attached: patch
2017-02-23 16:36 doligez Category OCaml general => -OCaml general
2017-03-03 15:50 doligez Category -OCaml general => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker