types - Coq 中的类型封装

Question

有没有一种方法可以在 Coq 模块中定义类型但封装构造函数？

我希望模块的客户端能够使用该类型但不能构造该类型的成员，类似于在 OCaml 中使用抽象类型可以完成的操作。

Answer 1

是的。您可以在模块中定义您的类型并为其分配模块类型:

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.

另一种可能性是将您的模块类型声明为依赖记录并通过合适的实现参数化您的开发，例如

Record FOO := { t : Type }.

Section Defs.

Variable Foo : FOO.

(* Code ... *)

End Defs.

(* Instantiate FOO *)

Definition Foo := {| t := nat |}.

严格来说，这并没有隐藏类型的构造函数，但只要您的客户只是使用接口(interface)编写他们的定义，他们就无法引用您的具体实现。