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

问题描述 投票:3回答:1

我是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]。

  1. 在这种记录类型中,有没有办法强制使用类型系统,nums1中的项目也不应该在nums2中,即它们的交集应该是空的?
type bar = {nums1: int list; nums2: int list;} ;;

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

先感谢您。

types ocaml
1个回答
4
投票

是的,不是。依赖于运行时值的类型称为a dependent type,而OCaml不支持完整范围的依赖类型。传统编程语言支持它们并不常见,因为它们使编程非常繁琐。例如,理论上,OCaml有足够的依赖类型来支持你的情况,除了你将无法使用listint,你将不得不使用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与许多其他编程语言一样,正在使用模块化算法,因此添加两个正数会导致负数,因此我们的示例很拙劣。但是为了举个例子,让我们忽略这个:)

© www.soinside.com 2019 - 2024. All rights reserved.