CODEWITHSUNDEEP
typesocaml
Max Maier
Max Maier

Reputation: 1045

Constraint/Guard a type in OCaml

Given is a type in order to construct a binary tree:

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

Now assume we want to express via types that a binary tree contains a node with an element zero, i.e., I would like to express something of the following form:

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)

That means, whenever I have a tree of type ZeroTree, then I can be sure that the tree contains a node with an element zero, i.e., the predicate p holds.

Is something like that expressible in OCaml?

Upvotes: 0

Views: 349

Answers (2)

Martin Jambon
Martin Jambon

Reputation: 4909

A hybrid solution is possible but it's clunky. Here we keep a boolean around so we can cheaply convert from a zero-tree to a regular one.

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

Upvotes: 0

camlspotter
camlspotter

Reputation: 9030

Answer 1: No. What you want is beyond the scope of OCaml type system.

Answer 2: You can define zerotree as a completely different type from tree. 

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

zerotree is either ZLeaf, a leaf with 0; ZNodeL, a node whose left subtree is zerotree; ZNodeR, a node whose right subtree is zerotree; or ZNodeI, a node whose int is 0.

Answer 3: Answer 2 only works for some simple data structures and simple invariants. In the real world we often use private types to enforce the invariants by forbid arbitrary construction of values:

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 is as same as tree but its constructors are private outside of module Z: you cannot use the constructors to create values but only deconstruct (i.e. pattern match) them outside of the module.

Construction of the value zerotree must be done via the functions Z.leaf and Z.node, which check the property you have to provide.

Upvotes: 4

Related Questions