The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

On 27.04.2017 03:03, Julia Belyakova wrote:
> 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.

Doesn't the following, proposed in the previous mail by Istvan, do
exactly that?

> 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. 

Of course, the annoying part is that addition is defined twice.  This is
something I have also encountered when I do hiding via modules:  Many of
the things that *are* exported have to be duplicated.

; Ralf

> 
> 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
>  
> <mailto: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
>