Update/shadow existing quotations?

[LdBeth]

MetaPRL theory files get inherited quotations from declared parent files, by direct iter Quotation.add over them, however 8.00 now adds check to Quotation.add that quotations with the same name cannot added twice. It is possible to check if the quotation has been added before add it, but I think the correct semantics is shadow old quotations with new one. Please consider keep a variant of Quotation.add that does shadowing instead of report failure when duplicated entries found.

[chetmurthy]

OK, so it's easy enough to add a Quotation.upsert entrypoint. But why is MetaPRL doing this? I mean, why would a theory file get loaded twice ?

So: why does Camlp5 8.00 have this new restriction? Well, quotations change the -language- you're parsing, right? So if you allow quotations to be overridden, then you can get different behaviour depending on which order two different modules are loaded/linked. This is really bad, and difficult-to-debug. Since typically you invoke camlp5 via a build-tool, even if were were a warning that you were overriding a quotation, it would be hidden in some rarely-consulted logfile.

Are you sure you want this? Maybe I can help you to change the way you structure quotations?

Historically, people using ML have used #load as their only way of accessing previous content. This has a lot of bad aspects, but the biggest one is that you cannot do separate compilation. Switching to actual module-open has two good qualities: (1) separate compilation, and (2) ability to express what you actually depend upon.

Anyway, let me know, and if you really want an unsafe update/upsert operation, I'll add it.

[chetmurthy]

OK, I added it: Quotation.upsert. Let me know if this does what you'd like (I didn't write a unit-test for it, b/c I don't want to make it something people would want to use normally).

[LdBeth]

But why is MetaPRL doing this? I mean, why would a theory file get loaded twice ?

There is a extend sigitem defined by MetaPRL's CamlP5 grammar that appears similar to open, but also handles grammar and other things that are not regular OCaml items.

When the CamlP5 grammar encounters extend Foo it will do a Quotation.add to both quotations defined in Foo, and those inherited from other ancestor files.

If in both theory Itt_a and Itt_b they have extend Base_grammar, and when a theory Itt_c that has both extend Itt_a and extend Itt_b, then the quotations in Base_grammar will be added twice.

And you can see this is similar to the notorious diamond problem of multiple inherence, and to properly solve that it seems more complex scope management such as selectively import or export quotations is required.

[chetmurthy]

So, um, I had to solve the same problem in Coq V5.10. I added a notion of modularity there, and that included for extensible grammars and pretty-printing, in addition to theorems, definitions, etc. The solution was to make "modules" a first-class construct, so when module D imports C, B, which each import A, then module A gets imported only once by whichever of C,B are imported first.

This shouldn't be a difficult thing to arrange, I would think.

[LdBeth]

"Modules" works in a strange way in MetaPRL because it is unlike many Curry-Howard correspondence base provers that really makes no distinction between proofs and programs, proof check and type check.

The proofs are done via an interactive interface, and a mechanism called "resources" is used to guard the soundness of proofs, i.e. the rule hasn't been used to prove itself, while I believe Coq/Agda/Lean only needs simple scope check for these. The problem is the current resource mechanism does not directly apply when first class modules are involved, which is reason why nested modules are not adopted in MetaPRL yet.

[chetmurthy]

I don't know whether modern Coq has nested modules, but when I implemented V5.10, it was just modules-equals-files. Just like caml-light did. Coq also proves things interactively, which means that a theorem cannot use itself in its proof, b/c the theorem doesn't exist until after it's been fully-proven.

I remember that Nuprl wasn't like this: a Nuprl "library" had all the theorems in it, and so theorem A's proof could cite theorem B, which could itself cite theorem A. I don't remember how circularity was avoided.

[LdBeth]

Coq also proves things interactively, which means that a theorem cannot use itself in its proof, b/c the theorem doesn't exist until after it's been fully-proven.

Yes, just like a function cannot be called by itself unless it is marked as rec in Caml, which means methods developed for functional languages can be applied with minor modifications. But to MetaPRL theorems are all compiled to sequent rewrite rules and can be used with or without proofs, it is only that there's an function checks if all theorems referenced by a proof have also been proved, and resources are for prevent creating circular dependency.

Nuprl library has a restriction that any theorem can only reference theorems listed before it in the library, it is similar to MetaPRL except it keeps both the definition and proofs of the library in a database, while MetaPRL has the definition in a file that will be compiled to OCaml module, and proofs in a separated database file.

[LdBeth]

so when module D imports C, B, which each import A, then module A gets imported only once by whichever of C,B are imported first.

Ok, now I made changes to make metaprl follow this behavior so that update grammar is now disallowed, and when a new quotation declared has the same name to the one already in the scope the Quotation.add will raise an error, and extend can ignore already existed quotations. I think it is still worth to keep Quotation.upsert so I can add a version of declaration that allows update the quotation in the future, if a user really wants to do that. But I think I want upsert not print to stderr but raise an exception so I can substitute the waring message.