The Coq mailing list

[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