Constraint/Guard OCaml 中的一种类型

Question

给定一个类型以构造二叉树：

type tree = Leaf of int | Node of int * tree * tree

现在假设我们想通过类型表达二叉树包含一个元素为零的节点，即我想表达以下形式的东西：

let rec p x = match x with 
            | Leaf(y) -> y = 0
            | Node(y,l,r) -> y = 0 || (p l) || (p r)

type zerotree = ZeroTree of t:tree where p(t)

这意味着，每当我有一棵 ZeroTree 类型的树时，我就可以确定该树包含一个元素为零的节点，即谓词 p 成立。

在 OCaml 中可以表达类似的东西吗？

Answer 1

答案1：不，你想要的超出了OCaml类型系统的范围。

答案2：可以将zerotree定义为与tree完全不同的类型。

type zerotree = 
  | ZLeaf
  | ZNodeL of int * zerotree * tree
  | ZNodeR of ... (* left for the reader *)
  | ZNodeI of ...

zerotree 要么是 ZLeaf，要么是 0 的叶子； ZNodeL，左子树为zerotree的节点； ZNodeR，右子树为zerotree的节点；或 ZNodeI，int 为 0.

的节点

答案3：答案2只适用于一些简单的数据结构和简单的不变量。在现实世界中，我们经常使用 私有类型 通过禁止任意构造值来强制执行不变量：

module Z : sig
  type zerotree = private Leaf of int | Node of int * zerotree * zerotree
  val leaf : int -> zerotree
  val node : int -> zerotree -> zerotree -> zerotree
end = struct
  type zerotree = Leaf of int | Node of int * zerotree * zerotree
  let rec p = function
    | Leaf y -> y = 0
    | Node(y,l,r) -> y = 0 || p l || p r
  let check zt = if p zt then zt else assert false
  let leaf i = check (Leaf i)
  let node i l r = check (Node (i,l,r))
end

open Z

(* let z = Leaf 1    Compile error: Cannot create values of the private type *)
(* let z = leaf 1    Runtime error *)
let z = leaf 0
let () = match z with  (* you can still pattern match *)
  | Leaf 0 -> ()
  | _ -> assert false

Type zerotree 与 tree 相同，但其构造函数在模块 Z 之外是私有的：您不能使用构造函数来创建值，而只能解构（即模式匹配）他们在模块之外。

值 zerotree 的构造必须通过函数 Z.leaf 和 Z.node 完成，这会检查您必须提供的属性。

Answer 2

混合解决方案是可行的，但它很笨重。这里我们保留了一个布尔值，这样我们就可以廉价地将零树转换为常规树。

type ('left, 'right) either = Left of 'left | Right of 'right

module type Zero_tree = sig
  type t = private Leaf of int | Node of bool * int * t * t
    (* The type of any tree. The boolean indicates whether
       this is a zero-tree.
       The type is private so we can guarantee that the
       boolean is set correctly.
    *)

  type z
    (* The type of zero-trees, a subtype of t which is guaranteed to contain
       at least one zero-node.
       In the module implementation, it uses the same representation as t.
    *)

  (* Constructors *)
  val leaf : int -> t
  val node : int -> t -> t -> t

  val leaf_zero : t
  val node_zero : t -> t -> z
  val node_left : int -> z -> t -> z
  val node_right : int -> t -> z -> z
  val node2 : int -> z -> z -> z

  (* Destructors *)
  val view : z -> t
  val classify : t -> (z, t) either
  val as_zero : t -> z option
end

module Zero_tree : Zero_tree = struct
  type t = Leaf of int | Node of bool * int * t * t
  type z = t

  let leaf n = Leaf n
  let leaf_zero = Leaf 0

  let is_zero = function
    | Leaf 0
    | Node (true, _, _, _) -> true
    | _ -> false

  let node n a b =
    let iz = n = 0 || is_zero a || is_zero b in
    Node (iz, n, a, b)

  let node_zero a b = node 0 a b
  let node_left = node
  let node_right = node
  let node2 = node

  let view x = x

  let classify x =
    if is_zero x then Left x
    else Right x

  let as_zero x =
    if is_zero x then Some x
    else None
end

Constraint/Guard OCaml 中的一种类型

Constraint/Guard a type in OCaml

ocaml

types