[New module system] "Inheriting" and "distributing" interfaces/parameters of imports

[rybla]

Suppose that you have two modules, A and B and a module interface, I. A imports I, and B imports A. Your intention is for B is to use A without yet instantiating the import of I it is parametrized by. There are two basic kinds of ways to do this:

1. A inherits B's parametrized interface i.e. A is parametrized by I and (in some way) "passes" its parametrized instance of I to A when it imports A.
2. A distributes B's parametrized interface over its declarations i.e. each declaration in B that used something from I becomes parametrized by those things before being imported into A. This is analogous to the "backtick" import that Cryptol used to support before this new module system.

Inheriting interfaces/parameters

Inheriting an named interface

Inheriting a named interface is currently impossible. There is no way to import an interface and pass it as a functor argument when instantiating a module that is parametrized by the same interface. It seems reasonable that you should be able to write something like (not that this uses the same syntax as #1368):

module interface I where
a : *
x : a

module A where
import I

module B where
import I
import A { I = I }

Inheriting an anonymous interface

Inheriting an anonymous interface is currently possible, but still clunky.

module A where
parameter
  a : *
  x : a

module B where
parameter
  a_ : *
  x_ : a

submodule A_inst = A where
  a = a_
  x = x_
import submodule A_inst

With #1368, this becomes a slightly more clean, but still requires redundant names:

module A where
parameter
  a : *
  x : a

module B where
parameter
  a_ : *
  x_ : a

import A where
  a = a_
  x = x_

A much better syntax for this common task of inheriting parameters would be something like the following.

module A where
parameter
  a : *
  x : a

module B where
import A inheriting (a, x)

This can be combined with #1368 like so:

module A where
parameter
  a : *
  x : a

module B where
import A inheriting (x) where
  a = [8]

This is just syntax sugar for

module A where
parameter
  a : *
  x : a

module B where
parameter
  x : [8]

import A where
  a = [8]
  x = x // pretend that the first x is from A, the second x is from B

(This is sort of like partial functor application)

Distributing interfaces/parameters

I call this "distributing" because it is a transformation of the form

(alpha, x) -> module A where { type A = T; f : t = a}
  ~~>
module A where { type A alpha x = T; f : {alpha, x} t = a}

In this way the functor's parameters are "distributed" under the module in the module's declarations (where necessary).

Since "backtick" imports were considered useful enough in Cryptol before this new module system, it's probably worth bringing back?

[yav]

We can now to this using the following notation:

module A where
  import I
  ...

module B where
  import I as X
  import A { interface X }

Basically using interface X in an instantiation means pass parameter X. By the way, the as X part is optional, if it is not provided, the name of the parameter is derived from the name of the interface. For example, you could also do something like this:

module B where
  import I
  import A { interface I }

I find the keyword interface to be a bit confusing in this context, and I think using parameter I would be more readable. Unfortunately, the keyword parameter starts a layout block (because of the top-level parameter blocks), so not sure what to do... One option would be to using something like A { module parameter I }, which could be made to work because we'd modify the layout algorithm to only start a layout block for parameter if it is not preceded by the keyword module.

[rybla]

I think this syntax is fine, since it mirrors how you pass interfaces as arguments when instantiating functors i.e.

module A = B { interface I }

It maintains the general rule that:

When interface appears before an argument when instantiating a functor (whether while importing that instantiated functor or just instantiating it normally), that indicates that the argument is an instance of the appropriately-named interface expected by that functor.

[yav]

I think we have basic support for this, so I'll close this for now. If new issues come up we can reopen or make a new tickets