Modules

Currently this page is a collection of ideas relating to NV modules. We're using it to keep track of ideas, questions, thoughts, examples, etc. that will inform our design.

Needs:

1. Modules should be able to represent an SRP, much like the Syntax.network type does now.
2. Given a module that represents an SRP, we should be able to get a solution that can be used later on. i. For example, let m = solution RIP. In SMT terms, this should declare a symbolic map m and a requires clause which constraints m to be the solution of RIP.
3. Users should be able to declare modules, and reference module fields, e.g. RIP.merge
4. We should be able to typecheck modules (and probably also do type inference). We've run into a lot of problems where transformations propagate incorrect types, and being able to spot these automatically would be very helpful.
5. It would be nice to allow declarations within modules in an arbitrary order, and try to topologically sort them to check for dependency loops.
6. It would be nice for modules to be able to represent different "layers" of the network; e.g. one module for RIP and one module for iBGP that have different connections.
7. It would be nice to have files automatically turned into a module.
8. We should be able to have primitives that represent whole program transformations that can't be simply expressed in NV (e.g. slicing, compression) that can be used like functors in an NV program.

Questions:

1. Should modules be able to contain a topology, or should they all reference one overarching topology? Pros: Can represent different logical levels of connectivity, non-generic algebras need a topology to be meaningful. Cons: Modules which use another solution have to map between topologies, makes node and edge types unclear (one type per topology?)
2. Should we include something like OCaml functors? These let us represent routing algebra combinators in the same language as the algebras.
3. Relatedly, how should we handle NV code with modules (and possibly related things like functors) sprinkled about?
4. Do we want module signatures?
5. Do we want higher-level metalanguage combinators? Something like that?

Thoughts:

1. We've talked about generalized assertion functions which take full solutions instead of individual node/attribute pairs. Those would work nicely with this change. Yes, we should do them.
2. Combining a bunch of points: I (personally) would like two different pieces of functionality from modules: first, to be able to define generic algebras (e.g. RIP) independent of topology; second, to be able to represent an entire SRP as a module. Perhaps a natural way to do this is to represent that latter as a module and the former as a functor-like thing which returns a module (when given a topology/init/etc).