[Agda] Allow cyclic module imports

[Sergei Meshveliani]

For example, Haskell  allows cyclic module import, and I used such. 
A real-world library for mathematics is likely to use cyclic module
import.
But Agda is somewhat more complex, I do not know where this may lead
to. 

------
Sergei



On Wed, 2018-04-25 at 21:01 +0100, Martín Hötzel Escardó wrote:
> But of course still check that any cyclic definitions within the cyclic 
> modules are well founded.
> 
> I don't want to put this as a feature request before we discuss this and 
> see the (un)desirable consequences that I haven't seen on my own.
> 
> To some extent, breaking anything into modules is arbitrary and depends 
> on taste. But, nevertheless, modules are useful to aid understanding 
> (and compilation efficiency too).
> 
> However, I often find myself creating artificial modules to break module 
> import cycles. And I am sure you do to.
> 
> Here is a concrete example.
> 
> I have four modules UF-Subsingletons*, two modules UF-Equiv*, two 
> modules UF-Retracts* because
> 
> (1) in order to define equivalence, we need to know what subsingleton 
> types are and some properties of them.
> 
> (2) in order to prove some properties about subsingletons, we need to 
> use some properties of equivalences.
> 
> (3) in order to prove some more properties of equivalences, we need to 
> prove some more properties of subsingletons.
> 
> (4) and then add retracts to the picture, and something analogous to 
> (1)-(3) takes place.
> 
> My original development was monolitic because of that. In one (big) 
> file, you develop things in the mathematical order they are needed.
> 
> Then I refactored it into "topics" (as above). But then the same topic 
> needed several modules, as explained.
> 
> Couldn't we just allow cyclic module imports, provided the total set of 
> definitions in all modules are well founded?
> 
> There are a number of things to consider:
> 
> (1) Is this easy to implement?
> 
> (2) Does it have conceptual / software engineering disadvantages?
> 
> Looking mathematically at the problem, I see things like this: we have a 
> directed acyclic graph of definitions (or replace acyclic by well 
> founded). Assigning them to modules amounts to quotienting this graph. 
> Such quotients are seldom nice - they hardly ever reflect the structured 
> of the unquotiented graph. In particular, in the development I am 
> discussing, the module-picture of the development ( 
> http://www.cs.bham.ac.uk/~mhe/agda-new/module-graph.pdf) clearly shows 
> (to me) that most of the dependencies are artificial when particular 
> definitions in particular modules are considered.
> 
> Martin
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>