Skip to content

Lecture 6.1: Abstract Types and Type Invariants

Booleans as an abstract type

We closed last class on a discussion of interface design and defined Booleans as the abstract type, along with a bijection to and from OCaml's Booleans 

module type BSig = sig
    type t
    val tru : t
    val fls : t 
    val ite : t -> 'a -> 'a -> 'a
end

module B : BSig = struct ...  end

let t_of_bool (b : bool) : B.t = if b then B.true else B.fls
let bool_of_t (x : B.t) : bool = B.ite x true false

module M : BSig = struct
    type t = unit option
    let tru = None
    let fls = Some ()
    let ite o x y = match o with | None -> x | Some _ -> y
end

Let's look at this once more, but this time using the Natural numbers as an abstract type:

module type NatSig = sig
    type t
    val z : t
    val s : t -> t
end

How many values of type t can we create? Infinitely many! There is one value of t for every natural number. Zero corresponds to z, while n + 1 corresponds to s n.

On it's nose, this is not particularly useful: we can only create Nats and we have no way to use them. Perhaps one way to make this more useful might be to introduce a similar kind of bijection between our nats and OCaml's integer type:

module type NatSig = sig
    type t
    val z : t
    val s : t -> t
    val to_int : t -> int
    val fr_int : int -> t
end

But this is not general enough! Lots of things correspond to the Naturals. Instead, we can make a more general bijection by adding a way to recurse on values. To handle this, we'll introduce recurse.

My claim is that recurse has all the ingredients we need to convert between any nat and any desired result.

module type NatSig = sig
    type t
    val z : t
    val s : t -> t

    val recurse : t -> 'a -> ('a -> 'a) -> 'a

    (* if we inspect a hypothetical combination of z's and s's: *)
    (* recurse x f zero = x *)
    (* recurse x f (succ (suc ... (suc zero))) = f (f ... (f x)) *)
end

We can now convert to and from (nonnegative) integers: 

let int_of_t (x : Nat.t) : int = 
    Nat.rec x 0 (fun x -> x + 1)

let rec t_of_int (x : int) : Nat.t = 
    if x <= 0 then Nat.z else 
        Nat.s (t_of_int (x - 1))

Let's implement this interface in a couple of different ways: 

module NatFl : NatSig = struct
    type t = float
    let z = 0.0
    let s x = x +. 1.0
    let rec recurse x v f = if x <= 0.0 then v else f (recurse (x -. 1.0) v f)
end

module NatList : NatSig = struct 
    type t = unit list
    let z = []
    let s xs = () :: xs
    let rec recurse xs v f = 
        match xs with
        | [] -> v
        | _ :: xs' -> f (recurse xs' v f)
end

module NatADT : NatSig = struct
    type t = | Z | S of t
    type z = Z
    let s x = S x
    let rec recurse x v f =
        match x with
        | Z -> v
        | S x' -> f (recurse x' v f)
end

While this presents a minimal interface, recurse also lets us recreate functions we would expect of the Naturals

module Nat = NatADT
let add n m = Nat.recurse m Nat.s n
let mul n m = Nat.recurse m z (fun m' -> add n m')

Type invariants

Next, will see how abstract types are useful for program correctness. Let's think of a simple example first.

Suppose you want to share a Nat resource between two processes while preventing data races. We can split this into "even" and "odds" and ensure that usage of one Nat never interferes with the other process. We can do this by using abstract types: we will have a type, in this case Even, and we will know by design that every value of this type always represents an even number.

OK, suppose we are now working with this type Even. What operations can we do with it? That is, what is its API?

We should certainly be able to create even numbers (say, starting from 0 and 2). And we should certainly be able to add even numbers together, since that will stay even. But we definitely can't add an even integer to an arbitrary one, since that might not be even.

We can translate that into a module type by including the allowed operations, and not including the ones we shouldn't be able to do: 

module type EvenSig = sig
    type t
    val zero : t
    val two : t
    val add : t -> t -> t
    val mult : t -> int -> t
    val get : t -> int
end

To create a t, there are two base cases: zero and two. Then, we can add ts together, and we can also multiply t's by arbitrary numbers (since that preserves the property of being even). We also have a function get, for turning a t back into an int.

Now that we have the module type, we can go back to our main question: what is the "bad thing" that we want to prevent users from doing?

We want to make sure that if x : t, then get x is never odd. Turned around: we want an invariant (something that should always be true) that:

  • if x : t, then (get x) mod 2 = 0.

Assuming that the functions are implemented in the ways we expect, this invariant should be true.

Now, let's implement EvenSig. To do this, we have to choose a type for t. Since this type is meant to encode even integers, we can just let the type be int itself: 

module Even : EvenSig = struct
    type t = int
    let zero = 0
    let two = 2
    let add x y = x + y
    let mult x y = x * y
    let get i = i
end

How can we check that the invariant always holds? There are two options:

Checking Invariants via Traces

One way is to use property-based testing. Let's randomly create values of type Even.t, and see if they actually are even.

let flip a b =
    if Random.bool () then a () else b ()

let rec mk_even (n : int) : Even.t = 
    if n <= 0
    then flip (fun _ -> Even.zero) (fun _ -> Even.two)
    else flip (fun _ -> Even.add  (mk_even (n - 1)) (mk_even (n - 1)))
              (fun _ -> Even.mult (mk_even (n - 1)) (Random.int 50))

let check_even (n : int) : bool = 
    let e = mk_even n in 
    (Even.get n) mod 2 = 0

Checking Invariants via Dynamic Checks

Instead of doing property-based testing, we can instead allow our functions to throw an exception if they ever see a "bad" value of type even:

module EvenChecked : EvenSig = struct
  type even = int
  let zero = 0
  let two = 2
  (* notice that with_check and mk are /not/ in the EvenSig interface *)
  let with_check (f : unit -> even) : even =
      let x = f () in 
      if x mod 2 = 0 then x else failwith "INTERNAL ERROR: Invariant does not hold!" 
  let mk i = with_check (fun _ -> if i mod 2 = 0 then Some i else None)

  let add x y = with_check (fun _ -> x + y)
  let mult x y = with_check (fun _ -> x * y)
  let get i = i
end

If our invariant actually does hold, then we won't see the internal error, and EvenChecked will behave exactly the same as Even. But if there was a bug, this will eventually catch it.

Question

Pros/cons of using PBT versus using a wrapper that can throw an exception?