Module Specifications.Assign5

Programming

Practice Problems (Ungraded)

These problems come the textbook OCP.

• powerset
• safe hd and tl
• list max exn string
• list max exn ounit
• account balance
• valid matrix
• fraction

Evaluation with Errors

In this problem we'll be looking at a common pattern for representing expressions with metadata. We'll look at arithmetic expressions with addition, subtraction, multiplication, division, and exponentiation.

Expressions are defined mutually recursively so that all expressions, including subexpressions, carry metadata of a given type parameter.

Note the very cool use of the and keyword, which allows use to define mutually recursive types (and functions). We'll be implementing an evaluator for expressions with metadata, and for which errors cases are handled using the result type.

There are two kinds of errors that could occur when evaluating an arithmetic expression of this form:

• The second argument of a division evaluates to zero, in which case evaluation should result in a DivByZero error.
• The second argument of an exponentiation evaluates to a negative number, in which case evaluation should result in a NegExp error.

Like expressions, errors carry metadata. As an example, we can imagine expressions and errors carrying data describing the line number at which an expression/error occurs, so that we can present a better error message to the user.

let ( let* ) = Result.bind

let guard b error = if b then Error error else Ok ()

let check x_res error =
  let* x = x_res in
  let* _ = guard (x = 0) error in
  Ok x

let _ = assert (check (Ok 2) () = Ok 2)
let _ = assert (check (Error ()) () = Error ())
let _ = assert (check (Ok 0) () = Error ())

Exception Handling

Deques

A double-ended queue, or dequeue, is a list-like data structure for which is possible to pop from and push to both the front and back. For our purposes a dequeue implements the following signature.

You need to implement two modules with this signature.

• ListDequeue, which takes t to be 'a list, and is implemented in the expected way. For this implementation push_back and pop_back will be inefficient.
• DoubleListDequeue, which takes t to be a 'a list * 'a list.

For the DoubleListDequeue implementation, we keep track of a front and back list, which we can pop from and push to. This means the the back list holds elements in reverse. In the case that the front list is empty when pop_front is called, the front and back list should be balanced. This means front and back after the call should have the property that

List.length back - List.length front <= 1

The same is true for a call to pop_back, the roles of front and back reversed. For example:

front: []                     front: [1;2;3;4;5;6]
 back: [5;4;3;2;1]             back: []

⇓ pop_front                   ⇓ pop_back

front: [2;3]                  front: [1;2;3]
 back: [5;4]                   back: [5;4]

Mapping Keys

In the second half of the course, we'll make use of maps and sets, which are implemented in OCaml using module functors. In the case of maps, we create a module for the type of we want to use for keys. For example, we use Map.Make to create structures for maps with a given type of key, e.g., StringMap and IntMap for maps with string keys and int keys, respectively. In the case of sets, we use Set.Make to create structures for sets with a given type of element.

Written

Partial Derivation

Not all judgments are derivable, but it's possible to write partial derivations of underivable judgments. These partial derivations can give us insight into why we get certain type errors when type-checking.

Formally, a typing derivation is partial if its leaves are not necessarily axioms. A partial derivation is maximal if every leaf of the derivation is either an axiom or a judgment which cannot be derived by any rule in our specification from any judgments.

Give maximal partial derivations of the following typing judgments.

    \varnothing \vdash \texttt{if true then 1 + 3 else x / false} : \texttt{int}
    

    \varnothing \vdash \texttt{if true then 1 + 3 else false / x} : \texttt{int}
    

In addition, write down the type error which OCaml gives you when trying to type-check each expression. What does the type-error tell you about the order in which OCaml type-checks sub-expressions?

Typing Derivation

So far, we haven't introduced any rules for typing recursive functions. Here's such a rule.

    \frac
    {\Gamma, f : \tau \to \tau_1, x : \tau \vdash e_1 : \tau_1
     \qquad
     \Gamma, f : \tau \to \tau_1 \vdash e_2 : \tau_2
    }
    {\Gamma \vdash \texttt{let rec} \ f \ x \ \texttt{=} \ e_1 \ \texttt{in} \ e_2 : \tau_2}
    

Note that this rule puts f into the context when determining the type of e_1, the body of f, which means that f can appear in its own body (and, hence, may be recursive). Using this rule, give a derivation of the following typing judgment.

    \varnothing \vdash \texttt{let rec sum l = match l with | [] -> 0 | h :: t -> h + sum t in sum} : \texttt{int → int}
    

This will be a somewhat wide derivation. You may use arrows as we've done in lecture to make the derivation less wide, but please make sure your solution is very clear.

Semantic Derivation

    \texttt{match 1 :: 2 :: [] with | [] -> true | h :: t -> false} \Downarrow \bot
    

Give a derivation of the above semantic judgment.