The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Le jeudi 03 mai 2007 à 11:03 +0200, Guillaume Melquiond a écrit :

> I am trying to use the module system with Coq 8.1 and I don't seem to
> get a sensible behavior. The following example defines an interface A (a
> module type) and an implementation B (a module) for this interface. The
> function g is an implementation detail (not in A, only in B) and it
> should be hidden to the user of module B.

(Replying to my own mail, as all the replies pointed to the same
syntax.)

Thanks a lot for your replies. When reading the documentation, I only
understood the "with" syntax as a way to specialize the parameters of a
module type; it did not occur to me that it would also change the symbol
from being opaque to being transparent. So thanks for pointing this out.

In my case, this syntax is a bit unpractical, as it requires all the
functions with some computational content (f in my original example) to
use the "with" syntax too, in order to be computed. It means that I
cannot factor out code from the exported functions, nor can I use
tactics (e.g. for proof terms used as function arguments), and so on.

So I kept searching for a way of preventing implementation details from
leaking while being able to compute with complicated functions defined
in modules. Here is the solution I found:

        Module Type A.
          Parameter T : Type.
          Parameter f : T -> T.
        End A.
        
        Module B <: A.
          Definition T := nat.
          Module Detail.
            Definition g := fun x : T => x.
          End Detail.
          Import Detail.
          Definition f := fun x : T => g (S x).
        End B.
        
        Import B.
        Eval compute in (f 0). (* = 1 : T *)
        Print g. (* User error: g is not a defined object *)

The implementation detail g is now hidden from the user, yet it is
possible to compute the result of f. This solution is not perfect, as
"Detail" still leaks in global scope, while not being part of the module
type. But I can live with this minor pollution.

Best regards,

Guillaume