Typical Coq Encapsulation
Is there a way that I can define the type inside the Coq module but encapsulate the constructors?
I want the module client to be able to use this type, but not create members of that type, similar to what can be done in OCaml with an abstract type.
+3
Nico lehmann
source
to share
1 answer
Yes. You can define your type inside the module and assign the module type to it:
Module Type FOO.
Variable t : Type.
End FOO.
Module Foo : FOO.
Inductive typ :=
| T : typ.
Definition t := typ.
End Foo.
(* This fails *)
Check Foo.T.
Another possibility is to declare your module type as a dependent entry and parameterize your design over a suitable implementation, for example
Record FOO := { t : Type }.
Section Defs.
Variable Foo : FOO.
(* Code ... *)
End Defs.
(* Instantiate FOO *)
Definition Foo := {| t := nat |}.
Strictly speaking, this doesn't hide the type constructors, but as long as your client only writes their definitions using the interface, they won't be able to reference your specific implementation.
+4
Arthur Azevedo De Amorim
source
to share