Parameterized module that extends another parameterized module

[brianhuffman]

Let's say I have a module A with a parameter x that defines some functions. Next I want to define another module B with parameters x and y, and I want functions in B to call functions from A, with parameter x passed through from B to A. How can I do this?

Or to put things another way: Say I am working on a parameterized module, and it is getting pretty big; I'd like to split a part off into a sub-module, which might use some subset of the top module's parameters. How can I do this?

[yav]

I don't think we can do this nicely at the moment. The only way we have of importing non-instantiated parameterized modules is with the backtick imports, but then you'd have to provide the parameters manually all the time.

Any ideas on how this should work?

[yav]

One way this could work, although it looks a bit complex is like this:

we allow importing parameterized modules but their arguments must also be arguments of the importing module (with the same types).

Here is an example:

module A where
   parameter f : [8]
   a = f

module B where
    import A
    parameter f : [8]
    b = a + f

Now consider C, an instantiation of B. To implement this, we need to generated an instantiation of A (with some internal name, say A'), and then change the import in C from A to A'.

If, otoh, module B is imported with a backtick, then we'd have to treat the import of A as if it also had a backtick, and rewrite uses of identifiers of A in B to pass the parameters as needed.

Seems kind of complicated, so I wonder if there is a better way to do it.

[brianhuffman]

Here's the syntax I'd like to be able to use. Basically I want to be able to put a where clause on the import statement when I'm importing a parameterized module.

module A where
parameter
  type n : #
  f : [n] -> [n]
[...]

module B where
import A as A64 where
  type n = 64
  f x = x + 1

Furthermore, the set of variables in scope inside the import/where clause should include (at least) the parameters of the current module, and names imported from other previously-imported modules.

module C where
parameter
  k : #
import Foo as Foo
import A where
  type n = k
  f = Foo::foo`{size=k}

It'd be convenient if other top-level declarations from the current module were also in scope for the import/where clause. I'd be OK with having restrictions on cyclic dependencies to avoid module-level recursion.