[Agda] Allow cyclic module imports

[Tom Murphy]

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!

Tom

On Thu, Apr 26, 2018 at 5:35 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> 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
> >
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180428/c543532b/attachment.html>