Clever Geek Handbook

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


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


source






More articles:


All Articles