Martín Hötzel Escardó
2018-04-25 20:01:25 UTC
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
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