Streamline Parameterized Module use

[jldodds]

I'm writing a literate spec meant to mirror an RFC. Ideally this specification would be all in one file, but let's call that a stretch goal.

The spec is parametrized over a hash

module A where

parameter
    hash : {MsgSize} (fin MsgSize) => [MsgSize] -> [8]

and it has some number of functions that use the hash definition.

I've got another file that contains a hash function and I would like to use it for a test case so I create another module

module ASHA2 = A where

import hashfile

hash = sha2

And then another module for the test cases

module ASHA2tests where

import ASHA2

tests...

This requires 3 files, which is more than I would like. I can get it down to two using the backtick notation:

module ASHA2tests where

import `A

tests...

But then I have to specify my hash function at least once for each function in module A that I want to call.

@yav's notes suggest a syntax like

module ASHA2tests where

import A as ASHA2 where
    hash = sha2

tests...

[yav]

That syntax has a few issues, which is why it is not implemented:

1. What's in scope in the where clause of the import instantiation (e.g., in your example where is the definition of sha2)?

2. If I have two imports with the same instantiations, do they result in the same generated module or not (i.e., are the functor applications "generative" or "applicative").

I think a relatively simple solution might be to think of these local import instantiations as a short-cut for the current behavior. More concretely, writing:

import A as X where ... (stuff) ...

should have the same meaning as writing:

module SomeNewName = A where ... (stuff) ... 

and then the import is replaced by:

import SomeNewName as X

With such a design my questions above would be answered as follows:

1. Nothing is in scope in the where clause of an import, you have to add imports or definitions manually.
2. We are going for the "generative" option, where each instantiation results in a conceptually different module, even if the instantiation is exactly the same.

I think that an approach like that would work fine for situations where you intend to do the instantiation just once, however multiple instantiations would lead to multiple copies of the code, which is undesirable.

Another option would be to do something similar, except that we try to compute the name of the new module (SomeNewName above) from the values of the parameters. This would probably require some syntactic restrictions on the form of how parameters can be defined (e.g., value parameters must be either a constant or a name). However, it could give us the "applicative" functor behavior in the common case.

Thoughts?