The Coq mailing list

[Julia Belyakova <julbinb AT gmail.com>]

Thank you for reply!

Are there other ways to hide some parts of a module except for opaque typing? I am primarily interested in hiding auxiliary lemmas.

It seems to me strange though that one cannot actually _use_ functions from the opaque-typed module. 

--

Kind regards,

Julia

ср, 26 апр. 2017 г., 17:10 ikdc <ikdc AT mit.edu>:

On 04/26/2017 04:57 PM, Julia Belyakova wrote:
> Dear Coq users,
>
> I guess it's a stupid question, but...
>
> I want to define a module with certain parts being hidden. For this I
> define a module type and then use opaque typing for the module. And the
> problem is that now I cannot compute functions of the module, their
> definitions are not accessible.
>
> Please, find a simple example below.
>
> Module Type Addition.
>   Parameter t : Type.
>   Parameter add : t -> t -> t.
> End Addition.
>
> Module MAddition : Addition with Definition t := nat.
>   Definition t := nat.
>   Definition add x y := x + y.     (* I want this to be available *)
>   Definition priv_id (x : t) := x. (* This must be hidden *)
> End MAddition.
>
> (* priv_id is not available as desired *)
> (* Compute (MAddition.priv_id 4). *)
> (* add is available, but the call does not reduce to 7 *)
> Compute (MAddition.add 3 4).
>


If I understand correctly, I don't think you can do this.  The fact that
the module type is opaque means that any program which uses a module
with that type must behave the same way; in particular it may not unfold
the definitions hidden by the module type.  You could of course do this:


Module MAddition : Addition
     with Definition t := nat
     with Definition add := fun x y => x + y.
   Definition t := nat.
   Definition add x y := x + y.
   Definition priv_id (x : t) := x.
End MAddition.


But if you want to be able to compute through [add], then perhaps the
module type "Addition" isn't actually the interface you want to be using
in the first place.

I don't know very much about the module system, so someone please
correct me if this is wrong.

--
Istvan Chung