RFC: We need bundling

[andres-erbsen]

Parametrizing every definition in a module individually leads to explosion in the number of parameters. See https://gist.github.com/andres-erbsen/3c4989ad05673f6807728b9ecccd0557 for an example. It would be nice if we figured out to how to modularize our code in a way that does not cause that.

In particular, I am thinking of the following:

Record field := { F:Type; add : F->F->F; ...; is_field F add ... }

Section Edwards.
  Context {f:field}.
  (* "from f import *" *)
  Let add := F.(add)
  Let mul := F.(mul)
  ...

 Lemma edwards_curve_is_group : is group ... .
 Qed.

  (* only this would be used from outside *)
 Definition edwards_curve_group : group := {
   op := point_addition;
   ...
   is_group := edwards_curve_is_group
 }

The module system could do this automatically for us, but would not let us Check module instantiations, determine module parameters from Ltac, or parametrize modules by something other than modules.

I am not sure how mechanically we could convert the existing codebase, but let's figure out what to do first.

Another question is how liberally we should use this construction. I definitely wouldn't want generic lemmas (e.g., about properties of fields) to talk about projections from bundles -- it is important that a lemma can be applied even if the goal is not in bundled form.

[JasonGross]

I will argue against using the module system this way. It enforces the choice on all downstream code, modules and module functors are some of the hairiest parts of the kernel, as I understand it.

[andres-erbsen]

Yeah, I am quite strongly against using the module system as well. This RFC is primarily for figuring out how to get the behavior we want without the module system, presumably using records.

[andres-erbsen]

I think this has been de-facto decided in favor of this proposal.