Skip to content

Homework 5: Modules and Invariants

Due: Sunday, October 12 11:59pm

Submission Instructions

Start with the template code here.

  • Replace each failwith "TODO" with your solution.
  • Be sure to test your solutions in utop or in tests alongside your submission. To load your file into utop, use #use "hw5.ml";;.
  • Submit your version of hw5.ml to the HW4 assignment on Gradescope. Only submit hw5.ml; NOT any other files or folders.
  • At the top of the template file, there is a comment for you to write in approximately how many hours you spent on the assignment. Filling this in is optional, but helpful feedback for the instructors.

Q1: An abstract type for non-empty lists

There are many applications where one wants to store a list of items, but we don't want the list to ever be empty. For example, think of a type of paths in a graph: we can represent this as a list of vertices, but since the path always has an origin, the list is never empty.

One way to do this is to implement a new type, nelist: 

type 'a nelist = | First of 'a | Cons of 'a * 'a nelist

While this can work, the main issue is that we then have to re-implement all of the list primitives on nelist (e.g., map, fold, and so on), which duplicates a lot of effort. Additionally, we might want to cast a nelist back into a list, which would require traversing the whole list to recursively build up the list.

Instead, we will implement non-empty lists as an abstract type, whose implementation is a wrapper around an ordinary list. Below is our signature for the corresponding module: 

module type NonEmptySig = sig
    type 'a t
    val well_formed : 'a t -> bool
    val mk : 'a -> 'a t
    val cons : 'a -> 'a t -> 'a t
    val uncons : 'a t -> ('a * ('a t) option) 
    val to_list : 'a t -> 'a list
end

We can then implement the module type in the following way: 

module NonEmpty = struct
    type 'a t = 'a list

    (* INVARIANT: xs has length > 0 *)
    let well_formed xs = 
        match xs with
        | [] -> false
        | _ :: _ -> true

    let mk x = [x]
    let cons x xs = x :: xs
    let uncons xs = 
        match xs with
        | [] -> failwith "UNREACHABLE"
        | [x] -> (x, None)
        | x :: xs' -> (x, Some xs')
    let to_list xs = xs
end

Q1.1 For each of the functions in NonEmpty that (may) return a value of type 'a t, explain why the invariant well_formed must hold of the output, given that well_formed holds of the inputs.
Additionally, for uncons, explain why we should never throw the exception failwith "UNREACHABLE".

(*
    Q1.1: Explain why the invariant is maintained for each of the following
    functions, and UNREACHABLE should never be reached:
    - mk: TODO
    - cons: TODO
    - uncons: TODO
*)

Q1.1: Grading Criteria

If you have valid explanations for each of the three functions.

Q1.2

For each of the following possible extensions to the NonEmptySig API, explain why it can or cannot be implemented in NonEmpty while maintaining the invariant. If it cannot be implemented while maintaining the invariant, explain how it could be adapted to a version that can maintain the invariant (for example, by returning an option and failing in some cases).

module type NonEmptySig = sig 
    ...
    (* Map the elements of the nonempty list by the function. *)
    val map : 'a t -> ('a -> 'b) -> 'b t

    (* Filter the nonempty list by the function (removing the element if the
    function returns false on that element.) *)
    val filter : 'a t -> ('a -> bool) -> 'a t
end

(* Q1.2: 
    - map: TODO
    - filter: TODO
*)

Q1.2: Grading Criteria

For each function:

  • Whether you have correctly identified if it can or cannot preserve the invariant as-is; and
  • If it cannot preserve the invariant, how it could be changed to make the invariant preserved.

Q2: A type for balanced trees

Now, we will implement a type for balanced binary trees: one where the depth of any path in the tree is the same length as any other depth.

We will do so by first defining a raw tree: 

type 'a raw_tree = | Leaf of 'a | Node of 'a raw_tree * 'a raw_tree
We call it a raw tree since it allows the user to write non-balanced trees (such as Node (Leaf 3, Node (Leaf 4, Leaf 5))), which has a depth of 0 on the left subtree and 1 on the right subtree.)

Below is our module type defining an API for balanced trees:

module type BalancedTreeSig = sig
    (* The type for balanced trees. *)
    type 'a t

    (* Is the balanced tree well-formed? *)
    val well_formed : 'a t -> bool

    (* Build the balanced tree consisting of a single leaf. *)
    val leaf : 'a -> 'a t

    (* Build the balanced tree consisting of a node (or returning None if it would result in a non-balanced tree.) *)
    val node : 'a t -> 'a t -> 'a t option

    (* Return the underlying raw_tree. *)
    val to_tree : 'a t -> 'a raw_tree
end

In this question, you will implement a module for balanced trees: 

module BalancedTree = struct
    type 'a t = unit (* TODO: Replace with your chosen type! *)

    let well_formed _ = failwith "TODO"

    let leaf _ = failwith "TODO"

    let node _ _ = failwith "TODO"

    let to_tree _ = failwith "TODO"
end

You may choose any internal representation for balanced trees. (Since you need to implement to_tree, storing at least the underlying raw_tree will be useful.)

Then, implement well_formed, leaf, node, and to_tree. For well_formed, you should ensure that any data stored within 'a t are valid: e.g., if it holds a raw_tree, that raw_tree should actually be balanced, and any other data that 'a t holds should also be well formed.

For node, node t1 t2 should return Some if and only if t1 and t2 are themselves well-balanced and have the same (constant) depth on all paths. If t1 and t2 have different depths, you should return None.

Hint

It will be useful to store more information than just the raw_tree in 'a t; perhaps something relating to the depth.

Q2: Grading Criteria

Whether you have:

  • correctly implemented the four functions;
  • correctly implemented well_formed so that if it returns true, then the underlying tree is balanced; and
  • successfully preserved the well_formed invariant for leaf and node.