The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Note that truly hiding private definitions which are used to define public transparent ones would break subject reduction, and is impossible; it would mean that you could unfold a well-typed identifier and get a term which is invalid.

On Thu, Apr 27, 2017, 10:46 AM Jason Gross <jasongross9 AT gmail.com> wrote:

Does this do what you want?

Module Type Addition.
  Parameter t : Type.
  Parameter add : t -> t -> t.
End Addition.

Module MAddition <: Addition.

  Definition t := nat.
  Definition add x y := x + y.     (* I want this to be available *)

  Local Definition priv_id (x : t) := x. (* This must be hidden *)
End MAddition.

On Thu, Apr 27, 2017, 7:45 AM Julia Belyakova <julbinb AT gmail.com> wrote:

Hello Ralf,

I use an aux private function to implement a public one, so this solution does not work in this case.

--

Kind regards, Julia

чт, 27 апр. 2017 г., 3:25 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
>