<div dir="ltr"><div>Fwiw Haskell's cyclic module imports can be a real pain and most 
projects don't use them. Not to discourage this line of inquiry, but as a
 data point!<br><br></div>Tom<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Apr 26, 2018 at 5:35 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">For example, Haskell  allows cyclic module import, and I used such. <br>
A real-world library for mathematics is likely to use cyclic module<br>
import.<br>
But Agda is somewhat more complex, I do not know where this may lead<br>
to. <br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
On Wed, 2018-04-25 at 21:01 +0100, Martín Hötzel Escardó wrote:<br>
> But of course still check that any cyclic definitions within the cyclic <br>
> modules are well founded.<br>
> <br>
> I don't want to put this as a feature request before we discuss this and <br>
> see the (un)desirable consequences that I haven't seen on my own.<br>
> <br>
> To some extent, breaking anything into modules is arbitrary and depends <br>
> on taste. But, nevertheless, modules are useful to aid understanding <br>
> (and compilation efficiency too).<br>
> <br>
> However, I often find myself creating artificial modules to break module <br>
> import cycles. And I am sure you do to.<br>
> <br>
> Here is a concrete example.<br>
> <br>
> I have four modules UF-Subsingletons*, two modules UF-Equiv*, two <br>
> modules UF-Retracts* because<br>
> <br>
> (1) in order to define equivalence, we need to know what subsingleton <br>
> types are and some properties of them.<br>
> <br>
> (2) in order to prove some properties about subsingletons, we need to <br>
> use some properties of equivalences.<br>
> <br>
> (3) in order to prove some more properties of equivalences, we need to <br>
> prove some more properties of subsingletons.<br>
> <br>
> (4) and then add retracts to the picture, and something analogous to <br>
> (1)-(3) takes place.<br>
> <br>
> My original development was monolitic because of that. In one (big) <br>
> file, you develop things in the mathematical order they are needed.<br>
> <br>
> Then I refactored it into "topics" (as above). But then the same topic <br>
> needed several modules, as explained.<br>
> <br>
> Couldn't we just allow cyclic module imports, provided the total set of <br>
> definitions in all modules are well founded?<br>
> <br>
> There are a number of things to consider:<br>
> <br>
> (1) Is this easy to implement?<br>
> <br>
> (2) Does it have conceptual / software engineering disadvantages?<br>
> <br>
> Looking mathematically at the problem, I see things like this: we have a <br>
> directed acyclic graph of definitions (or replace acyclic by well <br>
> founded). Assigning them to modules amounts to quotienting this graph. <br>
> Such quotients are seldom nice - they hardly ever reflect the structured <br>
> of the unquotiented graph. In particular, in the development I am <br>
> discussing, the module-picture of the development ( <br>
> <a href="http://www.cs.bham.ac.uk/~mhe/agda-new/module-graph.pdf" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe/<wbr>agda-new/module-graph.pdf</a>) clearly shows <br>
> (to me) that most of the dependencies are artificial when particular <br>
> definitions in particular modules are considered.<br>
> <br>
> Martin<br>
> <br>
> <br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
> <br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>