我是OCaml的新手,并一直在探索类型系统的功能。我有两个问题。
type foo = {all_nums: int list; nums1: int list; nums2: int list;} ;;
例如如果nums1 = [1]且nums2 = [2; 3]然后all_nums必须是[1; 2; 3]。
type bar = {nums1: int list; nums2: int list;} ;;
例如如果nums1 = [1],nums2也不能包含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与许多其他编程语言一样,正在使用模块化算法,因此添加两个正数会导致负数,因此我们的示例很拙劣。但是为了举个例子,让我们忽略这个:)