Incremental Include

[gmalecha]

From @gstew5

[gstew5]

Here's the rendered version of the proposal: https://github.com/coq/ceps/blob/31bcb7d97621390f37929a908a8032ce153667ac/text/000-incremental-include.md

[gares]

This reminds me of the module type of X feature of OCaml, but here it is about reusing the body and the type of first class values rather than modules (in some sense, Prove x = Lemma x : type of INTERFACE.x, Use x = Include (Module Tmp. Definition x := body of INTERFACE.x End Tmp)). I need to sleep on the extra thing "in the current context", which seems very powerful but also a bit too automagic to my taste (not unlike the current Include).

[gstew5]

Prove x = Lemma x : type of INTERFACE.x
Use x = Include (Module Tmp. Definition x := body of INTERFACE.x End Tmp).
...

That captures to some degree what we're proposing. But note that body of INTERFACE.x and type of INTERFACE.x will in general be open terms (up to the parameters declared before x in the module type).

So for example, in the module type:

Module Type INTERFACE.
  Axiom P : nat.
  Definition x := P + P.
End INTERFACE.

x is bound to an open definition like:

definition INTERFACE 
  x (app [global (const «Init.Nat.add»), abs INTERFACE P, abs INTERFACE P])

where

type abs string -> string -> term
pred definition o:string, o:string, o:term.

(or similar).

Then in a context like:

Module Implementation : INTERFACE.
  Provide Definition P := 0.
  Use x.
End Implementation.

The Use x desugars to

Include (Module Tmp. Definition x := body[abs INTERACE P |-> global (const «P»)]. End Tmp).

A similar substitution happens in types too.

I need to sleep on the extra thing "in the current context", which seems very powerful but also a bit too automagic to my taste (not unlike the current Include).

I don't think UseAll Available From INTERFACE is essential. But it does facilitate the use of modules like:

Module Type INTERFACE.
  Parameter P : nat.
  Definition x1 := ... P ...
  Definition x2 := ... P ...
  ...  
  Definition xN := ... P ...

  Parameter Q : nat.
  Definition y1 := ... x1 ... xN ... P ... Q ...
  Definition y2 := ... x1 ... xN ... P ... Q ...
  ...
  Definition yM := ... x1 ... xN ... P ... Q ...
End INTERFACE.

Here, it seems very convenient to be able to say:

Module Implementation : INTERFACE.
  Provide Definition P := 0.
  UseAll Available From INTERFACE. (*Desugars to Use x1. Use x2. ... Use xN.*)
  Provide Definition Q := x2.
  UseAll Available From INTERFACE. (*Desugars to Use y1. Use y2. ... Use yM.*)
End Implementation.

The alternative without UseAll Available is:

Module Implementation : INTERFACE.
  Provide Definition P := 0.
  Use x1. Use x2. ... Use xN.
  Provide Definition Q := x2.
  Use y1. Use y2. ... Use yM.
End Implementation.

which is admittedly better than copying all the definitions, but still tedious (because all of x1...xN and y1...yM must be named).

[gares]

Your explanation is very clear, thanks.

On this example it is easy to explain why UseAll smells a little fishy to me.

Module Implementation : INTERFACE.
  Provide Definition P := 0.
  UseAll Available From INTERFACE. (*Desugars to Use x1. Use x2. ... Use xN.*)
  Provide Definition Q := x2.
  UseAll Available From INTERFACE. (*Desugars to Use y1. Use y2. ... Use yM.*)
End Implementation.

The first UseAll should not pull in all the yn because of the dependency on Q which is not available yet, if I got it right.

This seems a little fragile, sometimes dependencies are hidden in implicit arguments (which you don't see) or in proof terms generated by tactics which may change if you tune a hint here or there (again you don't see them). I'm not against such a thing, but it may not be the best practice in polished files.

[gstew5]

The first UseAll should not pull in all the yn because of the dependency on Q which is not available yet, if I got it right.

Yes, that's right.

I agree that UseAll Available may have less intuitive semantics than the other forms. I don't think it's absolutely essential; the qualified forms Use x and Use x From INTERFACE would already be quite useful.

[Blaisorblade]

This seems a little fragile, sometimes dependencies are hidden in implicit arguments (which you don't see) or in proof terms generated by tactics which may change if you tune a hint here or there (again you don't see them). I'm not against such a thing, but it may not be the best practice in polished files.

If an interface proves a large number of derived theorems, UseAll seems likely to be very important.

Moreover, I am not sure these hidden dependencies really cause a problem. If they do, another semantics is possible and would fix that altogether.

Now, suppose that Definition y1 does not mention Q, and let's look at the semantics of this snippet in the implementation:

  Provide Definition P := 0.
  UseAll Available From INTERFACE.
  Provide Definition Q := x2.

I see two options for UseAll, and it might be desirable to provide both. The key requirement is that collectively, using UseAll covers everything from the interface, and that at each step UseAll provides enough to instantiate the next parameter.

• UseAll could Use of everything between Parameter P and Parameter Q. Thus, y1 is not available even if we could import it. Thus, what's available is independent of y1's body, and we can still Use y1 explicitly if we wanted. This seems appropriate if interfaces are written like the above, where definitions come before axioms they do not use. And crucially, this addresses your concern @gares.
• UseAll could also automatically Use y1, following your proposal, which is more complete. This seems more appropriate if, say interfaces declare all axioms early.

Both options achieve the two goal

In either case, what's the effect of expose y1 early?

• If y1 isn't used early, there's no effect.
• With or without y1, the type of Q is already well-formed, even if it needs other definitions in the interface: those definitions have all been imported.
• y1 can be used to define Q. That will break if y1 starts using Q, as you say. But I'm not sure that's a big problem or so undesirable: an implementation is expected to be tightly coupled to its interface.

[gares]

It seems UseAll is also available in interfaces. Sure, if you immediately implement it, you notice things changed. But my understanding is that you wanted to first build a bunch of interfaces and then parallelize implementation.

Anyway, I'm not against it. I would somehow prefer a more explicit way to name a bunch of things (not a sub module, but something giving anyway a name to a bunch of entries, so that you could write Use That). Unfortunately I don't have much experience of fiddling with modules, I don't have better ideas.

I think we could (or better you guys) start with UseAll and if it backfires too often come up with something more explicit.

[Blaisorblade]

It seems UseAll is also available in interfaces. Sure, if you immediately implement it, you notice things changed. But my understanding is that you wanted to first build a bunch of interfaces and then parallelize implementation.

I see. My alternative proposal would implicitly group definitions by source-code order: basically, as-if everything after an axiom depended on it. Not sure if @gstew5 would like that, but today's a US holiday.

Ah that's what I was missing: for UseAll in interfaces, this fragility might indeed be a problem. It's also a problem if you want to give another definition by hand (which however might not be supported here!).

And there are interesting usecases, where a Module Type gives a way to provide a Parameter in terms of another one. An artificial example:

Module Type Monoid.
  Parameter monoid : monoidT.
  (* Theory. *)
  Parameter somethingElse : ...
  Definition foo := body1. (* Does not use something else! *)
  (* *)
End Monoid.

Module Type FieldMonoid.
  Parameter field : fieldT.
  Provide Definition monoid := ... (* Implement [monoid] in terms of [field]. *)
  UseAll From Monoid.
  Definition foo := body2. (* Will fail if [foo] was already [Use]d. Not syntactically equal to [body1], but maybe definitionally equal. *)
  Provide somethingElse : ...
End FieldMonoid.  

I'd never do this example, but this is a common pattern with mixin modules/abstract classes: you can basically encode (non-destructive!) inheritance of abstract classes/mixin modules.

[gares]

The more I think about this, and the more I'm convinced it can be implemented in user space using Coq-Elpi (plus a few extra APIs which don't seem rocket science).

This API is too weak, since it does not give you access to a proper name (a gref data type), but it is close. Once you have it you can fetch its body/type in the current module/module-type. A missing API is to know the dependencies among objects, but I think I can reuse some code from coq-dpdgraph for that.

[gstew5]

@gares I do have a (pretty sketchy) implementation of some of these features in coq-elpi (that prototype prompted this CEP, in fact). I'd characterize it as a very early prototype since it doesn't deal with things like inductives, etc. That said, the proposed features seem generally useful, and might be easier to implement directly in Coq.

In my prototype, in a module type like:

Module Type INTERFACE0.
  Axiom N : nat.
  Axiom S : nat.
  Axiom N_S : N = S + 1.
  Definition x := N + S.
  Definition y := S + x.
end INTERFACE0 exporting x y N_S.

I hack the End INTERFACE0 to export definitions for x, y up to the open terms N and S:

DEBUG accum-def Exporting definition: name [x]
DEBUG accum-def Exporting definition: term 
[app [global (const «Init.Nat.add»), abs N, abs S]]
DEBUG accum-def Exporting definition: name [y]
DEBUG accum-def Exporting definition: term 
[app [global (const «Init.Nat.add»), abs S, abs x]]

Provide Definition N := ... adds a binding for abs N.
Use x defines x against the bindings for abs terms.

My current prototype has relations like:

  % a new term type to track abstracted constants
  type abs string -> term.

  % [global-ref Name GR] maps names to the grefs that define them (LHS)
  pred global-ref o:string, o:term.
  :name "global-ref.fail"
  global-ref Name _ :- coq.error "global ref" Name "is undefined".

  % [definition ModTyName Name T] maps names to their definitions (RHS)
  pred definition o:string, o:string, o:term.
  :name "definition.fail"
  definition _ModTyName Name _ :-
    coq.error "Did not find a definition of" Name.

After implementing the prototype once, I think it could be reimplemented in a nicer way if there were APIs for accessing the terms defined in a module type and for easily calculating dependencies between terms (as you're suggesting above, I think).

[gstew5]

external pred coq.env.module-type i:modtypath, o:list id.

This API is useful, but it didn't seem like there's currently a way to access the definitions of the terms given by list id.

[gares]

This API is useful, but it didn't seem like there's currently a way to access the definitions of the terms given by list id.

Indeed, the API has to be changed to expose a list of gref. Then you can fetch the body and substitute it.
I mean, given one of these terms you want to use, say x:

• for each of its dependency in the module (one needs another API to compute these efficiently), hence INTERFACE0.N and INTERFACE0.S
• locate in the current module something called "N" and something called "S", say M.N and M.S (what you already do for Provide seems perfect here)
• load in the context copy (global (const <<INTERFACE0.N>>)) (global (const <<M.N>>)) => ..
• then call coq.env.const "x" Body _Type, copy Body NewBody, coq.env.add-const "x" NewBody _ ...

It is an alternative to your end INTERFACE exporting which is a nice idea BTW, but a bit more clunky that what I propose, I believe. Of course one needs to patch the existing API (I think it is trivial to do) and add a new one to compute the depes of an object within a module. The developers of coq-dpdgraph told me they are interested in this feature (currently they don't stop at module boundaries), so maybe I'll give it a try next week (either in dpdgraph, or in Coq-Elpi directly).

What is missing is that some objects (notations, hints...) do have names in Coq (internally) but I've never bound them to Elpi. I guess you may want to Use these objects as well at some point.

[Blaisorblade]

The more I think about this, and the more I'm convinced it can be implemented in user space using Coq-Elpi (plus a few extra APIs which don't seem rocket science).

With Coq-Elpi, Use term must re-typecheck term's body, spending extra time and potentially generating fresh universes. I don't expect large terms in interfaces, or significant performance problems, but I'm ignorant, and the Coq kernel works hard to avoid this extra typechecking with functors and Include (at least https://link.springer.com/chapter/10.1007/10930755_18 does). Will we have to worry at some point?

[gares]

Yes you are correct, if you put the feature in the logic you can optimize that, but you wound need to check anyway that the captured variables have the correct type.

No idea if this matters in practice.