Rexporting functor parameters in an instantiation

Consider the following example (the use of submodules is not important, it is just easier to work with a single file):

submodule F where
  parameter type n: #
  f: [n] -> [n]
  f x = x

submodule M = submodule F where type n = 8

// g: [M::n] -> [M::n]
g = M::f

The definition of g is OK, but we cannot write the type signature, at least not in the style in the comment. The reason for that is that n is a module parameter, and its instantiation is not exported my M.

Workaround 1: Manual Export

submodule F where
  parameter type n: #
  type p_n = n             // This "exports" the parameter
  f: [n] -> [n]
  f x = x

submodule M = submodule F where type n = 8

g: [M::p_n] -> [M::p_n]
g = M::f

The draw-back to this approach is that you have to make a new name (e.g., p_n) and possibly duplicate stuff (e.g., docstrings).

Workaround 2: Save Parameter Module

submodule F where                                                                
  parameter type n : #                                                              
  f : [n] -> [n]                                                                    
  f x = x                                                                        

// Now `M` has both the parameters and the instantiation                                                   
submodule M where                                                                
  submodule Param where                                                          
    type n = 8                                                                   
  submodule Impl = submodule F { submodule Param }                               

g: [M::Param::n] -> [M::Param::n]                                                
g = M::Impl::f

The drawback here is that things look more complex than, perhaps, they should be, and one could accidentally use the wrong Param qualifier if a functor has multiple parameters.

The Challenge

There are two reasons for the current design (i.e., to not make parameters available in the instantiated module):

It is not clear what names to use for interfaces that are imported qualified (e.g., import interface I as I). Note that we cannot just use x for parameter I::x because the module might already contain x. It is also possible to import the same interface more than once.
We'd need some mechanism the control which parameters should be exported.

A Way Forward

Here's one possible design that could allow us to "export" functor parameters in common cases:

Only allow "exporting" functor parameters that are imported through an unqualified interface. Importantly, the common case of using a parameter block is just syntactic sugar for this. This should address issue (1) above.
Allow public/private blocks in interfaces (and by extension, parameter blocks). This indicates the visibility of the parameter in instantiations.

Related to (2) there's the question of what should be default visibility of interfaces. The most backward compatible choice would be to make them private by default (i.e., we'd basically get the current behavior where nothing is exported, and one would have to add a public annotation to exported parameters). The drawback of this choice is that is the opposite of other modules, where things are public by default. Because of that we don't actually have a public keyword at the moment but, hopefully, it should not be a big deal to add this.

Thoughts?

It seems weird to have public/private annotations in interfaces, since interfaces are supposed to define public stuff.

My thought would be that it's not, therefore, really sensible for interface parameters to be private and that there's no need to worry about that -- if you really want it to be private chances are it ought to be a parameter of the underlying module and not the interface. I think.

If naming is a concern one could introduce an extra reserved (sub)module name, e.g. I::Parameter::x. I kind of think it's wrong to have a parameter named x in an interface/module that also defines an x but perhaps that ship's sailed. (Or maybe doing that makes the parameter inaccessible.)

FWIW in ML this doesn't arise because functor arguments can only be modules, not types. So you're always doing Workaround 2.

Overwriting a parameter name with a declaration of the same name is common, for example key and block types for a mode derived from a block cipher, or a carrier type for a field derived from additive and multiplicative groups over the same carrier type.

Forward (1) could not apply to any of the growing number of use cases involving functors that import multiple and/or qualified interfaces. Challenge (1) could be overcome if importers of an instance could (through reserved naming as @sauclovian-g suggested, or syntax as suggested below) refer to (and if necessary alias) the qualified interface names that are already necessary to instantiate such functors, to "recover" the submodules and/or parameter values implementing these interfaces:

submodule Functor where
  import interface I  // or `Iface as I`
  import interface J

submodule Impl where ...
submodule Jmpl where ...

submodule Instance = submodule Functor { I = submodule Impl, J = submodule Jmpl }

// `Importer` needs `Instance` and knows `Functor`'s interface(s) `I` and `J`,
// but not `Instance`'s implementations `I = Impl` or `J = Jmpl`.
submodule Importer where
  submodule Impl' = interface I of submodule Instance
  // or some other backward-compatible syntax or reserved naming convention
  submodule Jmpl' = interface J of submodule Instance

// `= interface of` (omitting an interface name) could extract the implementation of an anonymous interface (`parameter` block)

Importer could avoid any name collisions by naming submodules it recovers from Instance distinctly from the rest of its namespace, as is already its responsibility when importing any other (sub)modules. Where Functor sees I::x, Importer would see Impl'::x.

Parameter values could be recovered directly using a corresponding direct import rather than a submodule assignment:

submodule ParameterImporter where
  import interface I of Instance as Impl'
  import interface J of Instance as Jmpl'

Direct parameter recovery could grant access to individual parameters (as in #1494 and cryptol-specs #79 (comment)), and submodule recovery might also address some issues arising from generative instantiation (#1484, #1581 (comment)), where the type checker does not recognize declarations from different instances of the same functor with equivalent implementations as equivalent. This comes up, for example, when a test module reconstructs an implementation of a custom field interface (not just an instance of the primitive Field typeclass) used to instantiate an elliptic curve parameterized over the same field interface. When the test module specifies affine points over the field and then tries to test elliptic curve operations, Cryptol reports an error that the test module's field is not compatible with the elliptic curve instance's field, even though they have the same implementation. Whether submodule recovery would actually solve that problem would depend on the type checker recognizing the recovered (sub)module implementation as equivalent to the instance's implementation. Applicative instantiation might more generally solve the same problem.

In case it is helpful, this is how OCaml modules handle the situation (assuming that references to n in the body of F are known to be equal to the parameter type n):

module F(X : sig type t end) : sig val f : X.t -> X.t end = struct
  let f x = x
end;;
module F : functor (X : sig type t end) -> sig val f : X.t -> X.t end
module M = F(struct type t = int end);;
module M : sig val f : int -> int end

The only difference is that a functor argument must be named (here, I've named it X), whereas in Cryptol it may be anonymous.

Is it possible to type g as g: [8] -> [8]?

I tried your example in my local Cryptol and I couldn't get it to accept g = M::f. I got:

module L where

  submodule F where
    parameter type n: #
    f: [n] -> [n]
    f x = x

  submodule M = F where type n = 8

  g = M::f

[error] at L.cry:10:7--10:11
    Value not in scope: M::f

Also, the key to deciding what the behavior 'should be' here is deciding whether or not the n in the functor's formal parameter and the (implicit) n in the functor's return module signature should be unified or not.

module F(X : sig type t end) : sig type t val f : t -> t end = struct
  type t = X.t
  let f x = x
end;;
module F : functor (X : sig type t end) -> sig type t val f : t -> t end
module M = F(struct type t = int end);;
module M : sig type t val f : t -> t end

If you don't unify them, the type you want to assign to g in your original program doesn't make sense (since M doesn't declare a type n). Suppose, instead, you unify them (as in the previous comment's OCaml example). In that case, you should be able to type g as g: [8] -> [8] (since substitution of the type variable is the only sensible thing to do, as n isn't a type declared by the module produced by F).

I guess one last thought... if you don't want the user to have to type [8] -> [8] everywhere, you should be able to do something like:

type n = 8
submodule M = F where type n = n

g: [n] -> [n]

That way, if you want to change n later, you only have to change the type alias.

GaloisInc / cryptol