[New module system] Interfaces with definitions

[yav]

Consider the following example of an "interface" that's currently rejected:

// I_BlockCipher.cry
interface module I_BlockCipher where
 type Key: *
 type BlockSize: #

 type Block = [BlockSize]  // illegal assignment in interface

 encipher: Key -> Block -> Block
 decipher: Key -> Block -> Block

We currently reject such declarations because interfaces are not allowed to define anything, they just declare the kinds/types of things. While semantically this makes sense, it is quite inconvenient as a language construct, and indeed the current system does not seem to have a way to express this sort of thing at all, which is unfortunate.

It seems that we could allow definitions in interfaces, which would essentially make them into a kind of functor. The idea would be that when a module imports an interface, it would get the parameters (just like now) but also it'd get the extra definitions. When instantiating a functor, we just need to add the definitions to the new module, at the same time when we add the parameters.

If we adapt this plan, then we can also change the handling of functors with parameter style parameters:

• currently these are desugared into a "new style" functor that imports an anonymous interface computed from the parameters block
• instead, these functors would become "interfaces" (i.e., the things that can be imports via "interface" imports in new-style functors)

There is however a question of what definitions should be allowed in an interface. In particular, I am not quite clear if it makes sense to define modules nested in "interfaces".

[yav]

If we do implement this, and also backtick imports we'll have to make sure that the two interact properly. They should work OK, as long we just allow declarations that are valid in a where clause. Here is an example:

-- This is basically an "interface"
submodule I where
   parameter
      type n : #
      type constraint (fin n, n > 1)

   type T = [n]

  parameter
      f : T

   g = f + 1

submodule M where
   import `submodule I

   h = g + 1

Then module M should be desugared like this:

submodule M where
   h : {n} (fin n, n > 1) => [n] -> [n]
   h f = g + 1
      where
      type T = [n]
      g = f + 1

Basically the parameters to the module become parameters to definition as before, and any local definitions go in a local where block. Since local type synonyms are not in scope in the signature, they'll have to be expanded there. This rewrting happens on already typechecked syntax though, so it is also possible to simply expand the type synonyms defined in the interfaces everywhere.

[yav]

The new module system branch now allows type/prop synonyms in interfaces, which allows definitions of type synonyms which may be used in the value parameters of a module. This is the main component that couldn't be expressed before---other definitions can go into a functor.