The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Wed, Oct 30, 2019 at 9:57 PM Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:

> Not exactly what you describe, but "Extract Constant" and "Extract Inductive" could help.
> Consider:
>
> Inductive t := A | B (n: nat) | C (b: bool).
> Extract Inductive t => "Lib.t" [ "Lib.A" "Lib.B" "Lib.C" ].
>
> Then, t will be defined as an abbreviation for Lib.t, and the code for f will use constructors prefixed with Lib.  That might do what you want.

The problem with this strategy is that I need to do the same trick not just on `t`, but on any types used by `t`; otherwise the generated code will apply Lib.B to its own copy of nat, rather than the one in the original library, and OCaml will reject the application.

So, in your example, I'd need to add extraction commands for `nat` and `bool` as well.  In my case the types used in the ASTs are more complex, and that task will introduce a mess of had-to-maintain extraction commands :/

You're right, this trick must be applied to all inductive types in your hierarchy.  It is a maintenance burden, indeed.  But at least you should get meaningful errors when  something is wrong (missing or wrong Extract Inductive command).

>     * Add unsafe casts and hope for the best, which I think should work fine, but won't detect issues like version mismatches between the FooBarBaz library used on the OCaml and the FooBar library used on the Coq side.
>
> Hmph.  What's the point of proving code if you're adding unsafe casts in the end?

The extracted code is already full of Obj.magic, whose justification is meta-theoretical, to pacify the OCaml typechecker; wouldn't these be of a similar nature?

No.  For the casts inserted by extraction, type soundness was checked by the Coq type-checker.  In other words, the extracted code is type-safe, just not typeable in OCaml because its type system is too weak.  So, assuming extraction is sound and OCaml compiles correctly in the presence of Obj.magic, you can feel reasonably safe about these casts.

The casts you'd introduce to equate two independently-defined datatypes are not checked at all.  If you (or rather Coq's extraction) change one of the types but forget to update the other copy, disaster will ensue.

> Don't use unsafe casts :-)

Is there any way to make them safer? For example, can I use compiler libraries to ensure that the two types are the same?

Off the top of my head, I don't know.  That would be a non-trivial project.

Erik Martin-Dorel adds:

I'm unsure whether this would be useful for Clément's use case… but your discussion makes me think about OCaml's type-equation feature
(the corresponding grammar being http://caml.inria.fr/pub/docs/manual-ocaml/typedecl.html#type-equation ), for example:

module A = struct type nat = O | S of nat end
module B = struct type nat2 = A.nat = O | S of nat2 end

Yes, this would solve Clément's problem... if Coq's extraction could generate the datatype-with-equation form (nat2 in the example above).  But I don't see how it could.  Rewriting (e.g. by sed scripts) the .ml files after extraction might, but it's messy.

Also, like the approach I mentioned earlier, equations must be added to every datatype in the hierarchy.