Coq 中的类型封装
Type encapsulation in Coq
有没有一种方法可以在 Coq 模块中定义类型但封装构造函数？
我希望模块的客户端能够使用该类型但不能构造该类型的成员，类似于在 OCaml 中使用抽象类型可以完成的操作。
是的。您可以在模块中定义类型并为其分配模块类型：
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 |}.
严格来说，这并没有隐藏类型的构造函数，但只要您的客户只是使用接口编写他们的定义，他们就无法引用您的具体实现。
有没有一种方法可以在 Coq 模块中定义类型但封装构造函数？
我希望模块的客户端能够使用该类型但不能构造该类型的成员，类似于在 OCaml 中使用抽象类型可以完成的操作。
是的。您可以在模块中定义类型并为其分配模块类型：
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 |}.
严格来说，这并没有隐藏类型的构造函数，但只要您的客户只是使用接口编写他们的定义，他们就无法引用您的具体实现。