types - 有没有办法使用 OCaml 类型系统来强制执行有关值的规则？

Question

我对 OCaml 还很陌生，一直在探索类型系统的功能。我有两个问题。

1. 在这个记录类型中，有没有办法使用 OCaml 的类型系统来强制执行 nums1 + nums2 = all_nums 的规则？

type foo = {all_nums: int list; nums1: int list; nums2: int list;} ;;

例如如果 nums1 = [1] 且 nums2 = [2; 3] 那么 all_nums 必须是 [1; 2； 3].

在此记录类型中，是否有一种方法可以使用类型系统强制执行 nums1 中的任何项目也不应出现在 nums2 中，即它们的交集应为空？

type bar = {nums1: int list; nums2: int list;} ;;

例如如果 nums1 = [1]，nums2 也不能包含 1。

提前谢谢您。

Answer 1

是和否。依赖于运行时值的类型称为 a dependent type ，并且 OCaml 不完全支持依赖类型。传统编程语言并不典型地支持它们，因为它们使编程变得相当麻烦。例如，理论上，OCaml 有足够的依赖类型来支持您的情况，但您将无法使用 list或int ，并且您必须为它们使用 GADT 表示。最终，它几乎无法使用。因为，OCaml 类型系统仍然是静态的，所以它必须在程序执行之前检查您的程序对于所有可能的集合是否有效。这将极大地限制可打字程序的集合。

但是，使用抽象类型与幻像类型相结合，可以对任意不变量进行编码并依赖类型系统来保存它。诀窍是定义一个小的可信内核，其中不变量是手动强制执行的。

以你的第一个例子为例，

 module Foo : sig 
   type t 
   val create : int list -> int list -> int list -> (t,error) result
 end = struct 
   type t = {all_nums: int list; nums1: int list; nums2: int list;}
   type error = Broken_invariant
   let create all_nums nums1 nums2 = 
      if invariant_satisfied all_nums nums1 nums 2 
      then Ok {all_nums; nums1; nums2}
      else Error Broken_invariant
 end

使用这种密封表示，无法在模块外部创建 Foo Foo.t 类型的值其中invariant_satisfied不是true 。因此，您的Foo是受信任的内核 - 您需要检查是否保留不变式的唯一地方。类型系统将处理剩下的事情。

如果您使用幻像类型，例如，您可以编码更复杂的不变量并且更具表现力，例如，

 module Number : sig 
     type 'a t 
     type nat
     type neg
     type any = (nat t, neg t) Either.t


     val zero : nat t
     val one : nat t
     val of_int : int -> any
     val padd : nat t -> nat t -> nat t 
     val gadd : 'a t -> 'b t -> any
 end = struct 
     type 'a t = int 
     type nat 
     type neg
     type any = (nat t, neg t) Either.t

     let zero = 0
     let one = 1
     let of_int x = if x < 0 then Right x else Left x
     let padd x y = x + y (* [see note 2] *)
     let gadd x y = of_int (x + y)
 end

其中Either.t类型定义为 type ('a,'b) t = Left of 'a | Right of 'b

<小时/>

注释

注意 1。您的第一个示例可以以不可能破坏不变量的方式进行编码，例如，而不是在 all_nums 中复制数据。 ，你可以代表你的类型 {nums1 : int list; nums2 : int list}并定义all_nums作为一个函数，let all_nums = List.append

注 2. 事实上，由于 OCaml 与许多其他编程语言一样，使用模算术，两个正数相加可能会导致负数，因此我们的示例是拙劣的。但为了举例，让我们忽略这一点:)