Skip to content

Lecture 5.3: Specifications with Modules

Last class we implemented Sets as int lists. Let's take another look at that, but this time we will use a polymorphic set:

module type MySetSig = sig
  (* Type of sets *)
  type 'a t

  (* Construct an empty set *)
  val empty : 'a t

  (* Set membership *)
  val mem : 'a -> 'a t -> bool

  (* Insert an element into a set *)
  val insert : 'a -> 'a t -> 'a t

  (* Remove an element from a set *)
  val remove : 'a -> 'a t -> 'a t
end

Comparing this to our previous signature, notice how 'a t replaces t everywhere: 

module type MyIntSetSig = sig
  type t
  val empty : t
  val mem : int -> t -> bool
  val add : int -> t -> t
  val remove : int -> t -> t
end

We can also now define our polymorphic implementation in the same way as before, but this time we will use some standard library functions: 

module ListSet : MySetSig = struct
  type 'a t = 'a list;;
  let mem (x : 'a) (s : 'a t) : bool = List.mem x s
  let add (el : 'a) (s : 'a t) : 'a t = el :: s
  let remove (x : 'a) (s : 'a t) : 'a t = List.filter ((<>) x) s
end

Specs for sets

What are some algebraic properties we can state about sets?

  • nothing is in an empty set: $$ \forall x.\ \neg \verb|mem|\ x\ \verb|empty| $$
  • inserting an element means the element is in the set $$ \forall x\ S.\ \verb|mem|\ x\ (\verb|add|\ x\ S) $$
  • removing an element from a set means the element is not in the set $$ \forall x\ S.\ \neg \verb|mem|\ x\ (\verb|remove|\ x\ S) $$
  • adding an element shouldn't add any additional ones $$ \forall x\ y\ S.\ x \neq y \wedge \neg \verb|mem|\ y\ S \implies \neg \verb|mem|\ y\ (\verb|add|\ x\ S) $$
  • removing an element shouldn't remove any other ones $$ \forall x\ y\ S.\ x \neq y \wedge \verb|mem|\ y\ S \implies \verb|mem|\ y\ (\verb|remove|\ x\ S) $$

let's make another set implementation

module FunSet : MySetSig = struct
  type 'a t = 'a -> bool;;
  let empty = fun (_ : 'a) -> false;;
  let mem x s = s x;;
  let add x s = fun x' -> if x = x' then true else s x'
  let remove x s = fun x' -> if x = x' then false else s x'
end;;

module TestSet = FunSet;;


let prop_mem_empty = 
  fun (x : string) -> (* forall x ... *)
    not (TestSet.mem x TestSet.empty)
;;

let prop_mem_add = 
  fun (x, s : string * string TestSet.t) -> (* forall x TestSet... *)
    TestSet.(mem x (add x s))
;;

let prop_mem_remove = 
  fun (x, s : string * string TestSet.t) -> (* forall x TestSet... *)
    let open TestSet in
    not (mem x (remove x s))
;;

let prop_mem_add_other = 
  fun (x, y, s : string * string * string TestSet.t) -> (* forall x TestSet... *)
    let open TestSet in
    if x <> y && not (mem y s) then
      not (mem y (add x s))
    else true
;;


let prop_mem_remove_other = 
  fun (x, y, s : string * string * string TestSet.t) -> (* forall x TestSet... *)
    let open TestSet in
    if x <> y && mem y s then
      mem y (remove x s)
    else true
;;

let rec build_set_acc (n : int) (gen : unit -> 'a) (acc : 'a TestSet.t) : 'a TestSet.t
  = if n <= 0
    then acc
    else (build_set_acc (n - 1) gen (MySet.add (Random.int 10) acc))


let build_set (n : int) (g : unit -> 'a) : 'a TestSet.t = build_set_acc n g TestSet.empty

let gen_int (bound : int) () : int = Random.int bound   

let gen2 (g1 : unit -> 'a) (g2 : unit -> 'b) () : 'a * 'b =
  (g1 (), g2 ())

let gen3 (g1 : unit -> 'a) (g2 : unit -> 'b) (g3 : unit -> 'c) () : 'a * 'b * 'c =
  (g1 (), g2 (), g3 ())

let rec forall
  ?(trials = 1000)
  (gen : unit -> 'a)
  (prop : 'a -> bool)
  : int option =

  if trials <= 0 
  then None
  else  
    let xs = gen () in 
    if not (prop xs) 
    then Some xs
    else forall gen prop (trials - 1)

let test_mem_empty () =
  forall (fun () -> failwith "...etc" ) prop_mem_empty 10

Booleans as an abstract type

Last class we gained more practice with abstract types: how to write them using modules and module types, and how we can model various data structures and existing concepts using abstract types.

Today, we will see how abstract types are useful for program correctness. Recall our slogan: "abstract types prevent users from doing bad things". Is there a way to make this more precise? What is a "bad thing"?

What about this? 

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

(* module B : BSig = struct ...  end *)

What can we do here? We can have tru : t and fls : t, and we can case on a t by using ite. While we can case on a t, there are still only two values of t we can use. This means that M2.t is in bijection with the booleans: any boolean can be turned into a t, and vice versa. We can actually implement these functions: 

(* module M : S = struct ... end *)
let t_of_bool (b : bool) : B.t = if b then B.tru else B.fls
let bool_of_t (b : B.t) : bool = B.ite b true false

Let's now implement it: 

module B : BSig = struct
  type t = unit option
  let tru : t = None
  let fls : t = Some ()
  let ite b (t : 'a) (f : 'a) : 'a =
    match b with
    | None -> t
    | Some () -> f
end